NANJING UNIVERSITY Transition System Lei Bu bulei@nju.edu.cn
Lei Bu bulei@nju.edu.cn Transition System
效绵县 Definitions and notations Reactive System The intuition is that a transition system consists of a set of possible states for the system and a set of transitions or state changes which the system c can effect. When a state change is the result of an external event or of an action made by the system,then that transition is labeled with that event or action. Particular states or transitions in a transition system can be distinguished
Definitions and notations ◼ Reactive System ◼ The intuition is that a transition system consists of a set of possible states for the system and a set of transitions - or state changes - which the system can effect. ◼ When a state change is the result of an external event or of an action made by the system, then that transition is labeled with that event or action. ◼ Particular states or transitions in a transition system can be distinguished
效绵鼎 model to describe the behavior of systems digraphs where nodes represent states,and edges model transitions state: the current color of a traffic light the current values of all program variables the program counter 0 the value of register and output transition:("state change") o a switch from one color to another the execution of a program statement the change of the registers and output bits for a new input
◼ model to describe the behavior of systems ◼ digraphs where nodes represent states, and edges model transitions ◼ state: the current color of a traffic light the current values of all program variables + the program counter the value of register and output ◼ transition: (“state change”) a switch from one color to another the execution of a program statement the change of the registers and output bits for a new input
效绵鼎 A beverage vending machine pay sprite select beer
效绵鼎 Transition systems A transition systems is a tuple A=<S,So,T,a,B> where o S is a finite or infinite set of states, So is initial location o Tis a finite or infinite set of transitions, a and B are two mapping from T to 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 written t:S→S. Several transitions can have the same source and target. A transition system is finite if S and T are 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