5. Principles of Model Checking. Baier_ Joost (2008) (5. Principles of Model Checking. Baier_ Joost (2008).pdf), страница 9

In both cases, it is required that there be atmost one initial state.Definition 2.5.Deterministic Transition SystemLet TS = (S, Act, →, I, AP, L) be a transition system.1. TS is called action-deterministic if | I | 1 and | Post(s, α) | 1 for all states sand actions α.2. TS is called AP-deterministic if | I | 1 and |Post(s) ∩ { s ∈ S | L(s ) = A }| 1for all states s and A ∈ 2AP .2.1.1ExecutionsSo far, the behavior of a transition system has been described at an intuitive level.

Thiswill now be formalized using the notion of executions (also called runs). An execution of atransition system results from the resolution of the possible nondeterminism in the system.An execution thus describes a possible behavior of the transition system. Formally:Definition 2.6.Execution FragmentLet TS = (S, Act, →, I, AP, L) be a transition system.

A finite execution fragment ofTS is an alternating sequence of states and actions ending with a stateαi+1−→ si+1 for all 0 i < n, = s0 α1 s1 α2 . . . αn sn such that si −−−Transition Systems25where n 0. We refer to n as the length of the execution fragment . An infinite executionfragment ρ of TS is an infinite, alternating sequence of states and actions:αi+1−→ si+1 for all 0 i.ρ = s0 α1 s1 α2 s2 α3 . .

. such that si −−−Note that the sequence s with s ∈ S is a legal finite execution fragment of length n=0. Eachprefix of odd length of an infinite execution fragment is a finite execution fragment. Fromnow on, the term execution fragment will be used to denote either a finite or an infiniteexecution fragment. Execution fragments = s0 α1 . . . αn sn and ρ = s0 α1 s1 α2 . . . willbe written respectively asα1αn→ .

. . −−→ sn = s0 −−andα1α2ρ = s0 −−→ s1 −−→ ... .An execution fragment is called maximal when it cannot be prolonged:Definition 2.7.Maximal and Initial Execution FragmentA maximal execution fragment is either a finite execution fragment that ends in a terminalstate, or an infinite execution fragment. An execution fragment is called initial if it startsin an initial state, i.e., if s0 ∈ I.Example 2.8.Executions of the Beverage Vending MachineSome examples of execution fragments of the beverage vending machine described in Example 2.2 (page 21) are as follows. For simplicity, the action names are abbreviated, e.g.,sget is a shorthand for get soda and coin for insert coin.sgetsgetcoinτcoinτ−−→ select −→soda −−−→ pay −−−−→ select −→soda −−−→ . . .ρ1 = pay −−sgetbgetτcoinτsoda −−−→ pay −−−−→ select −→beer −−−→ . .

.ρ2 = select −→sgetcoinτcoinτ−−→ select −→soda −−−→ pay −−−−→ select −→soda .= pay −−Execution fragments ρ1 and are initial, but ρ2 is not. is not maximal as it does notend in a terminal state. Assuming that ρ1 and ρ2 are infinite, they are maximal.Definition 2.9.ExecutionAn execution of transition system TS is an initial, maximal execution fragment.26Modelling Concurrent SystemsIn Example 2.8, ρ1 is an execution, while ρ2 and are not. Note that ρ2 is maximal butnot initial, while is initial but not maximal.A state s is called reachable if there is some execution fragment that ends in s and thatstarts in some initial state.Definition 2.10.Reachable StatesLet TS = (S, Act, →, I, AP, L) be a transition system.

A state s ∈ S is called reachable inTS if there exists an initial, finite execution fragmentα1α2αn→ s1 −−→ . . . −−→ sn = s .s0 −−Reach(TS) denotes the set of all reachable states in TS.2.1.2Modeling Hardware and Software SystemsThis section illustrates the use of transition systems by elaborating on the modeling of(synchronous) hardware circuits and sequential data-dependent systems – a kind of simplesequential computer programs. For both cases, the basic concept is that states representpossible storage configurations (i.e., evaluations of relevant “variables”), and state changes(i.e., transitions) represent changes of “variables”. Here, the term “variable” has to beunderstood in the broadest sense. For computer programs a variable can be a controlvariable (like a program counter) or a program variable.

For circuits a variable can, e.g,stand for either a register or an input bit.Sequential Hardware CircuitsBefore presenting a general recipe for modeling sequential hardware circuits as transitionsystems we consider a simple example to clarify the basic concepts.Example 2.11.A Simple Sequential Hardware CircuitConsider the circuit diagram of the sequential circuit with input variable x, output variabley, and register r (see left part of Figure 2.2). The control function for output variable yis given byλy = ¬(x ⊕ r)Transition Systems27yxXORNOTyxx0 r0x1 r0x0 r1x1 r1ORrrx ryFigure 2.2: Transition system representation of a simple hardware circuit.where ⊕ stands for exclusive or (XOR, or parity function).

The register evaluation changesaccording to the circuit functionδr = x ∨ r .Note that once the register evaluation is [r = 1], r keeps that value. Under the initialregister evaluation [r = 0], the circuit behavior is modeled by the transition system TSwith state spaceS = Eval(x, r)where Eval(x, r) stands for the set of evaluations of input variable x and register variabler. The initial states of TS are I = { x = 0, r = 0, x = 1, r = 0 }. Note that there aretwo initial states as we do not make any assumption about the initial value of the inputbit x.The set of actions is irrelevant and omitted here. The transitions result directly from the→ x = 0, r = 1 if the next input bitfunctions λy and δr . For instance, x = 0, r = 1 −equals 0, and x = 0, r = 1 −→ x = 1, r = 1 if the next input bit is 1.It remains to consider the labeling L.

Using the set of atomic propositions AP = { x, y, r },then, e.g., the state x = 0, r = 1 is labeled with { r }. It is not labeled with y since thecircuit function ¬(x ⊕ r) results in the value 0 for this state. For state x = 1, r = 1 weobtain L(x = 1, r = 1) = { x, r, y }, as λy yields the value 1. Accordingly, we obtain:L(x = 0, r = 0) = { y }, and L(x = 1, r = 0) = { x }.

The resulting transition system(with this labeling) is depicted in the right part of Figure 2.2.Alternatively, using the set of propositions AP = { x, y } – the register evaluations areassumed to be “invisible” – one obtains:L (x = 0, r = 0) = { y }L (x = 1, r = 0) = { x }L (x = 0, r = 1) = ∅L (x = 1, r = 1) = { x, y }The propositions in AP suffice to formalize, e.g., the property “the output bit y is setinfinitely often”.

Properties that refer to the register r are not expressible.28Modelling Concurrent SystemsThe approach taken in this example can be generalized toward arbitrary sequential hardware circuits (without “don’t cares”) with n input bits x1 , . . . , xn , m output bits y1 , . . . , ym ,and k registers r1 , .

. . , rk as follows. The states of the transition system represent the evaluations of the n+k input and register bits x1 , . . . , xn , r1 , . . . , rk . The evaluation of outputbits depends on the evaluations of input bits and registers and can be derived from thestates. Transitions represent the behavior, whereas it is assumed that the values of input bits are nondeterministically provided (by the circuit environment). Furthermore, weassume a given initial register evaluation[r1 = c0,1 , . . . , rk = c0,k ]where c0,i denotes the initial value of register i for 0 < i k. Alternatively, a set ofpossible initial register evaluations may be given.The transition system TS = (S, Act, →, I, AP, L) modeling this sequential hardware circuithas the following components.

The state space S is determined byS = Eval(x1 , . . . , xn , r1 , . . . , rk ).Here, Eval(x1 , . . . , xn , r1 , . . . , rk ) stands for the set of evaluations of input variables xi andregisters rj and can be identified with the set { 0, 1 }n+k .2 Initial states are of the form(. . . , c0,1 , . . .

, c0,k ) where the k registers are evaluated with their initial value. The firstn components prescribing the values of input bits are arbitrary. Thus, the set of initialstates isI = (a1 , . . . , an , c0,1 , . . . , c0,k ) | a1 , . . . , an ∈ { 0, 1 } .The set Act of actions is irrelevant, and we choose Act = { τ }. For simplicity, let the setof atomic propositions beAP = { x1 , . . . , xn , y1 , . . . , ym , r1 , . .

. , rk } .(In practice, this could be defined as any subset of this AP). Thus, any register, anyinput bit, and any output bit can be used as an atomic proposition. The labeling functionassigns to any state s ∈ Eval(x1 , . . . , xn , r1 , . .

. , rk ) exactly those atomic propositions xi ,rj which are evaluated to 1 under s. If for state s, output bit yi is evaluated to 1, then(and only then) the atomic proposition yi is part of L(s). Thus,L(a1 , . . . , an , c1 , . . . , ck ) = { xi | ai = 1 } ∪ { rj | cj = 1 }∪ { yi | s |= λyi (a1 , . . . , an , c1 , . . . , ck ) = 1 }An evaluation s ∈ Eval(·) is a mapping which assigns a value s(xi ) ∈ { 0, 1 } to any input bit xi .Similarly, every register rj is mapped onto a value s(rj ) ∈ { 0, 1 }. To simplify matters, we assume everyelement s ∈ S to be a bit-tuple of length n+k. The ith bit is set if and only if xi is evaluated to 1(0 < i n). Accordingly, the n+jth bit indicates the evaluation of rj (0 < j k).2Transition Systems29where λyi : S → {0, 1} is the switching function corresponding to output bit yi that resultsfrom the gates of the circuit.Transitions exactly represent the behavior.