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

In the following, let δrj denote the transitionfunction for register rj resulting from the circuit diagram. Then:τ(a1 , . . . , an , c1 , . . . , ck )( a1 , . . . , an , c1 , . . . , ck ) −→ input evaluation register evaluationif and only if cj = δrj (a1 , . . . , an , c1 , . . . , ck ). Assuming that the evaluation of input bitschanges nondeterministically, no restrictions on the bits a1 , .

. . , an are imposed.It is left to the reader to check that applying this recipe to the example circuit in the leftpart of Figure 2.2 indeed results in the transition system depicted in the right part of thatfigure.Data-Dependent SystemsThe executable actions of a data-dependent system typically result from conditional branching, as inif x%2 = 1 then x := x + 1 else x := 2·x fi.In principle, when modeling this program fragment as a transition system, the conditionsof transitions could be omitted and conditional branchings could be replaced by nondeterminism; but, generally speaking, this results in a very abstract transition system forwhich only a few relevant properties can be verified. Alternatively, conditional transitionscan be used and the resulting graph (labeled with conditions) can be unfolded into a transition system that subsequently can be subject to verification. This unfolding approach isdetailed out below.

We first illustrate this by means of an example.Example 2.12.Beverage Vending Machine RevisitedConsider an extension of the beverage vending machine described earlier in Example 2.2(page 21) which counts the number of soda and beer bottles and returns inserted coins if thevending machine is empty. For the sake of simplicity, the vending machine is representedby the two locations start and select. The following conditional transitionstrue : coin→ selectstart andtrue : refillstart → startmodel the insertion of a coin and refilling the vending machine.

Labels of conditionaltransitions are of the form g : α where g is a Boolean condition (called guard), and α isan action that is possible once g holds. As the condition for both conditional transitions30Modelling Concurrent Systemsabove always holds, the action coin is always enabled in the starting location. To keepthings simple, we assume that by refill both storages are entirely refilled. Conditionaltransitionsnsoda > 0 : sget→ startselect andnbeer > 0 : bgetselect → startmodel that soda (or beer) can be obtained if there is some soda (or beer) left in the vendingmachine. The variables nsoda and nbeer record the number of soda and beer bottles in themachine, respectively.

Finally, the vending machine automatically switches to the initialstart location while returning the inserted coin once there are no bottles left:nsoda = 0 ∧ nbeer = 0: ret coin→ startselect Let the maximum capacity of both bottle repositories be max . The insertion of a coin(by action coin) leaves the number of bottles unchanged. The same applies when a coinis returned (by action ret coin).

The effect of the other actions is as follows:ActionrefillsgetbgetEffectnsoda := max ; nbeer := maxnsoda := nsoda − 1nbeer := nbeer − 1The graph consisting of locations as nodes and conditional transitions as edges is nota transition system, since the edges are provided with conditions. A transition system,however, can be obtained by “unfolding” this graph. For instance, Figure 2.3 on page 31depicts this unfolded transition system when max equals 2.

The states of the transitionsystem keep track of the current location in the graph described above and of the numberof soda- and beer bottles in the vending machine (as indicated by the gray and black dots,respectively, inside the nodes of the graph).The ideas outlined in the previous example are formalized by using so-called programgraphs over a set Var of typed variables such as nsoda and nbeer in the example. Essentially, this means that a standardized type (e.g., boolean, integer, or char) is associatedwith each variable. The type of variable x is called the domain dom(x) of x.

Let Eval(Var)denote the set of (variable) evaluations that assign values to variables. Cond(Var) is theset of Boolean conditions over Var, i.e., propositional logic formulae whose propositionalsymbols are of the form “x ∈ D” where x = (x1 , . . . , xn ) is a tuple consisting of pairwisedistinct variables in Var and D is a subset of dom(x1 ) × . . . × dom(xn ). The proposition(−3 < x − x 5) ∧ (x 2·x ) ∧ (y = green),for instance, is a legal Boolean condition for integer variables x and x , and y a variablewith, e.g., dom(y) = { red, green }.

Here and in the sequel, we often use simplified notationsTransition Systems31refillrefillstartrefillcoinselectbeersodastartstartcoinselectbgetcoinsgetselectsgetstartbgetstartstartcoincoinselectcoinselectsgetselectsgetbgetbgetstartstartcoincoinselectselectsgetbgetstartcoinret coinselectFigure 2.3: Transition system modeling the extended beverage vending machine.32Modelling Concurrent Systemsfor the propositional symbols such as “3 < x − x 5” instead of “(x, x ) ∈ { (n, m) ∈IN2 | 3 < n − m 5 }”.Initially, we do not restrict the domains. dom(x) can be an arbitrary, possibly infinite,set. Even if in real computer systems all domains are finite (e.g., the type integer onlyincludes integers n of a finite domain, like −216 < n < 216 ), then the logical or algorithmicstructure of a program is often based on infinite domains.

The decision which restrictionson domains are useful for implementation, e.g., how many bits should be provided forrepresentation of variables of type integer is delayed until a later design stage and isignored here.A program graph over a set of typed variables is a digraph whose edges are labeled withconditions on these variables and actions. The effect of the actions is formalized by meansof a mappingEffect : Act × Eval(Var) → Eval(Var)which indicates how the evaluation η of variables is changed by performing an action. If,e.g., α denotes the action x := y+5, where x and y are integer variables, and η is theevaluation with η(x) = 17 and η(y) = −2, thenEffect(α, η)(x) = η(y) + 5 = −2 + 5 = 3, and Effect(α, η)(y) = η(y) = −2.Effect(α, η) is thus the evaluation that assigns 3 to x and −2 to y.

The nodes of aprogram graph are called locations and have a control function since they specify whichof the conditional transitions are possible.Definition 2.13.Program Graph (PG)A program graph PG over set Var of typed variables is a tuple (Loc, Act, Effect, →, Loc0 , g0 )where• Loc is a set of locations and Act is a set of actions,• Effect : Act × Eval(Var) → Eval(Var) is the effect function,• → ⊆ Loc × Cond(Var) × Act × Loc is the conditional transition relation,• Loc0 ⊆ Loc is a set of initial locations,• g0 ∈ Cond(Var) is the initial condition.Transition Systems33g:αThe notation → is used as shorthand for (, g, α, ) ∈ →. The condition g is alsog:αcalled the guard of the conditional transition → . If the guard is a tautology (e.g.,αg = true or g = (x < 1) ∨ (x 1)), then we simply write → .The behavior in location ∈ Loc depends on the current variable evaluation η.

A nong:αdeterministic choice is made between all transitions → which satisfy condition g inevaluation η (i.e., η |= g). The execution of action α changes the evaluation of variablesaccording to Effect(α, ·). Subsequently, the system changes into location . If no suchtransition is possible, the system stops.Example 2.14.Beverage Vending MachineThe graph described in Example 2.12 (page 29) is a program graph. The set of variablesisVar = { nsoda , nbeer }where both variables have the domain { 0, 1, .

. . , max }. The set Loc of locations equals{ start , select } with Loc0 = { start }, andAct = { bget , sget, coin, ret coin, refill } .The effect of the actions is defined by:Effect(coin, η)Effect(ret coin, η)Effect(sget, η)Effect(bget, η)Effect(refill , η)=====ηηη[nsoda := nsoda−1]η[nbeer := nbeer −1][nsoda := max , nbeer := max ]Here, η[nsoda := nsoda−1] is a shorthand for evaluation η with η (nsoda) = η(nsoda)−1and η (x) = η(x) for all variables different from nsoda. The initial condition g0 states thatinitially both storages are entirely filled, i.e., g0 = (nsoda = max ∧ nbeer = max ).Each program graph can be interpreted as a transition system.

The underlying transitionsystem of a program graph results from unfolding. Its states consist of a control component,i.e., a location of the program graph, together with an evaluation η of the variables.States are thus pairs of the form , η. Initial states are initial locations that satisfy theinitial condition g0 . To formulate properties of the system described by a program graph,the set AP of propositions is comprised of locations ∈ Loc (to be able to state at whichcontrol location the system currently is), and Boolean conditions for the variables.