5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 35
Текст из файла (страница 35)
This is known as the emptinessproblem. From the acceptance condition, it follows directly that L(A) is nonempty if andonly if there is at least one run that ends in some final state. Thus, nonemptiness of L(A)is equivalent to the existence of an accept state q ∈ F which is reachable from an initialstate q0 ∈ Q0 . This can easily be determined in time O(|A|) using a depth-first searchtraversal that encounters all states that are reachable from the initialstates and checkswhether one of them is final.
For state q ∈ Q, let Reach(q) = w∈Σ∗ δ∗ (q, w); that is,Reach(q) is the set of states q that are reachable via an arbitrary run starting in state q.Theorem 4.7.Language Emptiness is Equivalent to ReachabilityLet A = (Q, Σ, δ, Q0 , F ) be an NFA.
Then, L(A) = ∅ if and only if there exists q0 ∈ Q0and q ∈ F such that q ∈ Reach(q0 ).156Regular PropertiesRegular languages exhibit some interesting closure properties, e.g., the union of two regular languages is regular. The same applies to concatenation and Kleene star (finiterepetition). This is immediate from the definition of regular languages as those languagesthat can be generated by regular expressions. They are also closed under intersection andcomplementation, i.e., if L, L1 , L2 are regular languages over the alphabet Σ, then so areL = Σ∗ \ L and L1 ∩ L2 .Let us briefly sketch the proofs for this. In both cases, we may proceed on the basis offinite automata and assume a representation of the given regular languages by NFA A,A1 , and A2 with the input alphabet Σ that accept the regular languages L, L1 , and L2 ,respectively. Intersection can be realized by a product construction A1 ⊗ A2 which canbe viewed as a parallel composition with synchronization over all symbols A ∈ Σ.
Infact, the formal definition of ⊗ is roughly the same as the synchronization operator ; seeDefinition 2.26 on page 48. The idea is simply that for the given input word, we run thetwo automata in parallel and reject as soon as one automaton cannot read the currentinput symbol, but accept if the input word is fully consumed and both automata accept(i.e., are in a final state).Definition 4.8.Synchronous Product of NFAsFor NFA Ai = (Qi , Σ, δi , Q0,i , Fi ), with i=1, 2, the product automatonA1 ⊗ A2 = (Q1 × Q2 , Σ, δ, Q0,1 × Q0,2 , F1 × F2 )where δ is defined byAA→1 q1 ∧ q2 −−→2 q2q1 −−A(q1 , q2 ) −−→ (q1 , q2 ).It follows that this product construction of automata corresponds indeed to the intersectionof their accepting languages, i.e., L(A1 ⊗ A2 ) = L(A1 ) ∩ L(A2 ).Let us now consider the complementation operator.
Given an NFA A with the inputalphabet Σ, we aim to construct an NFA for the complement language Σ∗ \ L(A). Themain step to do so is first to construct an equivalent deterministic finite automaton Adetwhich can be complemented in a quite simple way.Definition 4.9.Deterministic Finite Automaton (DFA)Let A = (Q, Σ, δ, Q0 , F ) be an NFA. A is called deterministic if |Q0 | 1 and |δ(q, A)| 1for all states q ∈ Q and all symbols A ∈ Σ. We will use the abbreviation DFA for adeterministic finite automaton.Automata on Finite Words157DFA A is called total if |Q0 | = 1 and |δ(q, A)| = 1 for all q ∈ Q and all A ∈ Σ.Stated in words, an NFA is deterministic if it has at most a single initial state and if for eachsymbol A the successor state of each state q is either uniquely defined (if |δ(q, A)| = 1) orundefined (if δ(q, A) = ∅).
Total DFAs provide unique successor states, and thus, uniqueruns for each input word. Any DFA can be turned into an equivalent total DFA by simplyadding a nonfinal trap state, qtrap say, that is equipped with a self-loop for any symbolA ∈ Σ. From any state q = qtrap , there is a transition to qtrap for any symbol A for whichq has no A-successor in the given nontotal DFA.Total DFA are often written in the form A = (Q, Σ, δ, q0 , F ) where q0 stands for the uniqueinitial state and δ is a (total) transition function δ : Q × Σ → Q.
Also, the extendedtransition function δ ∗ of a total DFA can be viewed as a total function δ∗ : Q × Σ∗ → Q,which for given state q and finite word w returns the unique state p = δ∗ (q, w) that isreached from state q for the input word w. In particular, the accepted language of a totalDFA A = (Q, Σ, δ, q0 , F ) is given byL(A) = {w ∈ Σ∗ | δ∗ (q0 , w) ∈ F }.The observation that total DFAs have exactly one run for each input word allows complementing a total DFA A by simply declaring all states to be final that are nonfinal in A andvice versa. Formally, if A = (Q, Σ, δ, q0 , F ) is a total DFA then A = (Q, Σ, δ, q0 , Q \ F ) isa total DFA with L(A) = Σ∗ \ L(A). Note that the operator A → A applied to a nontotalDFA (or NFA with proper nondeterministic choices) fails to provide an automaton for thecomplement language (why?).It remains to explain how to construct for a given NFA A = (Q, Σ, δ, Q0 , F ) an equivalenttotal DFA Adet .
This can be done by a powerset construction, also often called a subsetconstruction, since the states of Adet are the subsets of Q. This allows Adet to simulateA by moving the prefixes A1 . . . Ai of the given input word w = A1 . . . An ∈ Σ to theset of states that are reachable in A for A1 . . .
Ai . That is, Adet starts in Q0 , the setis a subset of A’s state space Q),of initial states in A. If Adet is in state Q (whichthen Adet moves the input symbol A to Q = q∈Q δ(q, A). If the input word has beenconsumed and Adet is in a state Q that contains a state in A’s set of accept states, thenAdet accepts. The latter means that there exists an accepting run in A for the given inputword w that ends in an accept state, and hence, w ∈ L(A). The formal definition of Adetis Adet = (2Q , Σ, δdet , Q0 , Fdet ) whereFdet = {Q ⊆ Q | Q ∩ F = ∅}and where the total transition function δdet : 2Q × Σ → 2Q is defined byδ(q, A).δdet (Q , A) =q∈Q158Regular PropertiesClearly, Adet is a total DFA and, for all finite words w ∈ Σ∗ , we have∗δdet(Q0 , w) =δ∗ (q0 , w).q0 ∈Q0Thus, by Lemma 4.5, L(Adet ) = L(A).Example 4.10.Determinizing a Nondeterministic Finite AutomatonConsider the NFA depicted in Figure 4.1 on page 153.
This automaton is not deterministicas on input symbol B in state q0 the next state is not uniquely determined. The totalDFA that is obtained through the powerset construction is depicted in Figure 4.2.AB{ q0 }{ q0 , q1 }BABA{ q0 , q2 }A{ q0 , q1 , q2 }BFigure 4.2: A DFA accepting L((A + B)∗ B(A + B)).The powerset construction yields a total DFA that is exponentially larger than the original NFA. In fact, although DFAs and NFAs have the same power (both are equivalentformalisms for regular languages), NFAs can be much more efficient. The regular languagegiven by the regular expression Ek = (A + B)∗ B(A + B)k (where k is a natural number)is accepted by an NFA with k+2 states (namely?), but it can be shown that there is noequivalent DFA with less than 2k states.
The intuitive argument for the latter is that eachDFA for L(Ek ) needs to “remember” the positions of the symbol B among the last k inputsymbols which yields Ω(2k ) states.We finally mention that for any regular language L there is a unique DFA A with L = L(A)where the number of states is minimal under all DFAs for L. Uniqueness is understoodup to isomorphism, i.e., renaming of the states. (This does not hold for NFA. Why?)There is an algorithm to minimize a given DFA with N states into its equivalent minimalDFA which is based on partition refinement and takes O(N · log N ) time in the worst case.The concepts of this minimization algorithm are outside the scope of this monograph andcan be found in any textbook on automata theory.
However, in Chapter 7 a very similarpartitioning-refinement algorithm will be presented for bisimulation minimization.Model-Checking Regular Safety Properties4.2159Model-Checking Regular Safety PropertiesIn this section, it will be shown how NFAs can be used to check the validity of an importantclass of safety properties. The main characteristic of these safety properties is that all theirbad prefixes constitute a regular language. The bad prefixes of these so-called regularsafety properties can thus be recognized by an NFA.
The main result of this section isthat checking a regular safety property on a finite transition system can be reduced toinvariant checking on the product of TS and an NFA A for the bad prefixes. Stateddifferently, if one wants to check whether a regular safety property holds for TS, it sufficesto perform a reachability analysis in the product TS⊗A to check a corresponding invarianton TS ⊗ A.4.2.1Regular Safety PropertiesRecall that safety properties are LT properties, i.e., sets of infinite words over 2AP , suchthat every trace that violates a safety property has a bad prefix that causes a refutation(cf.
Definition 3.22 on page 112). Bad prefixes are finite, and thus the set of bad prefixesconstitutes a language of finite words over the alphabet Σ = 2AP . That is, the inputsymbols A ∈ Σ of the NFA are now sets of atomic propositions. For instance, if AP ={ a, b }, then Σ = { A1 , A2 , A3 , A4 } consists of the four input symbols A1 = {}, A2 = { a },A3 = { b }, and A4 = { a, b }.1Definition 4.11.Regular Safety PropertySafety property Psafe over AP is called regular if its set of bad prefixes constitutes a regularlanguage over 2AP .Every invariant is a regular safety property. If Φ is the state condition (propositionalformula) of the invariant that should be satisfied by all reachable states, then the languageof bad prefixes consists of the words A0 A1 .
. . An such that Ai |= Φ for some 0 i n.Such languages are regular, since they can be characterized by the (casually written)regular notationΦ∗ (¬ Φ) true∗ .Here, Φ stands for the set of all A ⊆ AP with A |= Φ, ¬Φ for the set of all A ⊆ AP withA |= Φ, while true means the set of all subsets A of AP. For instance, if AP = { a, b } andΦ = a ∨ ¬b, thenThe symbol {} denotes the empty subset of AP which serves as symbol in the alphabet Σ = 2AP .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
