5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 34
Текст из файла (страница 34)
. . , Ak , A1 , . . . , Al ⊆ Act.(a) Let F be the fairness assumption F = (∅, Fstrong , Fweak ) whereFstrong = {A1 , . . . , Ak } and Fweak = {A1 , . . . , Al }.Provide a sketch of a scheduling algorithm that resolves the nondeterminism in TS in anF -fair way.(b) Let Fucond = {A1 , . . . , Ak }, viewed as an unconditional fairness assumption for TS. Designa (scheduling) algorithm that checks whether Fucond for TS is realizable, and if so, generatesan Fucond -fair execution for TS.Chapter 4Regular PropertiesThis chapter treats some elementary algorithms to verify important classes of safety properties, liveness properties, and a wide range of other linear-time properties. We firstconsider regular safety properties, i.e., safety properties whose bad prefixes constitute aregular language, and hence can be recognized by a finite automaton.
The algorithm tocheck a safety property Psafe for a given finite transition system TS relies on a reductionto the invariant-checking problem in a certain product construction of TS with a finiteautomaton that recognizes the bad prefixes of Psafe .We then generalize this automaton-based verification algorithm to a larger class of lineartime properties, the so-called ω-regular properties. This class of properties covers regularsafety properties, but also many other relevant properties such as various liveness properties. ω-regular properties can be represented by so-called Büchi automata, a variant offinite automata that accept infinite (rather than finite) words. Büchi automata will be thekey concept to verify ω-regular properties via a reduction to persistence checking.
Thelatter is a variant of invariant checking and aims to show that a certain state-conditionholds continuously from some moment on.4.1Automata on Finite WordsDefinition 4.1.Nondeterministic Finite Automaton (NFA)A nondeterministic finite automaton (NFA) A is a tuple A = (Q, Σ, δ, Q0 , F ) where151152Regular Properties• Q is a finite set of states,• Σ is an alphabet,• δ : Q × Σ → 2Q is a transition function,• Q0 ⊆ Q is a set of initial states, and• F ⊆ Q is a set of accept (or: final) states.The size of A, denoted |A|, is the number of states and transitions in A, i.e.,|δ(q, A)|.|A| = |Q| +q∈Q A∈ΣΣ defines the symbols on which the automaton is defined.
The (possibly empty) set Q0defines the states in which the automaton may start. The transition function δ can beidentified with the relation → ⊆ Q × Σ × Q given byA → q iff q ∈ δ(q, A).q −−Thus, often the notion of transition relation (rather than transition function) is used forA → q denotes that the automaton can move from state q to state q whenδ. Intuitively, q −−reading the input symbol A.Example 4.2.An Example of a Finite-State AutomatonAn example of an NFA is depicted in Figure 4.1. Here, Q = { q0 , q1 , q2 }, Σ = { A, B },Q0 = { q0 }, F = { q2 }, and the transition function δ is defined byδ(q0 , A) = { q0 }δ(q1 , A) = { q2 }δ(q2 , A) = ∅δ(q0 , B) = { q0 , q1 }δ(q1 , B) = { q2 }δ(q2 , B) = ∅ABBAB→ q0 , q0 −−→ q0 , q0 −−→ q1 , q1 −−→ q2 , and q1 −−→ q2 .This corresponds to the transitions q0 −−The drawing conventions for an NFA are the same as for labeled transition systems.
Acceptstates are distinguished from other states by drawing them with a double circle.The intuitive operational behavior of an NFA is as follows. The automaton starts in oneof the states in Q0 , and then is fed with an input word w ∈ Σ∗ . The automaton reads thisAutomata on Finite Words153AAq0Bq1q2BBFigure 4.1: An example of a finite-state automaton.word character by character from the left to the right. (The reader may assume that theinput word is provided on a tape from which the automaton reads the input symbols fromthe left to the right by moving a cursor from the current position i to the next positioni+1 when reading the ith input symbol.
However, the automaton can neither write on thetape nor move the cursor in another way than one position to the right.) After reading aninput symbol, the automaton changes its state according to the transition relation δ. Thatis, if the current input symbol A is read in the state q, the automaton chooses one of theA → q (i.e., one state q ∈ δ(q, A)) and moves to q where the nextpossible transitions q −−input symbol will be consumed. If δ(q, A) contains two or more states, then the decisionfor the next state is made nondeterministically. An NFA cannot perform any transitionwhen its current state q does not have an outgoing transition that is labeled with thecurrent input symbol A.
In that case, i.e., if δ(q, A) = ∅, the automaton is stuck and nofurther progress can be made. The input word is said to be rejected. When the completeinput word has been read, the automaton halts. It accepts whenever the current state isan accept state, and it rejects otherwise.This intuitive explanation of the possible behaviors of an NFA for a given input wordw = A1 . . .
An is formalized by means of runs for w (see Definition 4.3 below). For anyinput word w there might be several possible behaviors (runs); some of them might beaccepting, some of them might be rejecting. Word w is accepted by A if at least one ofits runs is accepting, i.e., succeeds in reading the whole word and ends in a final state.This relies on the typical nondeterministic acceptor criterion which assumes an oraclefor resolving the nondeterminism such that, whenever possible, an accepting run will begenerated.Definition 4.3.Runs, Accepted Language of an NFALet A = (Q, Σ, δ, Q0 , F ) be an NFA and w = A1 . .
. An ∈ Σ∗ a finite word. A run for w inA is a finite sequence of states q0 q1 . . . qn such that• q0 ∈ Q0 and154Regular PropertiesAi+1• qi −−−−→ qi+1 for all 0 i < n.Run q0 q1 . . . qn is called accepting if qn ∈ F . A finite word w ∈ Σ∗ is called accepted byA if there exists an accepting run for w. The accepted language of A, denoted L(A), isthe set of finite words in Σ∗ accepted by A, i.e.,L(A) = {w ∈ Σ∗ | there exists an accepting run for w in A }.Example 4.4.Runs and Accepted WordsExample runs of the automaton A in Figure 4.1 are q0 for the empty word ε, q0 q1 forthe word consisting of the symbol B, q0 q0 q0 q0 for, e.g., the words ABA and BBA andq0 q1 q2 for the words BA, and BB.
Accepting runs are runs that finish in the final stateq2 . For instance, the runs q0 q1 q2 for BA and BB and q0 q0 q1 q2 for the words ABB, ABA,BBA, and BBB are accepting. Thus, these words belong to L(A). The word AAA is notaccepted by A since it only has single run, namely q0 q0 q0 q0 , which is not accepting.The accepted language L(A) is given by the regular expression (A + B)∗ B(A + B). Thus,L(A) is the set of words over { A, B } where the last but one symbol is B.The special cases Q0 = ∅ or F = ∅ are allowed. In both cases, L(A) = ∅.
If F = ∅,then there are no accepting runs. If there are no initial states, then there are no runs atall. Intuitively, the automaton rejects any input word immediately.An equivalent alternative characterization of the accepted language of an NFA A is asfollows. Let A be an NFA as above. We extend the transition function δ to the functionδ ∗ : Q × Σ∗ → 2Q as follows: δ∗ (q, ε) = { q }, δ∗ (q, A) = δ(q, A), andδ∗ (p, A2 .
. . An ).δ∗ (q, A1 A2 . . . An ) =p∈δ(q,A1 )∗ (q, w) is the set of states that are reachable from q for the input wordStated in words, δw. In particular, q0 ∈Q0 δ∗ (q0 , w) is the set of all states where a run for w in A can end.If one of these states is final, then w has an accepting run. Vice versa, if w ∈/ L(A), thennone of these states is final. Hence, we have the following alternative characterization ofthe accepted language of an NFA by means of the extended transition function δ∗ :Automata on Finite WordsLemma 4.5.155Alternative Characterization of the Accepted LanguageLet A be an NFA. Then:L(A) = {w ∈ Σ∗ | δ∗ (q0 , w) ∩ F = ∅ for some q0 ∈ Q0 }.It can be shown that the language accepted by an NFA constitutes a regular language.In fact, there are algorithms that for a given NFA A generate a regular expression forthe language L(A).
Vice versa, for any regular expression E, an NFA can be constructedthat accepts L(E). Hence, the class of regular languages agrees with the class of languagesaccepted by an NFA.An example of a language that is nonregular (but context-free) is { An Bn | n 0 }. Theredoes not exist an NFA that accepts it. The intuitive argument for this is that one needsto be able to count the number of A’s so as to be able to determine the number of B’sthat are to follow.Since NFAs serve to represent (regular) languages we may identify those NFA that acceptthe same language:Definition 4.6.Equivalence of NFAsLet A and A be NFAs with the same alphabet. A and A are called equivalent ifL(A) = L(A ).A fundamental issue in automata theory is to decide for a given NFA A whether itsaccepted language is empty, i.e., whether L(A) = ∅.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
