Write T for the set of finite paths and T@ for the set of infinite paths. The mappings a and B can be extended to tt by defining a(t1…tn)=a(t1),β(t1…tn)=(tn) o A finite path c represents a finite evolution of a TS from state a(c)toβ(c) Similarly the mapping a is extended to to by defining a(t1 o a infinite path c represents an infinite evolution of a TS from state ac)
◼ Write 𝑇 + for the set of finite paths and 𝑇 𝜔 for the set of infinite paths. The mappings 𝛼 and 𝛽 can be extended to 𝑇 + by defining 𝛼 𝑡1 … 𝑡𝑛 = 𝛼 𝑡1 , 𝛽 𝑡1 … 𝑡𝑛 = 𝛽(𝑡𝑛) A finite path 𝑐 represents a finite evolution of a TS from state 𝛼 𝑐 to 𝛽 𝑐 ◼ Similarly, the mapping 𝛼 is extended to 𝑇 𝜔 by defining 𝛼 𝑡1 … = 𝛼 𝑡1 , A infinite path 𝑐 represents an infinite evolution of a TS from state 𝛼 𝑐
A partial product over Tt is defined as o ifc=t1 .tn is a path of lengthn, if c=t.tm is a path of length m, and if B(c)=a(c C·C t'm is a finite path of length n+m and a(c·c)=a(c),B(c·c)=B(c T+ To: if c is a finite path, and c an infinite path, such that B(c)= a(c), then cc is an infinite path and a(cc=ac) Empty path: for each state s of S, define the empty path Es of length zero, and a(es=B(es) If c is a finite path and if s a( c ands=B(c, then Es C=c=c Es; If c is an infinite path and ifs=a(c), then EsC=C
◼ A partial product over 𝑇 + is defined as if 𝑐 = 𝑡1 …𝑡𝑛 is a path of length n, if 𝑐′ = 𝑡′1 … 𝑡′𝑚 is a path of length m, and if 𝛽 𝑐 = 𝛼 𝑐′ 𝑐 ∙ c ′ = 𝑡1 … 𝑡𝑛 𝑡′1 … 𝑡′𝑚 is a finite path of length n+m and 𝛼 𝑐 ∙ c ′ =𝛼 𝑐 , 𝛽 𝑐 ∙ c ′ =𝛽 𝑐′ ◼ 𝑇 + × 𝑇 ω: if c is a finite path, and 𝑐 ′ an infinite path, such that 𝛽 𝑐 = 𝛼 𝑐′ ,then 𝑐 ∙ c ′ is an infinite path and 𝛼 𝑐 ∙ c ′ =𝛼 𝑐 ◼ Empty path: for each state s of S, define the empty path ε𝑠 of length zero, and 𝛼 ε𝑠 =𝛽 ε𝑠 =s. ◼ If c is a finite path and if s = 𝛼 𝑐 and s′ = 𝛽 𝑐 , then ε𝑠 ∙c =c=c ∙ ε𝑠 ′ ; If c is an infinite path and if s = 𝛼 𝑐 , then ε𝑠 ∙c=c
Labeled transition systems a transition system labeled by an alphabet a is a 6- tuple aA = S, So, T,a, B,n> where o <S,So, T,a, B>is a transition system, o n is a mapping from t to A taking each transition t to its label n(t Intuitively, the label of a transition indicates the action or event which triggers the transition
Labeled transition systems ◼ A transition system labeled by an alphabet A is a 6- tuple 𝒜 =< 𝑆, 𝑆0 ,𝑇, 𝛼, 𝛽, 𝜆 > where < 𝑆, 𝑆0 , 𝑇,𝛼,𝛽 > is a transition system, 𝜆 is a mapping from T to A taking each transition t to its label 𝜆(𝑡) ◼ Intuitively, the label of a transition indicates the action or event which triggers the transition
It is logical to assume that two different transitions cannot have the same source target and label It is not necessary to distinguish two transitions that are triggered by the same action and that make the transition system pass from the same state s to the same state s This implies<a,λ,B>:T→S× A X Sis injective o An injective function is a function which associates distinct arguments to distinct values An injective functio A non-injective function In a given state the same action can provoke two different transitions ading to different states: a(t)=a(t) and n(t)=n(t,) do not necessarily imply t
◼ It is logical to assume that two different transitions cannot have the same source, target and label. ◼ It is not necessary to distinguish two transitions that are triggered by the same action and that make the transition system pass from the same state s to the same state s’ ◼ This implies < 𝛼, 𝜆, 𝛽 >:𝑇 → 𝑆 × 𝐴 × 𝑆 is injective An injective function is a function which associates distinct arguments to distinct values ◼ In a given state, the same action can provoke two different transitions leading to different states: 𝛼 𝑡 = 𝛼 𝑡′ and 𝜆 𝑡 = 𝜆 𝑡′ do not necessarily imply 𝑡 = 𝑡′
a beverage vending machine pay sprite get_beer insert_coin rate sele ct be eer