IA159 Formal Verification Methods Lecture Notes Version: April 18, 2010 Syllabus * Models of systems * Formal specification of program properties (modal and temporal logics) * Automatic verification - reachability analysis, symbolic and explicit model checking, equivalence checking * Deductive verification methods (theorem proving) * Software testing * Program analysis, abstraction, abstract interpretation * Counter-example guided abstraction refinement * Combining formal methods, SW tools BLAST, Spec# etc. 1 Basic information about the course 1.1 What does "Formal Verification Methods" mean? formal methods are a collection of notations and techniques for describing and analyzing systems. Methods are formal in the sense that they are based on some mathematical theories, such as logic, automata or graph theory. [Pel01] verification is the process of applying a manual or an automatic technique that is supposed to establish whether the code either satisfies a given property or behaves in accordance with some higher-level description of it. [Pel01] formal verificatin methods are techniques (usually based on mathematical theories) for analysing systems with the aim to improve their quality and reliability. The course is focused on theoretical and algorithmic bases of verification methods. The software engineering aspects connected to verification methods are beyond the scope of this course. 1.2 Literature There is no single reading material covering all the topics mentioned in this course. However, many these topics are covered by the books [Pel01] and [CGP99]. Recommended reading material for the other topics are some recent papers that will be referred in this text. 1.3 Connections to other courses In the course, we assume that students are familiar with the content of the following courses (in particular with the mentioned notions). * IB005 Formal Languages and Automata I (aka FJA I) - pushdown automata * IA006 Selected topics on automata theory (aka FJA II) - infinite words, B¨uchi automata, bisimulation equivalence * IA040 Modal and Temporal Logics for Processes - temporal logics, mainly LTL 1 ˇ IV113 Introduction to Validation and Verification - automata based LTL model checking Courses that are also relevant to our topic: * MA015 Graph Algorithms * IV010 Communication and Parallelism * IB002 Design of Algorithms I * IV022 Design and Verification of Algorithms * PA008 Compiler Construction Courses following (is some sense) our course: * IV115 Parallel and Distributed Laboratory Seminar * IV074 Laboratory for Parallel and Distributed Systems * IA072 Seminar on Concurrency 1.4 Examination There will be an oral exam at the end (no intrasemestral tests, no written exams, no homeworks). 2 Introduction Verification methods can be loosely divided into the following basic cathegories: * testing ­ simple, feasible, very good cost/performance ratio ­ very effective in early stages of debugging process ­ applicable directly to real systems ­ cannot guarantee that there are no errors ­ in practice: standard technique for enhancing the quality of systems, wide tool support * deductive verification (with use of theorem provers) ­ applicable to models of real systems ­ needs a huge effort of an expert on both deductive verification and systems under verification ­ can guarantee that (a model of) a real system satisfies a given property ­ in practice: used rarely (e.g. partial correctness of FPU in AMD processors) * equivalence checking ­ applicable to models of real systems ­ needs a detailed formal specification of a system under verification ­ there are no algorithms for reasonable equivalences and infinite-state sys- tems ­ in practice: some specific applications (e.g. equivalence of different levels of hardware design) * reachability and model checking ­ applicable to (usually finite-state) models of real systems 2 ­ needs formal specification of a system under verification ­ fully automatic, but feasible only for relatively small finite-state systems ­ in practice: a standard technique for verification of simple hardware designs, used also for verification of small systems (e.g. communication pro- tocols) * static analysis and abstract interpretation ­ applicable directly to source code of real systems, feasible ­ can verify only a specific class of properties (including many interesting properties) ­ may produce false alarms (the number of false alarms grows with the ability to find real bugs) ­ automatic (verification of some properties may require provision of a suitable abstraction) ­ in practice: some static analysis is performed by almost every compiler, there are very efficient tools (e.g. Coverity, Stanse) able to work with big pieces of real software, for example a linux kernel * combined methods ­ e.g. abstraction + model checking, model checking + counter-example guided abstraction refinement (CEGAR), abstract interpretation + counterexample guided abstraction refinement (CEGAR), testing + model checking, testing + symbolic execution (a case of abstract interpretation) ­ the aim is to develop methods which are applicable directly to (source code of) real systems and (more or less) automatic ­ may be incomplete and/or produce false alarms ­ in practice: already has some specific applications, e.g. verification of Windows drivers (by Static Driver Verifier [SDV] ­ definitely the most promising approach 3 Software testing This section is based on Chapter 9 of [Pel01] and [MBT]. We mention only some formal parts of software testing area. 3.1 Basic terminology There are two basic approaches to software testing: white box testing (aka transparent box testing)- based on inspecting the source code of the system under test black box testing - does not use the source code (which may be inaccessible or unknown) Software testing methods can be also divided according to the level of the tested parts of the system unit (module) testing - the lowest level of testing, where one tests small pieces of code separately integration testing - testing that different pieces of code work well together system testing - testing the system as a whole 3 y:=y+1 x=y and z>w x:=x-1 true false Figure 1: A simple flowchart. White box testing is suitable for unit testing and integration testing, while black box testing is more appropriate for system testing. We use the following terminology: execution path is a path in the flowchart of the tested code, i.e., it is a sequence of control points and instructions appearing in the tested code test case is a sequence of inputs, actions, and events accompanied with expected response of the system test suite is a set of test cases 3.2 White box testing A program typically has a very large, or even unbounded, number of execution paths. Hence, it is not feasible to examine all of them. Roughly speaking, we would like to have a reasonably small test suite which provides a high degree of probability of finding potential errors. Various code coverage criteria have been defined as a metrices saying whether (or to what extent) a given test suit covers a given code (the higher code coverage, the higher probability of finding potential error). The aim is to find the smallest test suit with the highest coverage. 3.2.1 Control flow coverage criteria We will present the main coverage criteria and the differences between them using a small example described in Figure 1. For the sake of readability, the test cases for our example are described using the state of the variables just prior to the decision predicate x = y z > w. statement coverage: Each executable statement of the program (e.g. assignments, input, test, output) appears in at least one test case. One test case is enough to cover the flowchart according to statement coverage: (x = 2, y = 2, z = 4, w = 3) (1) 4 edge coverage: Each execution edge of the flowchart appears in some test case. To cover the flowchart, we need to add to test case (1) another test case: (x = 3, y = 3, z = 5, w = 7) (2) condition coverage: Each decision predicate is a (possibly trivial) Boolean combination of element conditions (e.g. comparison between two expressions, application of a relation to some program variables). Each of these element conditions appears in some test case where it is calculated to TRUE and in another test case where it is calculated to FALSE, provided that it can have these truth values. Test case (2) together with the test case (x = 3, y = 4, z = 7, w = 5) (3) cover the code. However, in both cases, the decision predicate is evaluated to FALSE... edge/condition coverage: This coverage criterion requires the executable edges as well as the conditions to be covered. Test cases (1), (2), and (3) together cover the code. multiple condition coverage: This is similar to condition coverage, but instead of taking care of each trivial condition, we require each Boolean combination that may appear in any decision predicate during some execution of the program must appear in some test case. To cover the code, we need to add one more test case to the three present test cases. (x = 3, y = 4, z = 5, w = 6) (4) The main disadvantage of the multiple condition coverage is that it involves an explosion of the number of test cases. path coverage: This criterion requires that every executable path be covered by a test case. The number of paths for a given piece of code can be enormous. For example, loops may result in infinite or an unfeasible number of paths. We say that one criterion subsumes another, if guaranteeing the former coverage also guarantees the latter. This relation appears in Figure 2, where a coverage criterion that subsumes another appears above it, with an arrow from the subsuming criterion to the subsumed one. Please note that it can happen due to a lucky selection of the test cases, a less comprehensive coverage will find errors that a more comprehensive approach will happen to miss. The above criteria (except of path coverage) do not treat loops adequately: they do not care about number of iterations. There are several ad hoc strategies for testing loops loop coverage: * Check the case where the loop is skipped. * Check the case where the loop is executed once. * Check the case where the loop is executed some typical number of times. (But what is typical?) * If the bound n on the number of iterations of the loop is known, try executing it n - 1, n, and n + 1 times. Testing loops become even more difficult when nested loops are involved. 5 path coverage multiple condition coverage edge/condition coverage uujjjjjjjjj edge coverage condition coverage statement coverage Figure 2: A hierarchy of control flow coverage criteria. 3.2.2 Dataflow coverage criteria Using control flow coverage criteria, one may fail to include some execution path in which some variable is set to some value for a particular purpose, but later that value is misused. Hence, dataflow coverage criteria have been introduced [RW85]. Definition of dataflow coverage criteria employs the following sets of nodes. By nodes we mean nodes in the flowchart (corresponding to statements and conditions of the program). In the following, x ranges over program variables. def (x) = nodes where some value is assigned to x p-use(x) = nodes where x is used in a predicate (e.g. in if or while statements) c-use(x) = nodes where x is used in some expression other than a predicate For each s def (x) we define the following sets: dpu(s, x) = nodes s p-use(x) such that there is a path from s to s going only through nodes not included in def (x) dcu(s, x) = nodes s c-use(x) such that there is a path from s to s going only through nodes not included in def (x) Each dataflow coverage criterion defines the paths that should be included in a test suite. For each program variable x and each node s def (x), one needs to include at least the following paths starting in s and going only through nodes not included in def (x), as subpaths in the test suite: all-defs: include one path to some node in dpu(s, x) or in dcu(s, x). all-p-uses: include one path to each node in dpu(s, x). all-c-uses/some-p-uses: include one path to each node in dcu(s, x), but if dcu(s, x) is empty, include at least one path to some node in dpu(s, x). all-p-uses/some-c-uses: include one path to each node in dpu(s, x), but if dpu(s, x) is empty, include at least one path to some node in dcu(s, x). all uses: include one path to each node in dpu(s, x) and to each node in dcu(s, x). all-du-paths: include all the paths to each node in dpu(s, x) and to each node in dcu(s, x). These paths should not contain cycles except for the first and the last nodes, which may be the same (for example, an assignment x := x + 1 is both in def (x) and c-use(x)). The hierarchy of the dataflow coverage criteria appears in Figure 3. 6 all-du-paths coverage all-uses coverage xxrrrrrr 88vvvvvv all-c-uses/some-p-uses coverage all-p-uses/some-c-uses coverage tthhhhhhhhhhhhhh all-defs coverage all-p-uses coverage Figure 3: A hierarchy of dataflow coverage criteria. 3.2.3 Notes In general, we cannot expect that our test suite achieves the full coverage (for example, some instructions may be unreachable). Moreover, we cannot even compute the maximal possible coverage as it is undecidable whether a given part of the code is reachable or not. High code coverage is only one property of a quality test suite. There are also other ideas associated with quality of a test suite. For example, mutation analysis [BDLS80] is based on the following idea: A test suite is unlikely to be comprehensive enough if it gives the same results to two different programs. Given a test suite and a code, one generates several mutations of the program (based on code inspection or structural changes) and evaluates the test suite on these mutations. If some test case behaves differently on the original code and a mutation, then the mutation dies. At the end of the process, if a considerable number of mutations remain alive, the test suite is probably inappropriate. Note that an addition of a code monitoring executions of test cases (a code measuring the coverage) can affect the behaviour of the system under test. There are dedicated software packages for test case generation, coverage evaluation, test execution, and test management (maintaining different test suits, perform version control etc.) 3.3 Black box testing: model-based testing The mission of black box testing is to check functionality of all features of the system under test. First we need to know the intended observable behaviour of the system. This behaviour can be described in many ways like simple text, message sequence charts, state machines, etc. Formal descriptions are called models of the system. Figure 4 provides an example of a model given as a finite state machine. We use the model to generate test cases. Again, various coverage criteria can be chosen (some of them are similar to those mentioned before): * covering all the edges * covering all the nodes * covering all the paths (this is usually impractical) * covering each adjacent sequence of n nodes 7 Figure 4: A model of a simple phone system. * covering certain nodes at least/at most a given number of times in each sequence in the test suite * (switch coverage) covering each pair of incoming and outcoming edge for all nodes After execution of the tests and comparison of actual outputs with expected outputs, we decide on further actions (whether to modify the model, generate more tests, or stop testing). 3.3.1 Notes Model checking can be applied to verify whether the model satisfies desired properties. We may want to test primarily the typical executions of the system in order to maximize the minimal time to failure (MTTF). In this case, we can employ probabilistic testing. The system is modelled as Markov chain. The test suite is then generated according to the probabilities of transitions. 4 Deductive software verification This section is based on Chapter 7 of [Pel01]. Research in this area started in late 1960's by Floyd [Flo67] and Hoare [Hoa69]. Since deductive verification is often tedious, it is not performed frequently on the actual code. However, it can be performed on the basic algorithms or on abstractions of the code. The faithfulness of the translation of a program into an abstracted one can sometimes also be formally verified. 4.1 Two notions of correctness To simplify the presentation, we adopt several assumptions on the programs we want to verify. More precisely, we assume that the initial values of the program are stored in input variables x0, x1, . . . and that these variables do not change their values during the execution of the program. We also consider only deterministic programs. By state of a program we mean an assignment to the program variables. Let P be a program and a, b be its states. By P(a, b) we denote the fact that executing P from 8 the state a, it terminates with a state b. Further, by a |= we denote that the state a satisfies the formula . A specification (or some desired property) of a program P is given by two first order formulae: * initial condition is a formula with all its free variables among input variables of P * final assertion We define two notions of correctness. The program P is partially correct with respect to and , written {}P{}, iff for all states a, b the implication P(a, b) a |= = b |= holds. In other words, if the program starts with a state satisfying and then terminates, then the terminal state satisfies . totally correct with respect to and , written P , iff {}P{} and for every state a satisfying the program terminates. 4.2 Verification of flowcharts begin end true false p v:=e Figure 5: Nodes in a flowchart. We identify each program with its flowchart. A flowchart has four kinds of nodes (see Figure 5): begin - one outgoing edge, no incoming edges end - one incoming edge, no outgoing edges assignment has the form v := e, where v is a program variable and e is a first order term; one or more incoming edges, one outgoing edge decision predicate p is an unquantified first order formula; one or more incoming edges, two outgoing edges marked with true and false A location of a flowchart program is an edge connecting two flowchart nodes. An example of a simple flowchart program is given in Figure 6. 4.2.1 Partial correctness To verify that a program is partially correct with respect to and , it is sufficient to perform the following two steps. 1. We attach to each location of the flowchart a first order formula called assertion. To the location exiting from the begin node we attach and is attached to the location entering end node. The idea is that these assertions should be satisfied by every state reachable in the corresponding location by an execution starting in a state satisfying . These assertions are also called invariants1 . 1In some programming languages assertions can be inserted into the code as additional runtime checks so that the program will break with a warning message whenever an invariant is violated. 9 begin true false end y1:=0 y2:=x1 y2>=x2 y1:=y1+1 A C FD E B y2:=y2-x2 Figure 6: A flowchart program for integer division. 2. For every assignment or decision node c, every assumption pre(c) on an incoming edge (called precondition), and every assumption post(c) on an outgoing edge (called postcondition), we prove that if the control of the program is just before c, with a state satisfying pre(c) and c is executed such that the control moves to the location annotated with post(c), then the state after the move satisfies post(c). Every considered triple pre(c), c, post(c) fits into one of the three cases: (a) c is a decision node with a predicate p and post(c) is associated to the outgoing edge marked with true. Then we need to prove: pre(c) p = post(c) (b) c is a decision node with a predicate p and post(c) is associated to the outgoing edge marked with false. Then we need to prove: pre(c) p = post(c) (c) c is an assignment of the form v := e, where v is a variable and e an expression. This case is more difficult, as the states before and after the assignment are different (i.e. pre(c) and post(c) reason about different states). Therefore, we relativize the postcondition to assert about the states before the assignment. Hence, we have to prove pre(c) = post(c)[v/e] where post(c)[v/e] is the assertion post(c) where all occurences of v are replaced with e. Proving the consistency between each precondition and postcondition of all nodes guarantess that {}P{}. In fact, it guarantees even a stronger property: 10 In each execution that starts with a state satisfying the initial condition of the program, when the control of the program is at some location, the assumption attached to that location holds. Finding assertions for the proof may be a difficult task. There are some heuristics and tools suggesting invariants. But there cannot be a fully automatic way of finding them (the problem is undecidable). Example. In order to prove that the flowchart in Figure 6 computes an integer divison, we define the initial condition and final assertion as x1 0 x2 > 0 (x1 = y1 x2 + y2) y2 0 y2 < x2 and the other invariants as (A) x1 0 x2 > 0 (B) x1 0 x2 > 0 y1 = 0 (C) (x1 = y1 x2 + y2) y2 0 (D) (x1 = y1 x2 + y2) y2 x2 (E) (x1 = y1 x2 + y2 - x2) y2 - x2 0 (F) (x1 = y1 x2 + y2) y2 0 y2 < x2 Please note that the decision node y2>=x2 has in fact two ingoing edges, one leading from the node y2:=x1, the other leading from the node y2:=y2-x2. Both locations corresponding to these edges are associated with the invariant (C). Now the consistency can be checked using a mechanized theorem prover (at least in this case). 2 4.2.2 Modification for array variables To verify programs with array variables, the method has to be modified in one point: relativization of postconditions of assignment nodes. The problem can be demonstarted by the following simple example. Consider the assignment x[x[1]] := 2 with precondition pre(c) x[1] = 1 x[2] = 3 and postcondition post(c) x[x[1]] = 2. It is easy to prove that pre(c) = post(c)[x[x[1]]/2] holds as post(c)[x[x[1]]/2] is in fact the tautology 2 = 2. But if pre(c) holds and the assignment is performed, then x[1] = 2 and x[x[1]] = 3 and hence the post(c) does not hold. In order to fix this problem, we extend the syntax of terms with a new construct (x; e1:e2)[e3], where x is an array variable (we assume that the set of array variables is disjoint from simple variables and we do not allow quantifying over array variables in our first order logic) and e1, e2, e3 are terms. Informally, (x; e1:e2) denotes almost the same array as x: only the element with the index e1 has been set to e2. The added construct does not increase the expressiveness of the logic. Consider a formula containing an (x; e1:e2)[e3] construct. This formula can be translated into an equivalent formula (e1 = e3 [(x; e1:e2)[e3]/e2]) ((e1 = e3) [(x; e1:e2)[e3]/x[e3]). This translation removes all occurrences of (x; e1:e2)[e3]. The process can be repeated until all added constructs are eliminated. Let c be an array assignment x[e1] := e2. To guarantee that if pre(c) holds and c is executed then post(c) holds, we have to prove that pre(c) = post(c)[x/(x; e1:e2)] where post(c)[x/(x; e1:e2)] denotes the post(c) formula with x substituted by (x; e1:e2). 11 Example. Let us return to the case where c is x[x[1]] := 2 and post(c) x[x[1]] = 2. The relativized postcondition post(c)[(x; x[1]:2)/x] can be simplified in the following way: post(c)[x/(x; x[1]:2)] (x[x[1]]) = 2)[x/(x; x[1]:2)] (x; x[1]:2)[(x; x[1]:2)[1]] = 2 (x[1] = 1 (x; x[1]:2)[2] = 2) ((x[1] = 1) (x; x[1]:2)[x[1]] = 2) ... x[1] = 1 = x[2] = 2 The resulting formula is the expected one. The simplification steps may be quite difficult and hard to follow. Fortunately, mechanized theorem provers can help. 2 4.3 Proving termination A partially ordered domain is a pair (W, ) where W is a set and is a strict partial order relation over W (i.e. irreflexive, asymmetric, and transitive). We often write u v instead of v u. We also write u v when u v or u = v. A well founded domain is a partially ordered domain that contains no infinite sequence of the form w0 w1 w2 . . .. To prove the termination with respect to the initial condition , we need to follow the following steps: 1. Select a well founded domain (W, ) such that W is a subset of the domain of program variables and is expressible using the signature of the program. 2. Attach to each location in the flowchart an invariant and an expression. The invariant attached to the outgoing edge of the begin node is the initial condition. 3. Show consistency for each triple pre(c), c, post(c), as in the partial correctness proof. 4. We show that expressions associated with locations satisfy the following condi- tions: * When an expression e, attached to a flowchart location, is calculated in some state in the execution (when the program counter is in that location), it is within W. This means that for each location with an associated invariant and expression e we have to prove = (e W). Note that e W is not, in general, a first order logic formula. However, in this context, it can often be translated into a first order formula. * In each execution of the program, when proceeding from one location to its successor location, the value of the associated expression does not increase. More precisely, for every node c, every invariant pre(c) and expression e1 associated with an incoming edge, and every expression e2 associated with an outgoing edge, we have to prove that ­ if c is a decision node with predicate p and e2 is associated with the true edge, then pre(c) p = e1 e2, ­ if c is a decision node with predicate p and e2 is associated with the false edge, then pre(c) p = e1 e2, 12 ­ if c is an assignment v := e then pre(c) = e1 e2[e/v]. * In each execution of the program, during a traversal of a cycle (a loop) in the flowchart there is some point where a decrease occurs in the value of the associated expression from one location to its successor. This means that for each cycle we have to find a node with an incoming and an outgoing edges such that the corresponding implication above holds even if is replaced with . If we manage to do all these steps, the termination is proven. It may be difficult to find the right well founded domain, invariants and expressions. Clearly, termination and partial correctness can be proven simultaneously. Example. Termination of the flowchart in Figure 6 with the initial condition x1 0 x2 > 0 can be proven with the following invariants and expressions: (A) x1 0 x2 > 0 e(A) x1 (B) x1 0 x2 > 0 e(B) x1 (C) x2 > 0 y2 0 e(C) y2 (D) x2 > 0 y2 x2 e(D) y2 (E) x2 > 0 y2 x2 e(E) y2 (F) y2 0 e(F) y2 2 4.4 Axiomatic program verification Hoare [Hoa69] developed a proof system that included both logic and pieces of code. This proof system allows us to verify code (rather than flowcharts) and to prove different sequential parts of the program separately (and combine the proofs later). The logic in constructed on top of some first order deduction system. In addition to first order formulas, the logic allows assertions of the form {}S{}, where , are first order formulas and S is (a part of) a program with the following syntax: S ::= v := e | skip | S; S | if p then S else S fi | while p do S end | begin S end where v is a variable, e is a first order expression, and p is an unquantified first order formula. These assertions are called Hoare triples. A Hoare triple {}S{} means that if execution of S starts with a state satisfying and S terminates from that state, then a state satisfying is reached. Clearly, if S is the entire program, then {}S{} claims that S is partially correct with respect to initial condition and final assertion . The axioms and proof rules of Hoare's logic are given below. The proof rules use the standard notation where premises are above the line while the consequent is below the line. Assignment axiom {[v/e]}v := e{} Skip axiom {}skip{} Left strengthening rule = { }S{} {}S{} 13 Right weakening rule {}S{ } = {}S{} Sequential composition rule {}S1{} {}S2{} {}S1; S2{} If-then-else rule { p}S1{} { p}S2{} {}if p then S1 else S2 fi{} While rule { p}S{} {}while p do S end{ p} Begin-end rule {}S{} {}begin S end{} Some other proof rules can be derived, like the following rules combining the assignment axiom with the left strengthening rule (this rule has actually just one premise, the axiom is written there just for explanation) and the sequential composition rule with the right weakening or left strengthening rule, respectively: = [v/e] (axiom: {[v/e]}v := e{}) {}v := e{} {}S1{1} 1 = 2 {2}S2{} {}S1; S2{} The proof trees are constructed as usual... There are several proof system that extend the Hoare proof system for verifying concurrent programs. Such proof systems provide axioms for dealing with shared variables, synchronous and asynchronous communication, procedure calls). They are usually tailored for a particular programming language, e.g. Pascal or CSP. A generic proof system for handling concurrency was suggested by Manna and Pnueli [MP83]. The system is not connected to any particular syntax. Instead, it works with transition systems. It allows verifying temporal properties. Here is an example of proof rules (these two are called FCS and FPRS): G( = (1 2)) G(1 = X) G(2 = X) G( = X) G( = X) G( = F) 4.5 Notes Deductive verification * is not limited to finite state systems. * can handle programs of various domains and datastructures (and even parametrized programs). * can be applied directly to the code. * can verify that the program is correct (but a bug can occur in compiler, in hardware, due to a wrong initial condition or difference between assumed semantics of code and the real one, etc.). 14 model M 55qqqqqq specification S xxrrrrrrr GF ED @A BC model checking algorithm ~~}}}}}}} 55qqqqqq YES, M satisfies S NO, M does not satisfy S (+ counterexample) Figure 7: The model checking schema. * needs a great mental effort as it is mostly manual (the result depends strongly on the ingenuity of the people performing verification). Hence it is very slow. Moreover, proofs constructed manually may contain errors. The chance to find an error is high. * is not scalable. The presented Hoare's proof system is sound. It is not complete thanks to incompletenes of first order logic with natural numbers and basic arithmetic operations over them (G¨odel's incompletenes theorem). But it is relatively complete, i.e. any correct assertion can be proved under the following two (sometimes unrealistic) conditions: * Every correct (first order) logic assertion that is needed in the proof is already included as an axiom in the proof system. (Alternatively: there is an oracle (e.g. a human) that is responsible to decide whether such an assertion is correct or not.) * Every invariant or intermediate assertion that we need for the proof is expressive. The second condition eliminates the cases when the proof needs some properties that cannot be expressed in first order logic. The relative completeness of the Hoare's proof system implies that the system is complete for programs and first order logic with natural numbers and addition and subtraction as the only operators. 5 Model checking: an overview In this section we define the model checking problem and we provide a basic taxonomy of system classes and temporal logics. In particular, we recall definitions of low-level formalisms for system description (Kripke structure and labelled transition system), Linear Temporal Logic (LTL), and B¨uchi automata (BA). We also provide borders of decidability of the model checking problem. Further, we recall the automata-based approach to LTL model checking of finite-state systems. Informations presented in this section can be found e.g. in Chapters 1, 2, 3 and 9 of [CGP99] and in [May98] (everything specific to infinite-state systems). Model checking problem is the problem to decide whether a given model (or system) satisfies a given specification (see Figure 7). The problem is further specified by the considered class of models and by the considered class of specifications. 15 5.1 Specifications Specification is a formal description of some property that should be satisfied by the system. Note that in the context of model checking, specification usually does not describe the full functionality of the system. Specification is typically given as a formula of some temporal logic. There are two kinds of temporal logics: linear-time logics Formulae are interpreted over sequences representing single runs. The most popular linear-time logic is Linear Temporal Logic (LTL). branching time logics Formulae are interpreted over trees, where a tree represents all possible runs starting in a given state. Typical examples of branching-time logics are Computational Tree Logic (CTL), CTL , Hennessy­Milner logic, and modal -calculus. modal -calculus CTL wwwwwww CTL LTL Henessy-Milner logic Figure 8: The hierarchy of basic temporal logics. Figure 8 represents the relative expressive power of the mentioned logics: a line between two logics means that every property expressible in the lower logic can be also expresses in the upper logic, but not vice versa. Temporal logics can be also divided into state-based and action-based. state-based These logics talk about properties of states of the system. Properties of a single state are reflected by validity of atomic propositions in the state. These atomic propositions are then atomic formulaes of state-based logics. action-based Every transition of a system is labelled with an action. Action-based logic are interpreted over behaviours of the system represented only by sequences (or trees) of actions. In the following, we focus on LTL model checking problems. Now we provide definition of both action-based and state-based LTL. Formulas of state-based Linear Temporal Logic (LTL) are defined by the abstract syntax equation ::= | a | | 1 2 | X | 1 U 2, where stands for true and a ranges over a countable set AP of atomic propositions. We also use to abbreviate , F to abbreviate U , G to abbreviate F, and R to abbreviate ( U ). The temporal operators X, F, U, G, R are called next, eventually, until, globally, and release, respectively. The set of atomic propositions occurring in a formula is denoted by AP(). We define the semantics of LTL in terms of languages over infinite words. An alphabet is a set = 2AP , where AP AP is a finite subset. A word over alphabet is an infinite sequence w = w(0)w(1)w(2) . . . of letters from . For every i N0, by wi we denote the suffix of w of the form w(i)w(i + 1)w(i + 2) . . .. The validity of an LTL formula for w , written w |= , is defined as follows: 16 w |= w |= a iff a w(0) w |= iff w |= w |= 1 2 iff w |= 1 w |= 2 w |= X iff w1 |= w |= 1 U 2 iff i N0 : wi |= 2 0 j < i : wj |= 1 Given an alphabet , an LTL formula defines the language L () = {w | w |= }. An action-based LTL is very similar to the state-based version. The only changes are the following. In the syntax, a ranges over countable set of actions Act. Formulae of action-based LTL are then interpreted over infinite sequences of actions from a finite subset Act Act. Semantics of formula a is defined as follows: w |= a iff a = w(0) The specification can be formulated also without any logic. Linear-time properties can be defined for example with use of B¨uchi automata. Definition 5.1. A B¨uchi automaton (BA) is a tuple A = (, Q, , q0, F), where * is a finite alphabet, * Q is a finite set of states, * : Q × 2Q is a transition function, * q0 Q is an initial states, * F Q is a set of accepting states. A run of A on inifnite word w = w(0)w(1)... is an infinite sequence of states = (0)(1)..., where (0) = q0 and (i + 1) ((i), w(i)) holds for all i. A run is accepting if Inf ()F = , where Inf () is a set of the states appearing in infinitely often. An automaton A accepts a word w if there is an accepting run of A on w. We set L(A) = {w | A accepts w}. a a b q2 b q1 Figure 9: A B¨uchi automaton accepting words with infinitely many occurrences of a. A graphical description of B¨uchi automata is identical to the graphical desciprion of nondeterministic finite automata (see Figure 9). Later we show that every action-based LTL formula can be translated into an equivalent B¨uchi automaton. 17 byte cnt = 0; // number of processes in critical sections byte turn = 0; // token for entering a critical section init { run(P0); run(P1); // parallel execution of P0 a P1 } proctype P0() proctype P1() { { // s0 //s1 do do // NC0 (noncritical section) // NC1 (noncritical section) :: do :: do :: (turn == 0) -> break; :: (turn == 1) -> break; :: else; :: else; od; od; // CS0 (critical section) // CS1 (critical section) cnt = cnt + 1; cnt = cnt + 1; cnt = cnt - 1; cnt = cnt - 1; turn = 1; turn = 0; od; od; } } Figure 10: Mutual exclusion program in ProMeLa. 5.2 Models By model we mean a formal description of all possible behaviours of the system to be verified, where behaviour is a sequence (or a tree in the branching-time setting) of successive states or actions (depending on the setting) starting in an initial state of the system. A model can be described in a standard language (C, Java, VHDL, . . . ), or in some dedicated languge (for examle, SPIN [SPI] uses Process or Protocol Meta Language ProMeLa2 ), or with use of some process algebra (BPA, BPP, PA, pushdown processes, Petri nets, . . . . Here we introduce two low-level formalisms for representation of models: Kripke structure (used in context of state-based model checking) and labelled transition systems (used for the action-based approach). Definition 5.2. A Kripke structure is a tuple M = (S, R, S0, L), where * S is a set of states * R S × S is transitions relation * S0 S is a set of initial states * L : S 2AP is a labelling function associating to each state s S the set of atomic propositions that are true in s. A path in M starting in a state s is an infinite sequence = s0s1s2... of states such that s0 = s and (si, si+1) R holds for every i. Given a set AP AP, we set LAP (M) = {l0l1 . . . | a path s0s1 . . . of M . i 0 : li = L(si) AP }. 2An example of ProMeLa code is provided by Figure 10. 18 turn = 0 s0, NC1 turn = 0 NC0, s1 turn = 0 CS0, s1NC0, NC1 turn = 0 CS0, NC1 s0, CS1 turn = 1 s0, NC1 turn = 1 turn = 1 NC0, s1 turn = 1 NC0, NC1 turn = 1 NC0, CS1 , turn = 0 s0, s1 turn = 1 , turn = 1 s0, s1 turn = 0 turn = 0 Figure 11: Kripke structure for a mutual exclusion program. Figure 11 provides an example of a Kripke structure corresponding to the ProMeLa code of Figure 10. Each state is directly marked with the atomic propositions valid in the state. Definition 5.3. A labelled transition system (LTS) is a tuple M = (S, Act, , s0), where * S is a set of states * Act is a set of atomic actions or labels * S × Act × S is transitions relation (we write s a t instead of (s, a, t) ) * s0 S is a distinguished initial states A run of M over u = u0u1 . . . Act is a seguence s0 a0 s1 a1 s2 a2 . . . , where s0 is the initial state. We set L(M) = {u Act | there is a run of M over u}. We often use some more concise formalism for description of models. In particular, infinite-state models cannot be finitely described directly by a Kripke structure or an LTS. We introduce a formalism called Process Rewrite Systems (PRS) [May00], which subsumes many standard formalisms for description of infinite-state systems. More information about PRS and their properties can be found in [May98, ˇReh07]. The concept of Process Rewrite Systems is based on rewriting of process terms. 19 Definition 5.4. Let Const = {X, . . .} be a countably infinite set of process constants. The set T of process terms is defined by the abstract syntax t ::= | X | t1.t2 | t1 t2, where * is the empty term, * X Const is a process constant (used as an atomic process), * ' ' means a parallel composition, and * '.' means a sequential composition. We always work with equivalence classes of terms modulo commutativity and associativity of ' ' and modulo associativity of '.' We also define .t = t = t. and t = t. By Const(t) we denote the set of process constants occurring in t. We distinguish four classes of process terms as: "1" terms consisting of a single process constant only (i.e. 1), e.g. X. "S" sequential terms without parallel composition, e.g. X.Y.Z. "P" parallel terms without sequential composition. e.g. X Y Z. "G" general terms with arbitrarily nested sequential and parallel compositions. Definition 5.5. Let Act = {a, b, } be a countably infinite set of atomic actions and , {1, S, P, G} such that . An (, )-PRS (process rewrite system) is a pair = (R, t0), where * R (( {}) × Act × ) is a finite set of rewrite rules, and * t0 is an initial term. We write (t1 a t2) R instead of (t1, a, t2) R. We define Const() as the set of all constants occurring in the rewrite rules of or in its initial state, and Act() as the set of all actions occurring in the rewrite rules of . Definition 5.6. The semantics of an (, )-PRS = (R, t0) is given by the LTS (S, Act(), -, t0), where * the set of states S = {t | Const(t) Const()}, * the transition relation - is the least relation satisfying the following inference rules for all t1, t2, t S and a Act(). (t1 a t2) R t1 a - t2 t1 a - t2 t1 t a - t2 t t1 a - t2 t1.t a - t2.t Note that parallel composition is commutative and, thus, the inference rule for parallel composition also holds with t1 and t exchanged. Every pair , {1, S, P, G} induces a class of all labelled transition systems that can be expressed by an (, )-PRS. Some of the classes correspond to LTS classes of widely known models. * (1, 1)-PRS are equivalent to finite-state systems (FS). Every process constant corresponds to a state and the state space is bounded by |Const()|. * (1, S)-PRS are equivalent to Basic Process Algebra processes (BPA).This class can model sequential programs with procedures. BPA can model unbounded nesting of procedure calls, but cannot model return values and global variables. 20 ˇ (1, P)-PRS are equivalent to communication-free nets, the subclass of Petri nets where every transition has exactly one place in its preset. This class of Petri nets is equivalent to Basic Parallel Processes (BPP).The class can model systems consisting of simple finite-state parallel processes. The number of parallel processes in unbounded. Processes can be dynamically created or terminated, but they cannot communicate. * (1, G)-PRS are equivalent to PA-processes,process algebras with sequential and parallel composition, but no communication. This is the least common generalization of BPA and BPP. * It is easy to see that pushdown automata can be encoded as a subclass of (S, S)PRS (with at most two constants on the left-hand side of rules). Caucal showed that any unrestricted (S, S)-PRS can be presented as a pushdown automaton, in the sense that the transition systems are isomorphic up to the labelling of states. Thus (S, S)-PRS are equivalent to pushdown processes (PDA) (which are the processes described by pushdown automata). This formalism can model sequential programs with procedure call, return values, and global variables. * (P, P)-PRS are equivalent to Petri nets (PN). Every constant corresponds to a place in the net and the number of occurrences of a constant in a term corresponds to the number of tokens in this place. This is because we work with classes of terms modulo commutativity of parallel composition. Every rule in corresponds to a transition in the net. * (S, G)-PRS is the smallest common generalisation of pushdown processes and PA-processes. They are called PAD (PA + PDA). * (P, G)-PRS are called PAN-processes.It is the smallest common generalisation of Petri nets and PA-processes and it strictly subsumes both of them (e.g. PAN can describe all Chomsky-2 languages while Petri nets cannot). * The most general case (G, G)-PRS is simply called PRS. Figure 12 describes a hierarchy of (, )-PRS classes with respect to strong bisimulation equivalence (bisimilarity). We call this hierarchy the PRS-hierarchy. More precisely, the classes of PRS systems are interpreted as the sets of their underlying labelled transition systems. A line connecting X and Y with Y placed higher than X means that every transition systems definable in X can be (up to bisimulation equivalence) defined in Y while the reverse does not hold ­ we write X Y . Moreover, the classes that are not connected by any sequence of upward going lines are incomparable. 5.3 Model checking problems and decidability At the beginning, we have said that the model checking problem is to decide whether a given model satisfies a given specification. We have to define when a system satisfies a specification. In general, it means that all behaviours of the systems satisfy the specification. In state-based LTL setting, it means that a given model M and a given LTL formula satisfy LAP() (M) L2AP() (). Similarly, in action-based LTL setting, it means that a given model M and a given LTL formula satisfy L(M) LAct (). Recall that the model checking problem is parametrized by a logic and a class of systems. Hence, the model checking problem for a logic L and a class of systems C is to decide whether a given model of C satisfies a given formula of L. The combination of L and C determines whether the problem is decidable or not. For example, Figure 13 21 PRS (G, G)-PRS rrrrrrrr vvvvvvvv PAD (S, G)-PRS vvvvvvvv PAN (P, G)-PRS rrrrrrrr PDA (S, S)-PRS PA (1, G)-PRS rrrrrrrr vvvvvvvv PN (P, P)-PRS BPA (1, S)-PRS vvvvvvvv BPP (1, P)-PRS rrrrrrrr FS (1, 1)-PRS Figure 12: The PRS-hierarchy presents the decidability boundary of action-based LTL model checking problem for classes of PRS hierarchy, The situation in state-based LTL model checking is more complicated as the decidability depends also on the set of atomic proposition and their relation to states. The decidability border may differ from the one for action-based LTL model checking mentioned. For example, the state-based LTL model checking is undecidable for the class of Petri nets with atomic propositions saying whether a particular places are non-empty. Later we will show that state-based LTL model checking remains decidable for PDA where validity of atomic propositions depends only on control state and the topmost stack symbol. 5.4 Automata-based LTL model checking of finite systems This subsection is devoted to a prominent model checking problem: state-based LTL model checking of finite state systems. Figure 14 represents the automata-based approach to LTL model checking of finitestate systems. For details see [CGP99]. Time and space complexity of this Lalgorithm is O(|M| 2O(||) ), where |M| is the number of states and transitions in the Kripke structure M. The LTL model checking problem is PSPACE-complete. The biggest disadvantage of this approach originates in translations of a model into the corresponding Kripke structure: the Kripke structure is extremely large even for systems with relatively short description in some higher-level formalism (these formalisms represent the state space implicitly, while a Kripke structure explicitely represents each state of the model). This phenomenon is called state explosion problem. The main sources of the explosion are large domains of variable values, parallelism, dynamically allocated memory, etc. Many techniques fighting this problem have been 22 PRS qqqqqqqqqqqq wwwwwwwwwwww PAD wwwwwwwwwwwww PAN qqqqqqqqqqqqq undecidable decidable iiiiii PDA PA qqqqqqqqqqqqq wwwwwwwwwwwww PN BPA wwwwwwwwwwwww BPP qqqqqqqqqqqqq FS Figure 13: The decidability boundaries of the action-based LTL model checking. suggested. Some of them aim to minimize the Kripke structure, for example * abstraction, * partial order reduction, * symmetry reduction. Other techniques try to optimize the memory consumption of model checking algorithms or enable the algorithms to use more hardware sources (e.g. by running on more computers simultaneously): * on-the-fly algorithms * symbolic model checking * distributed algorithms Some of these methods are mentioned in the following sections. 6 Translation LTLBA via alternating automata There are two popular translations of LTL formulae into equivalent B¨uchi automata. Both of them proceed in two steps: * an LTL formula is translated into an intermediate formalism * this formalism is then translated into B¨uchi automata. One translation uses generalized B¨uchi automata (see e.g. Chapter 9 of [CGP99]), while the other employs alternating 1-weak B¨uchi automata [Var95]. The latter translation is more frequent nowadays as there exist some optimization reducing the size of alternating 1-weak automata and hence the B¨uchi automata produced by the whole translation are in some cases smaller than the automata produced by the other translation. We present the translation using alternating automata. 6.1 Alternating 1-weak B¨uchi automata (A1W) The transition function of an alternating automaton assigns to each state and letter a positive boolean formula over states. The set of positive boolean formulae over set 23 Kripke structure M with finitely many states LTL formula B¨uchi automaton AM accepts paths of M starting in initial states and projected by L to 2AP () 88xxxxxxxx B¨uchi automaton A accepts words over 2AP() violating xxpppppppppp product B¨uchi automaton B L(B) = L(AM ) L(A) L(B) ? = e.g. nested DFS algorithm wwooooooooooo 99yyyyyyyy YES NO + counterexample Figure 14: Automata-based LTL model checking of finite system. Q (denoted B+ (Q)) consists of formulae (true), (false), all elements of Q, and boolean combinations over Q built with and . A subset S of Q is a model of B+ (Q) iff is satisfied by the valuation assigning true just to states in S. A set S is a minimal model of (denoted S |= ) iff S is a model of and no proper subset of S is a model of . If we transform a positive boolean formula into a disjunctive normal form (DNF), then every minimal model corresponds to some clause and vice versa. Let us note that there is no model of , while every subset of Q is a model of . The minimal model of is the empty set. Definition 6.1. An alternating B¨uchi automaton is a tuple A = (, Q, , q0, F), where * is a finite alphabet, * Q is a finite set of states, * : Q × B+ (Q) is a transition function, * q0 Q is an initial state, * F Q is a set of accepting states. By A(p) we denote the automaton A with initial state p Q instead of q0. A run of an alternating automaton is a (potentially infinite) tree. A tree is a set T N 0 such that if xc T, where x N 0 and c N0, then also x T and xc T for all 0 c < c. A Q-labeled tree is a pair (T, r) where T is a tree and r : T Q is a labeling function. A run of an automaton A = (, Q, , q0, F) over word w = w(0)w(1) . . . is a Q-labeled tree (T, r) such that r() = q0 and for each x T the set S = {r(xc) | c N0, xc T} satisfies S |= (r(x), w(|x|)). A run (T, r) is accepting iff for each infinite path in T it holds that Inf ()F = , where Inf () is the set of all labels (i.e. states) appearing infinitely often on . An automaton A accepts a word w iff there exists an accepting run of A over w. A language of all words accepted by an automaton A is denoted by L(A). A (standard) B¨uchi automaton (BA) corresponds to an alternating B¨uchi automaton where, for each q Q and l , (q, l) is a disjunction of states (or ). The 24 difference is only in notation: in the case of (standard) B¨uchi automata we usually write (q, l) = {q1, . . . , qn} instead of (q, l) = q1 . . . qn and (q, l) = instead of (q, l) = . Definition 6.2. Let A = (, Q, , q0, F) be an alternating B¨uchi automaton. By Succ(p) we denote the set Succ(p) = {q | l , S Q : S {q} |= (p, l)} of all possible successors of p. We also set Succ (p) = Succ(p) {p}. An automaton A is called 1-weak (or linear or very weak) if there exists an ordering < on the set of states Q such that q Succ (p) implies q < p. In the following we use A1W automaton meaning `alternating 1-weak B¨uchi automaton'. Further, instead of S |= (l, p) we write p l S and say that there is a transition leading from p to S under l. We also say that a state p has a loop whenever p Succ(p). m l m l n q3 q2 p q1 n n l m Figure 15: An A1W automaton accepting the language l m(l + m + n) n . An A1W automaton A = (, Q, , q0, F) can be drawn as a graph; nodes are the states and every transition p l S is depicted as a branching edge labelled with l and leading from node p to the nodes in S. Edges that are not leading to any node correspond to the cases when S is the empty set, i.e. (p, l) = . Initial and accepting states are indicated in the standard way. For example, Figure 15 depicts an automaton accepting the language l m{l, m, n} n . 6.2 LTLA1W translation [MSS88, Var95] Let be an LTL formula and be an alphabet. The formula can be translated into an automaton A satisfying L(A) = L (), where A = (, Q, , q, F) and * the states Q = {q, q | is a subformula of } correspond to the subformulae of and their negations, * the transition function is defined inductively as: (q , l) = (qa, l) = if a l, (qa, l) = otherwise (q, l) = (q, l) (q, l) = (q, l) (q, l) (qX, l) = q (qU, l) = (q, l) ((q, l) qU) 25 where denotes the positive boolean formula dual to defined by induction on the structure of as: = q = q = = q = q = * the set of accepting states is F = {q(U) | U is a subformula of }. One can readily confirm that the resulting automaton is always A1W automaton. Moreover, the number of its states is linear in the length of . 6.3 A1WBA translation [Var95] Let A = (, Q, , q0, F) be an alternating BA. A B¨uchi automaton accepting the language L(A) can be constructed as A = (, Q , , q0, F ), where * Q = 2Q × 2Q , * q0 = ({q0}, ), * F = {} × 2Q , * ((U, V ), l) is defined as: ­ if U = then ((U, V ), l) = {(U , V ) | X, Y Q such that X |= V qU (q, l) and Y |= V qV (q, l) and U = X F and V = Y (X F)} ­ if U = then ((, V ), l) = {(U , V ) | Y Q such that Y |= V qV (q, l) and U = Y F and V = Y F)} Intuitively, A guesses labeling of each level of the computation tree of A. Moreover, A has to divide the set of states into two sets: states labeling paths with recent occurrence of an accepting states and the other states. 7 Partial order reduction Let LTL-X denote the fragment of all LTL formalas without X operator. The partial order reduction method can be used in model checking of finite systems against LTL-X formulas to reduce the systems to be checked. The size of the reduced system is usually 3­99% of the original size [Pel06]. Hence, the model checking process is faster and consumes less memory. The method is best suited for asynchronous systems. The method is also called model checking using representatives. This section is based on Chapter 10 of [CGP99]. In this section we use a slightly different definition of a Kripke structure: Definition 7.1. Kripke structure is a tuple (S, T, S0, L), where * S is a set of states, * T is a set of transitions (for each T, S × S), * S0 S is a set of initial states, * L : S 2AP is a labelling function associating to each state a set of atomic propositions that are true in the state. 26 We also consider finite and deterministic systems only. Hence every T is seen as a partial function : S S. A transition is enabled in a state s if (s) is defined. Otherwise, is disabled in s. The set of transitions enabled in s is denoted by enabled(s). A path in a Kripke structure K starting from a state s S is an infinite sequence = s0, s1, . . . of states such that s0 = s and for every i there is a transition i T satisfying i(si) = si+1. A path starting in a fixed state can be also identified with a sequence of transitions. Let be an LTL formula and let AP() denote the finite set of atomic propositions occurring in . A path = s0, s1, . . . of a Kripke structure (S, T, S0, L) satisfies , written |= , if w |= , where the word w = w(0)w(1) . . . is defined as w(i) = L(si) AP() for all i 0. A Kripke structure K satisfies , written K |= , if all paths starting from initial states of K satisfy . The model checking problem is the problem to decide whether for a given Kripke structure K and a given specification formula it holds that K |= . Let us consider a fixed Kripke structure K = (S, T, S0, L) and a fixed LTL-X formula . The idea of partial order reduction method is to disable some transitions in some states of K in such a way that the resulting structure K is equivalent to K in the sense that K |= if and only if K |= . More precisely, for every path of the original system starting from an initial state there has to be a path in the reduced system starting from an initial state such that |= iff |= . The reduced system is defined by so-called ample sets. For each state s, ample(s) enabled(s) is the set of transitions that are enabled in s in the reduced system. Calculation of ample sets needs to satisfy three goals: 1. The reduced system given by ample sets has to be correct, i.e. it has to satisfy iff the original system satisfies . 2. The reduced system should be substantially smaller than the original. 3. The overhead in calculating ample sets must be reasonably small. First we formulate some conditions on ample sets. Then we prove that ample sets matching these conditions define a correct reduced system. Finally we discuss some heuristics for calculating such ample sets and we argue that these sets can be calculated on-the-fly. 7.1 Conditions on ample sets First we recall the cornerstone of partial order reduction: the concept of stuttering. Let w be an infinite word. A letter w(i) is called redundant iff w(i) = w(i+1) and there is j > i such that w(i) = w(j). The canonical form of w is the infinite word obtained by deleting all redundant letters from w. Two infinite words w1, w2 are stutter equivalent, written w1 w2, iff they have the same canonical form. Theorem 7.2 ([Lam83]). Any LTL-X formula cannot distinguish between words that are stutter equivalent, i.e. the formula either satifies all such words or none of them. The stuttering equivalence can be extended to paths and Kripke structures. Paths = s0, s1, . . . and = s0, s1, . . . are stutter equivalent with respect to a set AP AP, written AP , iff w w , where w, w are defined as w(i) = L(si) AP and w (i) = L(si) AP for all i 0. Two Kripke structures K, K are stutter equivalent with respect to AP , written K AP K , iff * K and K have the same set of initial states, * for each path of K starting in an initial state s there exists a path of K starting in the same initial state such that AP and vice versa. 27 ?>=<89:;s0 0 ))`````` ?>=<89:;s1 1 00`````` ?>=<89:;r0 0 ?>=<89:;s2 2 00`````` ?>=<89:;r1 1 m ?>=<89:;r2 2 ?>=<89:;sm 11cccccc m ?>=<89:;rm Figure 16: Transition commuting with 01 . . . m. From Theorem 7.2 we immediately get: Corollary 7.3. Let be an LTL-X formula and K, K be Kripke structures such that K AP() K . Then K |= iff K |= . Hence, given a fixed LTL-X formula , for every set of stutter equivalent paths (with respect to AP()) of the original Kripke structure it is sufficient to keep at least one representant of these paths in the reduced structure. A transition T is invisible with respect to a set of propositions AP AP if for each pair of states s, s S such that (s) = s it holds that L(s)AP = L(s )AP . We always consider invisibility with respect to the set AP(). A transition is visible if it is not invisible. Definition 7.4. An independence relation I T ×T is a symmetric and antireflexive relation satisfying the following two conditions for each state s S and for each (, ) I: * Enabledness: if , enabled(s) then enabled((s)) * Commutativity: if , enabled(s) then ((s)) = ((s)) The dependency relation D is the complement of I, namely D = (T × T) I. When it is hard to check whether two transitions are independent or not, it is safe to assume that they are dependent. We say that state s is fully expanded when ample(s) = enabled(s). The following four conditions ensure that the reduced system is stutter equivalent to the original one (with respect to AP()). C0 ample(s) = if and only if enabled(s) = C1 Along every path in the original structure that starts in s, the following condition holds: a transition that is dependent on a transition in ample(s) cannot be executed without a transition in ample(s) occuring first. The condition C1 implies the following lemma. Lemma 7.5. The transitions in enabled(s) ample(s) are all independent of those in ample(s). 28 /.-,()*+ /.-,()*+ /.-,()*+ 1 ((WWWWWWW /.-,()*+ 3 ff /.-,()*+ 2 oo /.-,()*+ 1 ((WWWWWWW /.-,()*+ 3 ff /.-,()*+ 2 oo /.-,()*+ 1 ((WWWWWWW /.-,()*+ 3 ff /.-,()*+ 2 oo /.-,()*+ 1 ((WWWWWWW /.-,()*+ 3 ff /.-,()*+ 2 oo Figure 17: Two concurrent processes, full and (an invalid) reduced structures ( is visible, 1, 2, 3 are invisible, is independent of 1, 2, 3, and 1, 2, 3 are interdependent). Thanks to C1, all paths of the original structure starting in a state s and not included in the reduced structure have one of the following two forms: * the path has a prefix 01 . . . m, where ample(s) and each i is independent of all transitions in ample(s) including . * the path is an infinite sequence of transitions 01 . . . where each i is independent of all transitions in ample(s). Due to C1, after execution of a finite sequence of transitions 01 . . . m not in ample(s) from s, all the transitions in ample(s) remain enabled. Further, C1 implies that the sequence of transitions 01 . . . m executed from s leads to the same state as the sequence 01 . . . m (see Figure 16). As the sequence 01 . . . m is not included in the reduced system, we want 01 . . . m and 01 . . . m to be prefixes of stutter equivalent paths. This is quaranteed if is invisible. Therefore we formulate condition C2: C2 (invisibility) If s is not fully expanded, then every ample(s) is invisible. Conditions C0, C1 and C2 are not yet sufficient to guarantee that the reduced structure is stutter equivalent to the original one. There is a possibility that some transition will be delayed forever because of a cycle (see Figure 17). To remedy this problem, we add the following condition: C3 (cycle condition) A cycle in reduced structure is not allowed if it contains a state in which some transition is enabled, but is never included in ample(s) for any state s on the cycle. Condition C0, C1, C2, and C3 are sufficient. 7.2 Example Consider the following program for mutual exclusion: P :: m : cobegin P0 P1 coend P0 :: l0 : while True do NC0 : wait(turn = 0); CS0 : turn := 1; endwhile; P1 :: l1 : while True do NC1 : wait(turn = 1); 29 turn = 0 s0, NC1 NC0, s1 turn = 0 CS0, s1 turn = 0 NC0, NC1 turn = 0 CS0, NC1 s0, CS1 turn = 1 s0, NC1 turn = 1 turn = 1 NC0, s1 turn = 1 NC0, NC1 turn = 1 NC0, CS1 , turn = 0 s0, s1 turn = 1 , turn = 1 s0, s1 turn = 0 turn = 0 Figure 18: Reduced Kripke structure for the mutual exclusion program. CS1 : turn := 0; endwhile; Each process Pi has a noncritical region (when program counter pci has value NCi) and a critical region (when pci = CSi). The processes share the boolean variable turn. We would like to prove that, regardless the initial value of turn, the two processes cannot be in their critical regions at the same time. This desired property can be described by LTL-X formula = G((pc0 = CS0) (pc1 = CS1)). Figure 18 presents the Kripke structure corresponding to the program. Each state is labelled by values of turn, pc0 and pc1 (value of pc0 and pc1 is before the processes P0, P1 are started). The transition corresponds to the parallel start of processes P0, P1 and transitions i, i, i, i to execution of the commands at program locations li, NCi when turn = i, NCi when turn = i, CSi, respectively. The system can be reduced before model checking against the property . The reduced system has to be stutter equivalent to the original one with respect to AP() = {pc0 = CS0, pc1 = CS1}. Only the actions 0, 1, 0, 1 are visible with respect to AP(). The dependency relation is calculated according to the following rules. * All of the transitions are dependent on as it must be executed before any other transition in the program. * Each transition is dependent on itself (since dependency is reflexive). * Two transitions that change the same variable (including program counters) are dependent. * If one transition sets a variable and the other checks that variable, then the transitions are dependent. Thus, all transitions of the same process are interdependent. Also, pairs (1, 0), (0, 1), ( 1, 0), ( 0, 1), (0, 1) are dependent. 30 The reduced system satisfying conditions C0­C3 is also given in Figure 18. 7.3 Correctness Let be a fixed specification formula. The considered reduction is done with respect to the set AP(). Let K be a full structure and K be its reduced version satisfying the conditions C0­C3. We prove that K AP() K . Given a (finite or infinite) sequence v of transitions, vis(v) denotes the projection of v onto the visible transitions. Given two finite sequences v, w of transitions, we write v < w if v can be obtained from w by erasing one or more transitions. We write v w whenever v < w or v = w. For the rest of this subsection we extend the definition of path allowing both finite and infinite paths. By we denote the path constructed by concatenation of a finite path and a (finite or infinite) path ( is applicable only if the last state last() of is the same as the first state of ). By || we denote the number of transitions in . Let tr() denote the sequence of transitions on a path . Let be an infinite path of K starting in some initial state. We construct an infinite sequence of infinite paths 0, 1, 2, . . . where = 0. Each i is defined as i i such that |i| = i. Paths i are defined by induction. Clearly, 0 = = 0 0 where 0 is just the first state of and 0 = . The path i+1 = i+1 i+1 is constructed from i = i i in the following way. Let s0 = last(i) and i = s0 0 s1 1 s2 2 . . . . There are two cases: A 0 ample(s0). Then i+1 = i (s0 0 s1) and i+1 = s1 1 s2 2 . . .. B 0 ample(s0). By C2, all transitions in ample(s0) must be invisible. There are two cases: B1 Some ample(s0) appears on i after some sequence of independent transitions 01 . . . k-1 (i.e. = k). Then there is a path = s0 (s0) 0 (s1) 1 . . . k-1 (sk) k+1 sk+2 k+2 . . . . B2 Some ample(s0) is independent of all the transitions in i. Then there is a path = s0 (s0) 0 (s1) 1 (s2) 2 . . . . In both cases i+1 = i (s0 (s0)) and i+1 is obtained from by removing the first transition s0 (s0). Please note that the above construction uses conditions C0 and C1. Lemma 7.6. For every 0 i j it holds that: 1. i AP() j. 2. vis(tr(i)) = vis(tr(j)). 3. Let i, j be prefixes of i, j such that vis(tr(i)) = vis(tr(j)). Then L(last(i)) AP() = L(last(j)) AP(). Proof. It is sufficient to consider the case where j = i + 1. The proof is trivial if i+1 was constructed according to the case A as i = i+1. The proof for the cases B1 and B2 are straightforward. The following lemma is obvious. 31 Lemma 7.7. Let be the infinite path constructed as the limit of the finite paths i. Then belongs to the reduced structure K . Now it remains to prove that the path is stutter equivalent to . First we show that contains all the visible transitions of , and in the same order. Lemma 7.8. Let be the first transition of i. There exists j > i such that is the last transition of j and, for all i k < j, is the first transition of k. Proof. If is the first transition of k then it is clearly the last transition of k+1 (case A) or the first transition of k+1 (case B). The condition C3 implies that the second case cannot hold for all k i. Lemma 7.9. Let be the first visible transition on i and prefix(i) be the maximal prefix of tr(i) that does not contain . Then one of the following holds: * is the first action of i and the last transition of i+1, or * is the first visible transition of i+1, the last transition of i+1 is invisible, and prefix(i+1) prefix(i). Proof. If i+1 was constructed from i by the case A, then the first case of the lemma holds: if the first action of i is visible, then ample(s0) = enabled(s0) due to C2 and hence ample(s0). Now assume that i+i was constructed according to B, i.e. there exists another action that is appended to i to form i+1. Due to C2, is invisible. There are three cases: 1. appears in i before (case B1) 2. appears in i after (case B1) 3. is independent of all transitions of i (case B2) In case (1), prefix(i+1) < prefix(i) while prefix(i+1) = prefix(i) in cases (2) and (3). Lemma 7.10. Let v be a prefix of vis(tr()). Then there exists a path i such that v = vis(tr(i)). Proof. By induction on the length of v. The base case (|v| = 0) is trivial. Assume that v is a prefix of vis(tr()) and there is a path i such that vis(tr(i)) = v. We show that there is a path j where j > i and vis(tr(i)) = v, i.e. we show that is eventually added to j for some j > i and that no other visible transition is added to k for i < k < j. The construction implies that a visible transition can be added to the end of k to form k+1 only if it is the first transition of k. Lemma 7.9 says that remains the first visible transition in paths k for k > i unless it is being added to some j. Moreover the sequence of transitions before can only shrink. Lemma 7.8 says that the sequence will eventually shrink. Thus, is eventually added to some j. Theorem 7.11. The structures K and K are stutter equivalent with respect to AP(). Proof. It is sufficient to show that, for every path of K starting from an initial state, the path produced by the described construction is stutter equivalent to with respect to AP(). Note that starts from the same state as , this state is also an initial state in K , and that is a path in K due to Lemma 7.7. Lemma 7.10 implies that vis(tr()) = vis(tr()). Let vi denote the prefix of vis(tr()) = vis(tr()) of length i. Let |vi be the shortest prefix of such that vis(tr(|vi )) = vi and let |vi be the shortest prefix of such that vis(tr(|vi )) = vi. The definition of implies that |vi is a prefix of some k. Lemma 7.6 (3) says that L(last(|vi )) AP() = L(last(|vi )) AP(). Further, for every state s reachable from last(|vi ) or last(|vi ) by a sequence of invisible actions it holds that L(s)AP() = L(last(|vi ))AP() = L(last(|vi ))AP(). Hence, AP() . 32 7.4 Calculating ample sets First we discuss the complexity of checking conditions C0 to C3. Conditions C0 and C2 are local in the sense that their satisafaction in a state s depends just on sets enabled(s) and ample(s). C0 can be checked in constant time while C2 can be checked in linear time (with respect to the size of ample(s)). We focus on more complex non-local conditions C1 and C3. Theorem 7.12. Checking condition C1 for a state s and a set of transitions T enabled(s) is at least as hard as checking reachability for the original structure. Proof. It is easy to show that the problem whether a given state is reachable in a given structure can be reduced to checking condition C1. To avoid checking condition C1 for arbitrary subset of enabled transitions, we will give a procedure computing a set of transitions that is guaranteed to satisfy C1. The computed sets do not have to be optimal ­ there is a tradeoff between efficiency of computation and amount of reduction. Condition C3 is also non-local. In contrast to C1, C3 refers only to the reduced structure. Instead of checking C3, we formulate a stronger condition which is easier to check. Lemma 7.13. Assume that C1 holds for all ample sets along a cycle in a reduced structure. If at least one state along the cycle is fully expanded, then C3 hold for this cycle. Proof. Lemma 7.5 says that transitions in enabled(s) ample(s) are all independent of those in ample(s). Hence, every transition in enabled(s) ample(s) for some state s on a cycle is also enabled in the next state on the cycle. If the cycle contains a fully expanded state, then it surely satisfies C3. If we use depth-first search strategy to generate (and verify) a reduced structure, we can use the fact that every cycle in the reduced structure has to contain a back edge (i.e. an edge going to a state on the search stack) to replace C3 by the following stronger condition. C3' If s is not fully expanded, then no transition in ample(s) may reach a state that is on the search stack. Now we give some heuristics for calculating ample sets. The algorithm depends on the model of computation. We consider processes with shared variables and message passing with queues. By pci(s) we denote the program counter of process Pi in a state s. We use the following notation: * pre() is a set including all transitions such that there exists a state s for which enabled(s) and enabled((s)). * dep() = { | (, ) D} is the set of all transitions that are dependent on . * Ti is the set of transitions of process Pi. * Ti(s) = Ti enabled(s). * currenti(s) is the set of all transitions of Pi that are enabled in some s such that pci(s) = pci(s ). Hence, Ti(s) currenti(s). In fact, we do not need to compute the sets pre() and dep() precisely. We preffer to efficiently compute over-approximations of these sets. We construct pre() as follows: * pre() includes the transitions of the processes that contain and that can change a program counter to a value from which can execute. 33 ˇ If the enabling condition for involves shared variables, then pre() includes all other transitions that can change these shared variables. * If sends or receives messages on some queue q, then pre() includes transitions of other processes that receive or send data through q, respectively. We construct dep() as follows: * Pairs of transitions that share a variable, which is changed by at least one of them, are dependent. * Pairs of transitions belonging to the same process are dependent. * Two send transitions that use the same message queue are dependent (sending a message may cause the queue to fill). Two receive transitions are also dependent. Note that a pair of send and receive transitions in different processes are independent as they can potentially enable each other, but not disable. An obvious candidate for ample(s) is Ti(s) (as transitions in Ti(s) are interdependent, ample(s) must include either all of them or none of them ­ see Lemma 7.5). To compute ample(s), we check whether some Ti(s) = satisfies the conditions C1, C2, and C3'. If there is no such Ti(s), we set ample(s) = enabled(s). Assume that condition C1 is violated for ample(s) = Ti(s). This means that some transitions independent of those in Ti(s) may be successively executed from s, eventually enabling a transition Ti(s) dependent on Ti(s). The independent transitions preceding cannot be in Ti since all transitions of Pi are considered as interdependent. There are two cases. 1. Tj for some i = j. Then dep(Ti(s)) Tj = . 2. Ti. Let s be the state where is enabled. The transitions executed on the path from s to s are independent of Ti(s) and hence, are from other processes. Therefore pci(s) = pci(s ) and this implies currenti(s). As Ti(s), we get currenti(s) Ti(s). As Ti(s), there has to be a transition of pre() included in the sequence from s to s . Hence, pre(currenti(s) Ti(s)) includes transitions of processes other than Pi. The following function checks whether ample(s) = Ti(s) satisfies C1. More precisely, if the function returns true, then C1 holds. Unfortunately, it may return false even if Ti(s) satisfies C1. function checkC1(s, Pi) forall Pi = Pj do if dep(Ti(s)) Tj = or pre(currenti(s) Ti(s)) Tj = then return false return true end function Functions for checking C2 and C3'and for calculating ample(s) are straightforward. function checkC2(X) forall X do if visible() then return false return true end function function checkC3'(s, X) forall X do if onStack((s)) then return false return true end function function ample(s) forall Pi such that Ti(s) = do if checkC1(s, Pi) and checkC2(Ti(s)) and checkC3'(s, Ti(s)) then return Ti(s) return enabled(s) end function 34 8 LTL model checking of pushdown systems In this section we demostrante the decidability of (state-based) LTL model checking problem for pushdown systems. Let us note that these systems can be used to precisely model sequential programs with procedure calls, recursion, and both local and global variables. This section is based on [EHRS00, Sch02]. Definition 8.1. A Pushdown system is a triple P = (P, , ), where * P is a finite set of control locations, * is a finite stack alphabet, * (P × ) × (P × ) is a finite set of transition rules. We write q, q , w instead of ((q, ), (q , w)) . Notice that we do not consider any input alphabet as we do not use pushdown systems as language acceptors. A configuration of P is a pair p, w P × , where w is a stack content (the topmost symbol is on the left). The set of all configurations is denoted by C. An immediate successor relation on configurations is defined in standard way. Reachability relation C × C is the reflexive and transitive closure of the immediate successor relation, while + C × C is the transitive closure of the immediate successor relation. Given a set C C of configurations, we define the set of their predecessors as pre (C) = {c C | c C . c c }. We use a sort of finite automata to represent sets of configurations. These automata use as an alphabet and P as a set of initial states (there is one initial state for every control location of the pushdown system). Formal definition follows. Definition 8.2. Given a pushdown system P = (P, , ), a P-automaton (or simply automaton) is a tuple A = (Q, , , P, F) where * Q is a finite set of states such that P Q, * Q × × Q is a set of transitions, * F Q is a set of final states. A (reflexive and transitive) transition relation Q × × Q is again defined in a standard way. P-automaton A represents the set of configurations Conf (A) = { p, w | q F . p w q}. A set of configurations of P is called regular if it is recognized by some P-automaton. In the rest of this section, we use symbols p, p , p , . . . to denote initial states of an automaton (i.e. elements of P). Non-initial states are denoted by s, s , s , . . ., and arbitrary states (initial or not) by q, q , q , . . .. 8.1 Computing pre (C) for a regular set C We show that, given a P and a P-automaton A defining a regular set C of configurations, then the set pre (C) is again regular and the corresponding automaton Apre is effectively constructible. Without loss of generality we assume that A has no transition leading to an initial state. The automaton Apre is obtained from A by addition of new transitions according to the following saturation rule: If p, p , w and p w q in the current automaton, add a transition (p, , q). 35 ?>=<89:;p0 0 GG ?>=<89:;s1 0 GG ?>=<89:;76540123s2 ?>=<89:;p0 0 GG 1 o 33 ?>=<89:;s1 0 GG ?>=<89:;76540123s2 ?>=<89:;p1 ?>=<89:;p1 1 WWsssssss 1 `` ?>=<89:;p2 ?>=<89:;p2 2 YY = { p0, 0 p1, 10 , p2, 2 p0, 1 , p1, 1 p2, 20 , p0, 1 p0, } Figure 19: Automata A (left) and Apre . We apply this rule repeatedly until we reach a fixpoint (there is a fixpoint as the number of possible new transitions is finite). The resulting P-automaton is Apre . Figure 19 provides an example of a P-automaton A and the resulting automaton Apre . A pushdown system is in normal form if every rule p, p , satisfies |w| 2. The efficient algorithm given in Figure 20 works only with pushdown systems in normal form. This is not a real restiction as any pushdown system can be put into this form with only linear size increase. The algorithm computes just transitions of Apre . The rest of the automaton is identical to A. The algorithm uses sets rel and trans containing the transitions that are known to belong to Apre : the set rel contains transitions that have already been examined. No transition is examined more than once. When we have a rule p, p , and transitions t1 = (p , , q ) and t2 = (q , , q ) (where q, q are arbitrary states), we have to add transition (p, , q ). We do it in such a way that Input: a pushdown system P = (P, , ) in normal form a P-automaton A = (Q, , , P, F) without transitions into P Output: the set of transitions of Apre 1 rel := ; trans := ; := ; 2 forall p, p , do trans := trans {(p, , p )}; 3 while trans = do 4 pop t = (q, , q ) from trans; 5 if t rel then 6 rel := rel {t}; 7 forall p1, 1 q, ( ) do 8 trans := trans {(p1, 1, q )}; 9 forall p1, 1 q, 2 do 10 := { p1, 1 q , 2 }; 11 forall (q , 2, q ) rel do 12 trans := trans {(p1, 1, q )}; 13 return rel Figure 20: Algorithm for computing pre (C). 36 whenever we examine t1, we check whether there is a corresponding t2 rel and we add an extra rule p, q , to a set of such extra rules . This extra rule guarantees that if a suitable t2 will be examined in the future, the transition (p, , q ) will be added. Theorem 8.3. Let P = (P, , ) be a pushdown system and A = (Q, , , P, F) be a P-automaton. There exists an automaton Apre recognizing pre (Conf (A)). Moreover, Apre can be constructed in O(|Q|2 ||) time and O(|Q| || + ||) space. Proof. We can assume that every transition is added to trans at most once. This can be done (without asymptotic loss of time) by storing all transitions which are ever added to trans in an additional hash table. Further, we assume that there is at least one rule in for every (transitions of A under some not satisfying this assumption can be moved directly to rel). The number of transitions in as well as the number of iterations of the while-loop is bounded by |Q|2 ||. Line 10 is executed for each combination of a rule p1, 1 q, 2 and a transition (q, , q ) trans, i.e. at most |Q| || times. Hence, | | |Q| ||. For the loop starting at line 11, q and 2 are fixed. Thus, line 12 is executed at most |Q|2 || times. Line 8 is executed for each combination of a rule p1, 1 q, ( ) and a transition (q, , q ) trans. We already know that | | |Q| ||, hence line 8 is executed at most O(|Q|2 ||) times. As a conclusion, the algorithm takes O(|Q|2 ||) time. Memory is needed for storing rel, trans, and . The size of is in O(|Q| ||). Line 1 adds || transitions to trans. Line 2 adds at most || transitions to trans. In lines 8 and 12, p1 and 1 are given by the head of a rule in (note that every rule in have the same head as some rule in ). Hence, lines 8 and 12 add at most |Q| || different transitions. We directly get that the algorithm needs O(|Q|||+||) space. As this is also the size of the result rel, the algorithm is optimal with respect to the memory usage. 8.2 LTL model checking This subsection deals with the global state-based model checking problem for LTL and pushdown processes, i.e. to compute the set of all configurations of a given pushdown system P that violate a given LTL formula (where a configuration c violates if there is a path starting from c and not satifying ). To talk about LTL properties, we need to enrich the formalism of pushdown systems with a labelling function L : (P × ) 2AP assigning to each pair (p, ) of a control location and a stack symbol a set of atomic propositions that are true of it. The labelling function can be directly extended to configurations such that L( p, w ) = L(p, ). In other words, the set of atomic propositions valid in a configuration is determined by the control location and the topmost stack symbol. Definition of a Kripke structure induced by a pushdown system enriched with a labelling function is now straightforward (the set of initial states is not important as we are interested in global model checking problem). To show that the problem is decidable, we reduce it to accepting run problem first. As in the automata-based approach to LTL model checking of finite-state systems, we first translate into a corresponding B¨uchi automaton B = (2AP() , Q, , q0, F) and then we make a product of this automaton and the pushdown system. The result of the product is called B¨uchi pushdown system, which is basically a pushdown system extended with a set of accepting control locations. The B¨uchi pushdown system given 37 as product of a pushdown system P = (P, , ) with a labelling function L, and a B¨uchi automaton B = (2AP() , Q, , q0, F), is defined as BP = ((P × Q), , , G), where (p, q), (p , q ), w if p, p , w and q (q, L(p, ) AP()) and G = P × F. An accepting run of a BP is a path passing through some accepting control location infinitely often. Clearly, a configuration p, w of P violates if BP has an accepting run starting from (p, q0), w . Hence, it is sufficient to solve the following accepting run problem: Compute the set Ca of configurations c of BP such that BP has an accepting run starting from c (i.e. a run which visits infinitely often configurations with control locations in G). Now we define some terms useful for characterization of the configurations from which there are accepting runs. Definition 8.4. Let BP = (P, , , G) be a B¨uchi pushdown system. The relation r between configurations of BP is defined as follows: c r c if c g, u + c for some configuration g, u with g G. The head of a transition rule p, p , w is the configuration p, . A head p, is repeating if there exists v such that p, r p, v . The set of repeating heads of BP is denoted by R. Lemma 8.5. Let c be a configuration of a B¨uchi pushdown system BP = (P, , , G). BP has an accepting run starting from c if and only if there exists a repeating head p, such that c p, w for some w . Proof. The implication "=" is obvious. Let us now assume that BP has an accepting run starting from from c and going through configurations p0, w0 , p1, w1 , p2, w2 , . . .. We construct a strictly increasing sequence of indices i0, i1, . . . as follows: * |wi0 | = min{|wj| | j 0} * |wik | = min{|wj| | j > ik-1} for k > 0 In other words, once a configuration pik , wik is reached, the rest of the run never looks at or changes the bottom |wik |-1 stack symbols. Let ik be the topmost symbol of wik for each k 0. As the number of pairs (pik , ik ) is bounded by |P × |, there has to be a pair (p, ) repeated ininitely many times. Moreover, since some g G becomes a control location infinitely often, we can select two indeces j1 < j2 out of i0, i1, . . . such that pj1 , wj1 = p, w r pj2 , wj2 = p, vw for some w, v . As w is never looked at or changed in the rest of the run, we have that p, r p, v . This proves the implication "=". The lemma directly implies that the set of all configurations violating the considered formula can be computed as pre (R ), where R = { p, w | p, R, w }. As the set R of repeating heads is finite, the set R is clearly regular. As we already have an algorithm computing pre (C) for a given regular set C, the only remaining step to solve the global model checking problem is the algorithm computing the set R. The problem of finding the repeating heads is reduced to a graph-theoretic problem. Given a BP = (P, , , G), we construct a head reachability graph G = (P × , E) whose nodes are the heads of BP. The set of edges E (P × ) × {0, 1} × (P × ) corresponds to the reachability relation between heads. We define G(p) = 1 if p G and G(p) = 0 otherwise. E consists of the following edges: 38 If p, p , v1 v2 and p , v1 p , then ((p, ), G(p), (p , )) E. Moreover, if p , v1 r p , then ((p, ), 1, (p , )) E. The instances satisfying p , v1 p , or p , v1 r p , can be found with the algorithm for pre ({ p , }) or its small modification, respectively. Once the graph G is constructed, R can be computed by exploiting the fact that some head p, is repeating if and only if (p, ) is part of a strongly connected component of G which has an internal edge labelled with 1. WVUTPQRSp0, 0 0 GG WVUTPQRSp1, 1 1 oo 0 WVUTPQRSp0, 1 WVUTPQRSp2, 2 1oo = { p0, 0 p1, 10 , p2, 2 p0, 1 , p1, 1 p2, 20 , p0, 1 p0, } Figure 21: The graph G for BP = ({p0, p1, p2}, {0, 1, 2}, , {p2}). Figure 21 provides a graph G constructed for the B¨uchi pushdown system BP = ({p0, p1, p2}, {0, 1, 2}, , {p2}). The repeating heads are p0, 0 and p1, 1 . An efficient algorithm for computing the set R of repeating head is formulated in Figure 22. This algorithm assumes that the BP on input is in normal form. The algorithm runs in two phases. During the first phase, it computes the automaton Apre recognizing the set pre ({ p, | p P}). Every transition (p, , p ) of Apre signifies that p, p , . As we also need the information whether p, r p , , we enrich the alphabet of Apre : transitions of the form (p, , p ) are replaced by (p, [, b], p ) where b is a boolean. The meaning of a transition (p, [, 1], p ) should be that p, r p , . The second phase of the algorithm constructs the graph G, identifies its strongly conected components (e.g. using Tarjan's algorithm [Tar72]), and determines the set of repeating heads. Theorem 8.6. Let BP = (P, , , G) be a B¨uchi pushdown system. The set of repeating heads R can be computed in O(|P|2 ||) time and O(|P| ||) space. Proof. The first part of the algorithm is essentially the same as the algorithm computing Apre . The size of G is in O(|P| ||). Determining the strongly connected components takes linear time in the size of the graph [Tar72]. The same holds for searching each component for an internal 1-edge. Now we have all necessary components to solve the global model checking problem. Theorem 8.7. Let P be a pushdown system and be an LTL formula. The global model checking problem can be solved in O(|P|3 |B|3 ) time and O(|P|2 |B|2 ) space, where B is a B¨uchi automaton corresponding to . Proof. For proof see [Sch02]. 39 Input: a B¨uchi pushdown system BP = (P, , , G) in normal form Output: the set of repeating heads in BP 1 rel := ; trans := ; := ; 2 forall p, p , do 3 trans := trans {(p, [, G(p)], p )}; 4 while trans = do 5 pop t = (p, [, b], p ) from trans; 6 if t rel then 7 rel := rel {t}; 8 forall p1, 1 p, do 9 trans := trans {(p1, [1, b G(p1)], p )}; 10 forall p1, 1 b - p, do 11 trans := trans {(p1, [1, b b ], p )}; 12 forall p1, 1 p, 2 do 13 := { p1, 1 bG(p1) - p , 2 }; 14 forall (p , [2, b ], p ) rel do 15 trans := trans {(p1, [1, b b G(p1)], p )}; 16 17 R := ; E := ; 18 forall p, p , do E := E {((p, ), G(p), (p , ))}; 19 forall p, b - p , do E := E {((p, ), b, (p , ))}; 20 forall p, p , do E := E {((p, ), G(p), (p , ))}; 21 find all strongly connected components in G = ((P × ), E); 22 forall components C do 23 if C has a 1-edge then R := R C; 24 return R Figure 22: Algorithm for computing the set of repeating heads. 8.3 Notes Similarly to the definition of pre (C), we can also define the set post (C) of successor of configurations in C. If C is regular, then post (C) is regular as well. Theorem 8.8. Let P = (P, , ) be a pushdown system and A = (Q, , , P, F) be a P-automaton. There exists an automaton Apost recognising post (Conf (A)). Moreover, Apost can be constructed in O(|P| || (|Q| + ||) + |P| ||) time and space. 9 Abstraction Please use slides as the study material for this topic. References [BDLS80] Timothy A. Budd, Richard A. DeMillo, Richard J. Lipton, and Frederick G. Sayward. Theoretical and empirical studies on using program mutation to 40 test the functional correctness of programs. In Conference Record of the Seventh ACM Symposium on Principles of Programming Languages (POPL '80), pages 220­233. ACM Press, 1980. [CGP99] Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model Checking. The MIT Press, 1999. [EHRS00] Javier Esparza, David Hansel, Peter Rossmanith, and Stefan Schwoon. Efficient algorithms for model checking pushdown systems. In E. Allen Emerson and A. Prasad Sistla, editors, Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000, Proceedings, volume 1855 of Lecture Notes in Computer Science, pages 232­ 247. Springer, 2000. [Flo67] Robert W. Floyd. Assigning meanings to programs. In J. T. Schwartz, editor, Mathematical Aspects of Computer Science, volume 19 of Proceedings of Symposia in Applied Mathematics, pages 19­32. American Mathematical Society, 1967. [Hoa69] C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576­580, 583, 1969. [Lam83] Leslie Lamport. What good is temporal logic? In R. E. A. Mason, editor, Proceedings of the IFIP Congress on Information Processing, pages 657­ 667, Amsterdam, 1983. North-Holland. [May98] Richard Mayr. Decidability and Complexity of Model Checking Problems for Infinite-State Systems. PhD thesis, Technische Universit¨at M¨unchen, 1998. [May00] Richard Mayr. Process rewrite systems. Information and Computation, 156(1):264­286, 2000. [MBT] Model-based testing. https://www.goldpractices.com/practices/mbt/. [MP83] Zohar Manna and Amir Pnueli. How to cook a temporal proof system for your pet language. In Conference Record of the Tenth Annual ACM Symposium on Principles of Programming Languages, pages 141­154. ACM Press, 1983. [MSS88] David E. Muller, Ahmed Saoudi, and Paul E. Schupp. Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In Proceedings of the 3rd IEEE Symposium on Logic in Computer Science (LICS 1988), pages 422­427. IEEE Computer Society Press, 1988. [Pel01] Doron Peled. Software Reliability Methods. Springer, 2001. [Pel06] R. Pel´anek. Reduction and Abstraction Techniques for Model Checking. PhD thesis, Faculty of Informatics, Masaryk University, Brno, 2006. [ˇReh07] Vojtˇech ˇReh´ak. On Extensions of Process Rewrite Systems. PhD thesis, Masaryk University, Brno, 2007. [RW85] Sandra Rapps and Elaine J. Weyuker. Selecting software test data using data flow information. IEEE Transactions on Software Engineering, 11(4):367­375, 1985. [Sch02] Stefan Schwoon. Model-Checking Pushdown Systems. PhD thesis, Technische Universit¨at M¨unchen, 2002. [SDV] Static driver verifier. http://www.microsoft.com/whdc/devtools/tools/sdv.mspx. [SPI] Spin model checker. http://www.spinroot.com. [Tar72] Robert Endre Tarjan. Depth-first search and linear graph algorithms. SIAM J. Comput, 1(2):146­160, 1972. 41 [Var95] Moshe Y. Vardi. An automata-theoretic approach to linear temporal logic. In Faron Moller and Graham M. Birtwistle, editors, Banff Higher Order Workshop, volume 1043 of Lecture Notes in Computer Science, pages 238­ 266. Springer, 1995. 42