亲大费 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
a beverage vending machine pay sprite selec beer
Transition systems a transition systems is a tuple A = 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 𝒜 = 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 = 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 𝒜 = 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
