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

In such cases,TS1 can be understood as a refinement of TS2 , since TS1 resolves some nondeterminismin TS2 . TS1 , TS2 also holds when TS2 arises from TS1 by means of an abstraction.In fact, abstraction is a fundamental concept that permits the analysis of large or even aninfinite transition systems. Abstraction is identified by a set of abstract states S;abstraction function f , which associates to each (concrete) state s of the transition systemTS the abstract state f (s) which represents it; and a set AP of atomic propositions whichlabel the concrete and abstract states.

Abstractions differ in the choice of the set Sof abstract states, the abstraction function f , and the relevant propositions AP. Theconcept of abstraction functions has, in fact, already been used in several examples in thismonograph. For instance, an abstraction function was used for the Bakery algorithm inorder to prove that the infinite transition system TSBak has a finite bisimulation quotient,see Example 7.13 (page 461). Due to the special structure of the transition system,here a bisimulation-equivalent transition system results. Typically, however, an abstracttransition system results that simulates TS.We briefly outline the essential ideas of abstractions that are obtained by aggregatingdisjoint sets of concrete states into single abstract states. Abstraction functions mapconcrete states onto abstract ones, such that abstract states are associated with equallylabeled concrete states only.Definition 7.50.Abstraction FunctionLet TS = (S, Act, →, I, AP, L) be a transition system, and S be a set of (abstract) states.f : S → S is an abstraction function if for any s, s ∈ S: f (s) = f (s ) implies L(s) = L(s ).The abstract transition system TSf originates from TS by identifying all states that arerepresented by the same abstract state under abstraction function f .

An abstract stateis initial whenever it represents an initial concrete state. Similarly, there is a transitionfrom abstract state f (s) to state f (s ) if there is a transition from s to s .500Equivalences and AbstractionDefinition 7.51.Abstract Transition SystemLet TS = (S, Act, →, I, AP, L) be a (concrete) transition system, S a set of (abstract)states, and f : S → S an abstraction function. The abstract transition system TSf = Act, →f , If , AP, Lf ) induced by f on TS is defined by:(S,• →f is defined by the rule:α→ ss −−αf (s) −−→ f f (s )• If = { f (s) | s ∈ I }• Lf (f (s)) = L(s) for all states s ∈ SLemma 7.52.Let TS = (S, Act, →, I, AP, L) be a (concrete) transition system, S a set of (abstract)states, and f : S → S an abstraction function.

Then TS , TSf .Proof: Follows from the fact that R = { (s, f (s)) | s ∈ S } is a simulation for (TS, TSf ).Example 7.53.An Automatic Door OpenerConsider an automatic door opener as modeled by the (concrete) transition system inFigure 7.18; for simplicity, the action labels are omitted from the transitions. Let AP ={ alarm, open }. The door opener requires a three-digit code d1 d2 d3 as input with di ∈{ 0, . . . , 9 }. It allows an erroneous digit to be entered, but this may happen at most twice.The variable error keeps track of the number of wrong digits that have been provided, andis initially zero.

In case error exceeds two, the door opener issues an alarm signal. On asuccessful input of the door code, the door is opened. Once locked again, it returns to itsinitial state. Location i (for i = 0, 1, 2) indicates that the first i digits of the code havebeen correctly entered; the second component of a state indicates the value of the variableerror (if applicable).Consider the following two abstractions. In the first abstraction, the concrete states areaggregated as indicated by the dashed ovals in Figure 7.18. In fact, this is a data abstraction in which the domain of the variable error is restricted to { 1, 2 }, i.e., the values 0 and1 are not distinguished in the abstract transition system.

The corresponding abstractionSimulation Relations501function f is defined byf (, error = k) =, error 1if k ∈ { 0, 1 }, error = 2if k = 2For all other concrete states, f is the identity function. It immediately follows that fis indeed an abstraction function, as only equally labeled states are mapped onto thesame abstract state.

The abstract transition system TSf is depicted in Figure 7.19; byconstruction we have TS , TSf .0 , 01 , 02 , 00 , 11 , 12 , 13{ open }0 , 21 , 242 , 2{ alarm }Figure 7.18: Transition system of the door opener0 , 11 , 12 , 13{ open }0 , 21 , 242 , 2{ alarm }Figure 7.19: Abstract transition system of the door opener (under abstraction function f )Now consider an abstraction in which we completely abstract from the value of the variableerror. The concrete states that are aggregated are indicated by the dashed ovals in Figure502Equivalences and Abstraction7.20. The corresponding abstraction function g is defined by g(, error = k) = , for anylocation ∈ { 0 , 1 , 2 }; g is the identity function otherwise.

This yields the transitionsystem TSg in Figure 7.21. As g is indeed an abstraction function, it follows that TS ,TSg .0 , 01 , 02 , 00 , 11 , 12 , 13{ open }0 , 21 , 242 , 2{ alarm }Figure 7.20: Alternative aggregation of states for the door opener.0123{ open }4 { alarm }Figure 7.21: Abstract transition system of the door opener (under abstraction functiong).The abstract transition systems in the previous example have been obtained by choosingfor the variable error in the system an abstract domain that is smaller than its originaldomain { 0, 1, 2 }.

Let us illustrate what such a type of abstraction (also known as dataabstraction) means for program graphs. The essential idea of abstraction in programgraphs is to abstract from concrete values of certain program variables or locations, i.e.,program counters. Rather than keeping track of the concrete and precise value of variables,only abstract values are considered. For instance, a possible abstraction of an integer xcould be a three-valued variable which is −1 whenever x < 0, 0 whenever x=0, and 1 ifx > 1.

Such abstraction is useful when only the sign of x is of importance.Simulation RelationsExample 7.54.503Data Abstraction applied to a Simple Sequential ProgramConsider the following program fragment on the nonnegative integer variables x and y:01234while x > 0 dox := x − 1;y := y + 1;od;if even(y) then return “1” else return “0” fi;...Let PG be the program graph of this program, and TS its underlying transition systemTS(PG). Each state of TS is of the form s = , x = n, y = m, where is a programlocation and m and n are natural numbers.

By means of abstraction one of the variablesmay be completely ignored or the variable domains are restricted. We exemplify the secondkind of abstraction and restrict x and y to the domainsdomabstract (x) = {gzero, zero} anddomabstract (y) = {even, odd}.Stated in words, we only keep track of whether x > 0 or x=0, and whether y is even orodd. The precise values of x and y are not explicitly administered.The abstraction function f which maps a concrete state , x = n, y = m (with m, n ∈ IN)onto an abstract state , x = V, y = W (with V ∈ {gzero, zero} and W ∈ {even, odd}) isdefined as follows:⎧, x = gzero, y = even if x > 0 ∧ y is even⎪⎪⎨, x = gzero, y = oddif x > 0 ∧ y is oddf (, x = v, y = w) =,x=zero,y=evenif x = 0 ∧ y is even⎪⎪⎩, x = zero, y = oddif x = 0 ∧ y is oddTo obtain an abstract transition system TSf with TS , TSf , the operations in TS (e.g.,incrementing y) have to be replaced with corresponding abstract operations that yieldvalues from the abstract domains.

Accordingly, the statement y := y + 1 is replaced withthe abstract operation:even if y = oddy →oddif y = evenThe outcome of the statement x := x − 1 depends on the value of x. In the abstractsetting, the precise value of x is, however, not known. Thus, x := x − 1 corresponds tothe abstract nondeterministic statement:x := gzeroorx := zero504Equivalences and Abstraction(If the guard of the while loop would be x > 1, then there would be no reason fornondeterminism in the abstract program.)The abstract transition system TSf results from the following piece of program:01234while (x = gzero) dox := gzero or x := zero;if y = even then y := odd else y := even fi;od;if y = even then return “1” else return “0” fi;...Note that the abstract program originates from syntactic transformations which can becompletely automated.

The previous considerations show thatR = { (s, f (s)) | s ∈ Loc × Eval(x ∈ IN, y ∈ IN) }is a simulation for (TS, TSf ), provided that the initial values of the abstract variables arechosen in accordance with the initial values of the concrete variables, and the set of atomicpropositions is (a subset of)AP = { 0 , 1 , 2 , 3 , 4 , x > 0, x = 0, even(y), odd(y) }used with the obvious labeling function.If R is a simulation and (s1 , s2 ) ∈ R then each path fragment π1 of s1 can be lifted to apath fragment π2 of s2 such that π1 and π2 are statewise related via R, see Figure 7.22.Lemma 7.55.Simulation on Path FragmentsLet TS1 and TS2 be transition systems over AP, R a simulation for (TS1 , TS2 ), and(s1 , s2 ) ∈ R Then for each (finite or infinite) path fragment π1 = s0,1 s1,1 s2,1 .

. . startingin s0,1 = s1 there exists a path fragment π2 = s0,2 s1,2 s2,2 . . . from state s0,2 = s2 of thesame length such that (sj,1, sj,2 ) ∈ R for all j.Proof: The proof is similar to Lemma 7.5 (page 454).Hence, whenever R is a simulation that contains (s1 , s2 ) and π1 an infinite path from states1 then there exists an infinite path from s2 such that π1 and π2 are statewise R-related.The labeling condition ensures that the traces of π1 and π2 agree. This yields that allinfinite traces of s1 are at the same time infinite traces of s2 .