亲大费 NANJING UNIVERSITY Transition System bulei@nju.edu.cn
卜磊 bulei@nju.edu.cn Transition System
■ Part I: Introduction Chapter 0: Preliminaries o Chapter 1: Language and Computation ■ Part II: Models o Chapter 2: Finite Automata o Chapter 3: Regular Expressions o Chapter 4: Context-Free Grammars o Chapter 5: Pushdown Automata o Chapter 6: Turing machines
◼ Part I: Introduction Chapter 0: Preliminaries Chapter 1: Language and Computation ◼ Part II: Models Chapter 2: Finite Automata Chapter 3: Regular Expressions Chapter 4: Context-Free Grammars Chapter 5: Pushdown Automata Chapter 6: Turing Machines
Part Ill: Modeling o Chapter 7: Transition Systems o Chapter 8: Petri Nets, Time Petri Nets o Chapter 9: Timed Automata, Hybrid Automata o Chapter 10: Message Sequence Charts Part IV: Model Checking and tools o Chapter 11: Introduction of Model Checking o Chapter 12: SPiN Model Checker o Chapter 13: UPPAAL: a model-checker for real-time systems o Chapter 14
◼ Part III: Modeling Chapter 7: Transition Systems Chapter 8: Petri Nets, Time Petri Nets Chapter 9: Timed Automata, Hybrid Automata Chapter 10: Message Sequence Charts ◼ Part IV: Model Checking and Tools Chapter 11: Introduction of Model Checking Chapter 12: SPIN Model Checker Chapter 13: UPPAAL: a model-checker for real-time systems Chapter 14:…
7. 1 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
7.1 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 o the current color of a traffic light o the current values of all program variables the program counter o the value of register and output transition: ("state change o a switch from one color to another o the execution of a program statement o 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