5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 75
Текст из файла (страница 75)
(Techniques for otheroperators, such as W or R , can be derived. Alternatively, corresponding considerationscan be made for them.)In the sequel, let TS = (S, Act, →, I, AP, L) be a finite transition system without terminalstates.Counterexamples and Witnesses377The Next Operator A counterexample of ϕ = Φ is a pair of states (s, s ) with s ∈ Iand s ∈ Post(s) such that s |= Φ. A witness of ϕ = Φ is a pair of states (s, s ) withs ∈ I and s ∈ Post(s) with s |= Φ. Thus, counterexamples and witnesses for the next-stepoperator result from inspecting the immediate successors of the initial states of TS.The Until Operator A witness of ϕ = Φ U Ψ is an initial path fragment s0 s1 . .
. sn forwhichsn |= Ψ and si |= Φ for 0 i < n.Witnesses can be determined by a backward search starting in the set of Ψ-states.A counterexample is an initial path fragment that indicates a path π for which either:π |= (Φ ∧ ¬Ψ) or π |= (Φ ∧ ¬Ψ) U (¬Φ ∧ ¬Ψ).For the first case, a counterexample is an initial path fragment of the forms0 s1 . . .
sn−1 sn s1 . . . sr cyclesatisfy Φ ∧ ¬Ψwith sn = sr .For the second case, an initial path fragment of the forms0 s1 . . . sn−1 snwith sn |= ¬Φ ∧ ¬Ψsatisfy Φ ∧ ¬Ψdoes suffice as counterexample. Counterexamples can be determined by an analysis of thedigraph G = (S, E) whereE = { (s, s ) ∈ S × S | s ∈ Post(s) ∧ s |= Φ ∧ ¬Ψ }.Then the SCCs of G are determined.
Each path in G that starts in an initial state s0 ∈ Sand leads to a nontrivial SCC C in G provides a counterexample of the forms0 s1 . . . sn s1 . . . sr withsn = sr .∈CEach path in G that leads from an initial state s0 to a trivial terminal SCCC = { s } withs |= Ψprovides a counterexample of the form s0 s1 . . . sn with sn |= ¬Φ ∧ ¬Ψ.378Computation Tree Logicn1 , n2 , y=1w1 , n2 , y=1n1 , w2 , y=1c1 , n2 , y=0w1 , w2 , y=1n1 , c2 , y=0c1 , w2 , y=0w1 , c2 , y=0Figure 6.18: Transition system of semaphore-based mutual exclusion algorithm.The Always Operator A counterexample for the formula ϕ = Φ is an initial pathfragment s0 s1 . . . sn such that si |= Φ for 0 i < n and sn |= Φ.
Counterexamples maybe determined by a backward search starting in ¬Φ-states.A witness of ϕ = Φ consists of an initial path fragment of the forms0 s1 . . . sn s1 . . . srwithsn = sr .satisfy ΦWitnesses can be determined by a simple cycle search in the digraph G = (S, E) wherethe set of edges E is obtained from the transitions emanating from Φ-states, i.e., E ={ (s, s ) | s ∈ Post(s) ∧ s |= Φ }.Example 6.45.Counterexamples and Semaphore-Based Mutual ExclusionRecall the two-process mutual exclusion algorithm that exploits a binary semaphore y toresolve contention (see Eaxmple 3.9 on page 98).
For convenience, the transition systemTSSem of this algorithm is depicted in Figure 6.18. Consider the CTL formula over AP ={ c1 , c2 , n1 , n2 , w1 , w2 }:∀(((n1 ∧ n2 ) ∨ w2 ) U c2 ). ΦΨIt expresses that process P2 acquires access to the critical section once it starts waiting toenter it.Note that the state labeling of TSSem can be directly obtained from the information inCounterexamples and Witnesses379n1 , n2 , y=1w1 , n2 , y=1c1 , n2 , y=0n1 , w2 , y=1w1 , w2 , y=1n1 , c2 , y=0c1 , w2 , y=0w1 , c2 , y=0Figure 6.19: Graph to detect counterexamples for ∀(((n1 ∧ n2 ) ∨ w2 ) U c2 ).the states. Evidently, the CTL formula is refuted by TSSem .
Counterexamples can beestablished as follows. First, the graph G is determined by only allowing edges thatemanate from states satisfying Φ ∧ ¬Ψ. This entails that all edges emanating from s withs |= ¬((n1 ∧ n2 ) ∨ w2 ) ∨ c2 are eliminated. This yields the graph depicted in Figure 6.19.The graph G contains a single nontrivial SCC C that is reachable from the initial state inTSSem . The initial path fragment:n1 , n2 , y=1 n1 , w2 , y=1 w1 , w2 , y=1 c1 , w2 , y=0∈ Cis a counterexample as it shows that there is a path π in TSSem satisfying (((n1 ∧ n2 ) ∨w2 ) ∧ ¬c2 ), i.e., a path for which c2 is never established.Alternatively, any path from the initial state to the trivial terminal SCC satisfying ¬c2 isa counterexample as well. This only holds for the terminal SCC { w1 , n2 , y=1 }.Theorem 6.46.Time Complexity of Counterexample GenerationLet TS be a transition system TS with N states and K transitions and ϕ a CTL- pathformula.
If TS |= ∀ϕ, then a counterexample for ϕ in TS can be determined in timeO(N +K). The same holds for a witness for ϕ, provided that TS |= ∃ϕ.3806.6.2Computation Tree LogicCounterexamples and Witnesses in CTL with FairnessIn the case CTL fairness assumptions are imposed, witnesses and counterexamples can beprovided in a similar way as for CTL. Suppose fair is the fairness assumption of interest.The Next Operator A witness for π |=fair a originates from a witness for π |= (a ∧ afair ). Note that the latter is obtained as for CTL, as no fairness is involved. Acounterexample to a is a prefix of a fair path π = s0 s1 s2 . .
. in TS with π |= a. Asπ is fair and π |= a, it follows that s1 |= afair and s1 |= a. So, s1 |= afair → a. Acounterexample to a with respect to |=fair thus results from a counterexample to theformula (afair → a) for CTL without fairness.The Until Operator A witness of a U a with respect to the fair semantics is a witnessof a U (a ∧ afair ) with respect to the standard CTL semantics. A counterexample for a U awith respect to the fair semantics is either a witness of (a ∧ a ) U (¬a ∧ ¬a ∧ afair ) underthe common semantics |= or a witness of (a ∧ ¬a ) with respect to the fair semantics(explained below).The Always Operator For a formula of the form a, a counterexample with respectto the fair semantics is an initial path fragment s0 s1 .
. . sn such that:sn |= ¬a ∧ afairand si |= a for 0 i < n.Consider the strong fairness assumption of the form:( ♦ ai → ♦ bi ).sfair =0<ikA witness of a under sfair is an initial path fragments0 s1 . . . sn s1 s2 . . . srwith sn = sr|= asuch that for all 0 < i k it holds thatSat(ai ) ∩ { s1 , . . . , sr } = ∅ or Sat(bi ) ∩ { s1 , . .
. , sr } = ∅.A witness can be computed by means of an analysis of the SCCs of a digraph that originatesfrom the state graph of TS after some slight modifications. The costs are (multiplicatively)linear in the number of fairness conditions and in the size of the state graph.Symbolic CTL Model CheckingTheorem 6.47.381Time Complexity of Fair Counterexample GenerationFor transition system TS with N states and K transitions, CTL path formula ϕ and CTLfairness assumption fair with k conjuncts such that TS |=fair ∀ϕ, a counterexample forϕ in TS can be determined in time O((N +K)·k). The same holds for a witness for ϕ ifTS |= ∃ϕ.Example 6.48.Consider the transition system depicted in Figure 6.11 (page 350) and assume the formulaof interest is:∃ (a ∨ (b = c))under fairness constraintsfair = ♦ (q ∧ r) → ♦ ¬(q ∨ r).The strong CTL fairness constraint asserts that in case either state s0 or s2 is visitedinfinitely often, then also state s3 or s7 needs to be visited infinitely often.
The paths1 s3 s0 s2 s0 is a witness of ∃ (a ∨ (b = c)) in the absence of any fairness constraint. Itis, however, no witness under sfair as it visits s0 (and s2 ) infinitely often, but not s3 ors7 . On the other hand, the path s1 s3 s0 s2 s1 is a witness under sfair .6.7Symbolic CTL Model CheckingThe CTL model-checking procedure described so far relies on the assumption that thetransition system has an explicit representation by the predecessor and successor lists perstate.
Such an enumerative representation is not adequate for very large transition systems. To attack the state explosion problem, the CTL model-checking procedure can bereformulated in a symbolic way where sets of states and sets of transitions are representedrather than single states and transitions. This set-based approach is very natural for CTL,since its semantics and model-checking algorithm rely on satisfaction sets for subformulae.There are several possibilities to realize the CTL model checking algorithm in a purelyset-based stetting.
The most prominent ones rely on a binary encoding of the states, whichpermits identifying subsets of the state space and the transition relation with switchingfunctions. To obtain compact representations of switching functions, special data structures have been developed, such as ordered binary decision diagrams. Other forms for therepresentation of switching functions, such as conjunctive normal forms, could be used aswell. They are widely used in the context of so-called SAT-based model checking where themodel-checking problem is reduced to the satisfiability problem for propositional formulae(SAT).
The SAT-based techniques will not be described in this book. Instead we willexplain the main ideas of the approach with binary decision diagrams.382Computation Tree LogicWe first explain the general ideas behind symbolic approaches which operate on sets ofstates rather than single states and rely on a representation of transition systems byswitching functions. In the sequel, let TS = (S, →, I, AP, L) be a “large”, but finitetransition system. The set of actions is irrelevant here and has been skipped. That is,the transition relation → is a subset of S × S. Let n %log |S|&. (Since we supposea large transition system, we can safely assume that |S| 2.) We choose an arbitrary(injective) encoding enc : S → {0, 1}n of the states by bit vectors of length n.
Althoughenc might not be surjective, it is no restriction to suppose that enc(S) = {0, 1}n , since allelements (b1 , . . . , bn ) ∈ {0, 1}n \ enc(S) can be treated as the encoding of pseudo statesthat cannot be reached from any proper state s ∈ S. The transitions of these pseudostates are arbitrary. The idea is now to identify the states s ∈ S = enc−1 ({0, 1}n ) withtheir encoding enc(s) ∈ {0, 1}n and to represent any subset T of S by its characteristicfunction χT : {0, 1}n → {0, 1}, which evaluates to true exactly for the (encodings of the)states s ∈ T . Similarly, the transition relation → ⊆ S × S can be represented by a Booleanfunction Δ : {0, 1}2n → {0, 1} that assigns 1 to exactly those pairs (s, s ) of bit vectors oflength n each where s → s .On the basis of this encoding, the CTL model-checking procedure can be reformulated toan algorithm that operates on the representation of TS by binary decision diagrams for Δand the characteristic functions χSat(a) for the satisfaction sets of the atomic propositionsa ∈ AP.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
