a beverage vending machine pay sprite selec beer
Transition systems a transition systems is a tuple A =<S, So, T,a, B> where o sis a finite or infinite set of states o Is initial location o T is a finite or infinite set of transitions o a and B are two mapping from Tto S which take each transition t in Tto the two states a(t)and b(t, respectively the source and the target of the transition t a transition t with some source s and target s is ritten t:s→s’ Several transitions can have the same source and target a transition system is finite if s and Tare finite
Transition systems ◼ A transition systems is a tuple 𝒜 =< 𝑆, 𝑆0, 𝑇, 𝛼, 𝛽 > where S is a finite or infinite set of states, 𝑆0 is initial location T is a finite or infinite set of transitions, 𝛼 and 𝛽 are two mapping from T to S which take each transition t in T to the two states 𝛼(𝑡) and 𝛽(𝑡), respectively the source and the target of the transition t. ◼ A transition t with some source s and target s’ is written t : s→s’. ◼ Several transitions can have the same source and target. ◼ A transition system is finite if S and T are finite
Paths a path of length n, n>0, in a transition system A is a sequence of transitions t, t2. t such that vi:1≤i<n,β(t)=a(t+1),anda(t1)=S Similarly, an infinite path is an infinite sequence of transitions [1,2 tn… such that vi:1≤i<n,β(t)=a(t+1),anda(t1)=S
Paths ◼ A path of length n, n > 0, in a transition system 𝒜 is a sequence of transitions 𝑡1 , 𝑡2 ⋯ 𝑡𝑛,such that ∀𝑖: 1 ≤ 𝑖 < 𝑛, 𝛽 𝑡𝑖 = 𝛼(𝑡𝑖+1 ), and 𝛼 𝑡1 = 𝑆0 ◼ Similarly, an infinite path is an infinite sequence of transitions 𝑡1 , 𝑡2, ⋯ 𝑡𝑛, ⋯such that ∀𝑖: 1 ≤ 𝑖 < 𝑛, 𝛽 𝑡𝑖 = 𝛼(𝑡𝑖+1 ), and 𝛼 𝑡1 = 𝑆0
if彐t∈T,a(t)=s∧β(t)=s′, we say s→s,we define the generalized transition relation C SX A× S such that oIfs→s,s oIfs→S’,S′→S", we say s→S" Let A =<S,So, T,a, B> be a Ts, we say S is reachable if s∈S,So∈S,S0-→S
◼ 𝑖𝑓 ∃ 𝑡 ∈ 𝑇, 𝛼 𝑡 = 𝑠 ⋀𝛽 𝑡 = 𝑠 ′ ,we say s → 𝑠 ′ , we define the generalized transition relation ↠⊆ S × A × S such that If s → 𝑠 ′ , s ↠ 𝑠 ′ If s ↠ 𝑠 ′ , s ′ ↠ 𝑠 ′′ , 𝑤𝑒 𝑠𝑎𝑦 𝑠 ↠ 𝑠 ′′ ◼ Let 𝒜 =< 𝑆, 𝑆0 ,𝑇, 𝛼, 𝛽 > be a TS, we say s is reachable if 𝑠 ∈ 𝑆, 𝑠0 ∈ 𝑆0 , 𝑠0 ↠ 𝑠
Let t be a transition system a state s is a terminal state of t if there are no state s' such that s→s′ a state s is a deadlock state of t if s is reachable and terminal
◼ Let T be a transition system. A state s is a terminal state of T if there are no state s’ such that s → 𝑠 ′ . ◼ A state s is a deadlock state of T if s is reachable and terminal