Software Validation and Verification First Exercise Sheet Exercise 1 2

For this exercise we give the following definition: Definition 1. Deterministic Transition System Let TS = (S,Act,!, I,AP, L) be a transition system. 1. TS is called action-deterministic if | I |  1 and |Post(s,↵) |  1 for all states s and actions ↵. 2. TS is called AP-deterministic if | I |  1 and |Post(s) \ {s 0 2 S | L(s 0) = A}|  1 for all states s and A 2 2AP. Consider the following the transition system TS1.