5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 47
Текст из файла (страница 47)
(Recall the state explosionproblem which appears through parallel composition and the unfolding of program graphsinto transition systems, see page 77 ff.) In the persistence checking algorithm, we mayassume that the elements in Post(s ) are generated on the fly by means of the semanticrules for the transition relation. Ignoring the space required for the syntactic descriptionsof the processes, the additional space requirements for the presented persistence checkingalgorithm is O(N ) for the sets T and R and the stacks U and V , where N is the number ofreachable states in TS. In fact, the representation of T and R is the most (space-)criticalaspect when implementing the nested depth-first search and running it on large examples.Typically, T and R are organized using appropriate hash techniques.
In fact, T and R caneven be represented by a single hash table where the entries are pairs s, b with b ∈ {0, 1}.The meaning of s, 0 is that s is in R, but not in T (i.e., s has been visited in the outer,but not yet in the inner DFS). The pair s, 1 means that s has been visited in both theouter and the inner DFS. The single bit b is sufficient to cover all possible cases, since Tis always a subset of R.7exactly once, if Algorithm 8 does not abort with the answer ”no”.Summary217Another simple observation can speed up the nested depth-first search in case the persistence property is violated: whenever the inner DFS cycle check(s) reaches a state t whichis on the stack U (the DFS stack for the outer DFS), then the upper part of U yields a pathfragment from t to s, while the content of the DFS stack V for the inner DFS describes apath fragment from s to t. Thus, a cycle has been found which visits s infinitely often andthe nested DFS may abort with a counterexample. To support checking whether state tis contained in stack U , a further bit can be added to the entries in the hash table forrepresenting T and R.
I.e., we then have to deal with a hash table for triples s, b, c withs ∈ R and b, c ∈ {0, 1} depending on whether s is in T (in which case b = 1) and whethers is in U (in which case c = 1). This leads to a slight variant of Algorithm 8 which is oftenfaster and generates smaller counterexamples than the original version.4.5Summary• NFAs and DFAs are equivalent automata models for regular languages and can serveto represent the bad prefixes of regular safety properties.• Checking a regular safety property on a finite transition system is solvable by checking an invariant on a product automaton, and thus amounts to solving a reachabilityproblem.• ω-Regular languages are languages of infinite words that can be described by ωregular expressions.• NBAs are acceptors for infinite words.
The syntax is as for NFAs. The acceptedlanguage of an NBA is the set of all infinite words that have a run where an acceptstate is visited infinitely often.• NBAs can serve to represent ω-regular properties.• The class of languages that are recognized by NBAs agrees with the class of ω-regularlanguages.• DBAs are less powerful than NBAs and fail, for instance, to represent the persistenceproperty ”eventually forever a”.• Generalized NBAs are defined as NBAs, except that they require repeated visits forseveral acceptance sets.
Their expressiveness is the same as for NBAs.• Checking an ω-regular property P on a finite transition system TS can be reduced tochecking the persistence property “eventually forever no accept state” in the productof TS and an NBA for the undesired behaviors (i.e., the complement property P ).218Regular Properties• Persistence checking requires checking the existence of a reachable cycle containinga state violating the persistence condition. This is solvable in linear time by a nesteddepth-first search (or by analyzing the strongly connected components).
The sameholds for the nonemptiness problem for NBAs which boils down to checking theexistence of a reachable cycle containing an accept state.• The nested depth-first search approach consists of the interleaving of two depth-firstsearches: one for encountering the reachable states, and one for cycle detection.4.6Bibliographic NotesFinite automata and regular languages. The first papers on finite automata were published in the nineteen fifties by Huffman [217], Mealy [291], and Moore [303] who useddeterministic finite automata for representing sequential circuits. Regula r expressionsand their equivalence to finite automata goes back to Kleene [240]. Rabin and Scott [350]presented various algorithms on finite automata, including the powerset construction.
Theexistence of minimal DFAs relies on results stated by Myhill [309] and Nerode [313]. TheO(N log N ) minimization algorithm we mentioned at the end of Section 4.1 has been suggested by Hopcroft [213]. For other algorithms on finite automata, a detailed descriptionof the techniques sketched here and other aspects of regular languages, we refer to thetext books [272, 363, 214, 383] and the literature mentioned therein.Automata over infinite words.
Research on automata over infinite words (and trees) startedin the nineteen sixties with the work of Büchi [73], Trakhtenbrot [392], and Rabin [351]on decision problems for mathematical logics. At the same time, Muller [307] studieda special type of deterministic ω-automata (today called Muller automata) in the context of asynchronous circuits. The equivalence of nondeterministic Büchi automata andω-regular expressions has been shown by McNaughton [290]. He also established a link between NBAs and deterministic Muller automata [307] by introducing another acceptancecondition that has been later formalized by Rabin [351]. (The resulting ω-automata type istoday called Rabin automata.) An alternative transformation from NBA to deterministicRabin automata has been presented by Safra [361].
Unlike Büchi automata, the nondeterministic and deterministic versions of Muller and Rabin automata are equally expressiveand yield automata-characterizations of ω-regular languages. The same holds for severalother types of ω-automata that have been introduced later, e.g., Streett automata [382]or automata with the parity condition [305].The fact that ω-regular languages are closed under complementation (we stated this resultwithout proof) can be derived easily from deterministic automata representations. Theproof of Theorem 4.50 follows the presentation given in the book by Peled [327]. VariousExercises219decision problems for ω-automata have been addressed by Landweber [261] and later byEmerson and Lei [143] and Sistla, Vardi, and Wolper [373].
For a survey of automata oninfinite words, transformations between the several classes of ω-automata, complementation operators and other algorithms on ω-automata, we refer to the articles by Choueka[81], Kaminsky [229], Staiger [376], and Thomas [390, 391]. An excellent overview of themain concepts of and recent results on ω-automata is provided by the tutorial proceedings[174].Automata and linear-time properties.
The use of Büchi automata for the representationand verification of linear-time properties goes back to Vardi and Wolper [411, 412] whostudied the connection of Büchi automata with linear temporal logic. Approaches withsimilar automata models have been developed independently by Lichtenstein, Pnueli, andZuck [274] and Kurshan [250]. The verification of (regular) safety properties has beendescribed by Kupferman and Vardi [249]. The notion of persistence property has beenintroduced by Manna and Pnueli [282] who provided a hierarchy of temporal properties.The nested depth-first algorithm (see Algorithm 8) originates from Courcoubetis et al.
[102]and its implementation in the model checker SPIN has been reported by Holzmann, Peled,and Yannakakis [212]. The Murϕ verifier developed by Dill [132] focuses on verifyingsafety properties. Variants of the nested depth-first search have been proposed by severalauthors, see, e.g., [106, 368, 161, 163].
Approaches that treat generalized Büchi conditions(i.e., conjunctions of Büchi conditions) are discussed in [102, 388, 184, 107]. Furtherimplementation details of the nested depth-first search approach can be found in the bookby Holzman [209].4.7ExercisesExercise 4.1. Let AP = { a, b, c }. Consider the following LT properties:(a) If a becomes valid, afterward b stays valid ad infinitum or until c holds.(b) Between two neighboring occurrences of a, b always holds.(c) Between two neighboring occurrences of a, b occurs more often than c.(d) a ∧ ¬b and b ∧ ¬a are valid in alternation or until c becomes valid.For each property Pi (1 i 4), decide if it is a regular safety property (justify your answers) andif so, define the NFA Ai with L(Ai ) = BadPref(Pi ).
(Hint: You may use propositional formulaeover the set AP as transition labels.)220Regular PropertiesExercise 4.2. Let n 1. Consider the language Ln ⊆ Σ∗ over the alphabet Σ = { A, B } thatconsists of all finite words where the symbol B is on position n from the right, i.e., L containsexactly the words A1 A2 . . . Ak ∈ {A, B}∗ where k n and Ak−n+1 = B. For instance, the wordABBAABAB is in L3 .(a) Construct an NFA An with at most n+1 states such that L(An ) = Ln .(b) Determinize this NFA An using the powerset construction algorithm.Exercise 4.3. Consider the transition system TSSem for the two-process mutual exclusion witha semaphore (see Example 2.24 on page 43) and TSPet for Peterson’s algorithm (see Example 2.25on page 45).(a) Let Psafe be the regular safety property “process 1 never enters its critical section from itsnoncritical section (i.e., process 1 must be in its waiting location before entering the criticalsection)” and AP = { wait1 , crit1 }.(i) Depict an NFA for the minimal bad prefixes for Psafe .(ii) Apply the algorithm in Section 4.2 to verify TSSem |= Psafe .(b) Let Psafe be the safety property “process 1 never enters its critical section from a state wherex = 2” and AP = { crit1 , x = 2 }.(i) Depict an NFA for the minimal bad prefixes for Psafe .(ii) Apply the algorithm in Section 4.2 to verify TSPet |= Psafe .
Which counterexample isreturned by the algorithm?Exercise 4.4. Let Psafe be a safety property. Prove or disprove the following statements:(a) If L is a regular language with MinBadPref(Psafe ) ⊆ L ⊆ BadPref(Psafe ), then Psafe isregular.(b) If Psafe is regular, then any L for which MinBadPref(Psafe ) ⊆ L ⊆ BadPref(Psafe ) is regular.Exercise 4.5.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
