效绵县 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,l,B>:T→×A×S is injective An injective function is a function which associates distinct arguments to distinct values An injective function A non-injective function In a given state,the same action can provoke two different transitions leading to different states:a(t)=a(t)and (t)=(t)do not necessarily imply t 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 𝑡 = 𝑡′