|
COPYRIGHT 2000 Association for Computing Machinery, Inc.
1. INTRODUCTION
Temporal logics, which are modal logics geared toward the description of the temporal ordering of events, have been adopted as a powerful tool for specifying and verifying concurrent programs [Pnueli 1977; 1981]. One of the most significant developments in this area is the discovery of algorithmic methods for verifying temporal-logic properties of finite-state programs [Clarke et al. 1986; Lichtenstein and Pnueli 1985; Queille and Sifakis 1981]. This derives its significance both from the fact that many synchronization and communication protocols can be modeled as finite-state programs, as well as from the great ease of use of fully algorithmic methods. Finite-state programs can be modeled by transition systems where each state has a bounded description, and hence can be characterized by a fixed number of boolean atomic propositions. This means that a finite-state program can be viewed as a finite propositional Kripke structure, and its properties can be specified using propositional temporal logic. Thus, to verify the correctness of the program with respect to a desired behavior, one only has to check that the program, modeled as a finite Kripke structure, satisfies (is a model of) the propositional temporal logic formula that specifies that behavior. Hence the name model checking for the verification methods derived from this viewpoint [Clarke et al. 1999].
We distinguish between two types of temporal logics: linear and branching [Lamport 1980]. In linear temporal logics, each moment in time has a unique possible future, while in branching temporal logics, each moment in time may split into several possible futures. The complexity of model checking for both linear and branching temporal logics is well understood: suppose we are given a program of size n and a temporal logic formula of size m. For a branching temporal logic such as CTL, model-checking algorithms run in time O(nm) [Clarke et al. 1986], while, for linear temporal logic such as LTL, model-checking algorithms run in time n[2.sup.O(m)] [Lichtenstein and Pnueli 1985]. Since model checking with respect to a linear temporal logic formula is PSPACE-complete [Sistla and Clarke 1985], the latter bound probably cannot be improved. The difference in the complexity of linear and branching model checking has been viewed as an argument in favor of the branching paradigm.
Model checking suffers, however, from the so-called state-explosion problem. In a concurrent setting, the program under consideration is typically the parallel composition of many modules. As a result, the size of the state space of the program can be the product of the sizes of the state spaces of the participating modules. This gives rise to state spaces of exceedingly large sizes, which makes even linear-time algorithms impractical. This issue is one of the most important in the area of computer-aided verification and is the subject of active research (cf. Burch et al. [1990]).
Modular verification is one possible way to address the state-explosion problem, cf. Clarke et al. [1989], Aziz et al. [1994], and Kurshan [1987]. In modular verification, one uses proof rules of the following form:
[M.sub.1] ?? [[Psi].sub.1]} [M.sub.2] ?? [[Psi].sub.2]} C([[Psi].sub.1], [[Psi].sub.2], [Psi]} [[M.sub.1] [parallel] [[M.sub.2] ?? [Psi]
Here, M ?? [Theta] means that the module M satisfies the formula [Theta], the symbol "[parallel]" denotes parallel composition, and C([[Psi].sub.1], [[Psi].sub.2], [Psi]) is some logical condition relating [[Psi].sub.1], [[Psi].sub.2], and [Psi]. Using modular proof rules enables one to apply model checking only to the underlying modules, which have much smaller state spaces.
The state-explosion problem is only one motivation for pursuing modular verification. Modular verification is advocated also for other methodological reasons; a robust verification methodology should provide rules for deducing properties of programs from the properties of their constituent modules. Indeed, efforts to develop modular verification frameworks were undertaken in the mid 1980s [Pnueli 1985b].
A key observation (see Lamport [1983], Jones [1983], Misra and Chandy [1981], Stark [1984], and Pnueli [1985b]) is that in modular verification the specification should include two parts. One part describes the desired behavior of the module. The other part describes the assumed behavior of the system within which the module is interacting. This is called the assume-guarantee paradigm, as the specification describes what behavior the module is guaranteed to exhibit, assuming that the system behaves in the promised way.
For the linear temporal paradigm, an assume-guarantee specification is a pair ([Psi], [Psi]), where both [Psi] and [Psi] are linear temporal logic formulas. The meaning of such a pair is that all the computations of the module are guaranteed to satisfy [Psi], assuming that all the computations of the environment satisfy [Psi]. As observed in Pnueli [1985b], in this case the assume-guarantee pair can be combined to a single linear temporal logic formula [Psi] [right arrow], [Psi] (see also Jonsson and Tsay [1995]). Thus, model checking a module with respect to assume-guarantee specifications in which both the assumed and the guaranteed behaviors are linear temporal logic formulas is essentially the same as model checking the module with respect to linear temporal logic formulas.
The situation is different for the branching temporal paradigm. Here the guarantee is a branching temporal formula, which describes the computation tree of the module. There are two approaches, however, to the assumptions in assume-guarantee pairs. The first approach, implicit in Clarke et al. [1986] and Emerson and Lei [1985; 1987], and made explicit in Josko [1987a; 1987b; 1989], and Damm et al. [1989], is that the assumption in the assume-guarantee pair concerns the interaction of the module with its environment along each computation, and is therefore more naturally expressed in linear temporal logic. Thus, in this approach, an assume-guarantee pair should consist of a linear temporal assumption [Psi] and a branching temporal guarantee [Psi]. The meaning of such a pair is that [Psi] holds in the computation tree that consists of all computations of the program that satisfy [Psi]. The problem of verifying that a given module M satisfies such a pair , which we call the linear-branching modular model-checking problem, is more general than either linear or branching model checking.
A second approach was considered in Grumberg and Long [1994], where assumptions are taken to apply to the computation tree of the system within which the module is interacting. Accordingly, assumptions in Grumberg and Long [1994] are also expressed in branching temporal logic. There, a module M satisfies an assume-guarantee pair if and only if whenever M is part of a system satisfying [Psi], the system satisfies [Psi] too. We call this branching modular model checking. Furthermore, it is argued there, as well as in Datum et al. [1989], Josko [1989], Grumberg and Long [1991], and Dams et al. [1993], that in the context of modular verification it is advantageous to use only universal branching temporal logic, i.e., branching temporal logic without existential path quantifiers. That is, in a universal branching temporal logic one can state properties of all computations of a program, but one cannot state that certain computations exist. Consequently, universal branching temporal logic formulas have the helpful property that once they are satisfied in a module, they are satisfied also in a system that contains this module. The focus in Grumberg and Long [1994] is on using [inverted] ACTL, the universal fragment of CTL, for both the assumption and the guarantee.
In this paper, we focus on the branching modular model-checking problem, which we show to be a proper extension of the linear-branching modular model-checking problem. We consider assumptions and guarantees in both [inverted] ACTL and in the more expressive [inverted] ACTL*. We start by examining the most fundamental questions about these logics: satisfiability, validity, and implication (since [inverted] ACTL and [inverted] ACTL* are not closed under negation, these problems are not interreducible as they are for CTL and CTL*). Solving the satisfiability and validity problems enables us to check that a specification is not trivially true or false. Implication generalizes these questions and is strongly related to modular model checking. Recall that in the linear framework, checking an assume-guarantee pair in a module M is equivalent to checking whether M satisfies the implication [Psi] [right arrow], [Psi]. In the branching framework, we show here that an assume-guarantee pair holds in a universal module that exhibits all possible behaviors if and only if the implication [Psi] [right arrow] [Psi] is valid.
We use two fundamental techniques to solve these questions. The first technique is the maximal-model technique introduced in Grumberg and Long [1994]. It is shown there that with every [inverted] ACTL formula [Psi] one can associate a maximal model [M.sub.[Psi]] (called the tableau of [Psi] in Grumberg and Long [1994]) such that a module M satisfies [Psi] precisely when M simulates [M.sub.[Psi]] (we define simulation later on). We use here automata-theoretic techniques for CTL* [Vardi and Stockmeyer 1985; Emerson and Jutla 1988] to construct maximal models for [inverted] ACTL* formulas. While maximal models for [inverted] ACTL involve an exponential blow-up, maximal models for [inverted] ACTL* involve a doubly exponential blow-up.
The second technique is the automata-theoretic framework to branching-time model checking introduced in Kupferman et al. [2000]. It is shown there how to use alternating tree automata to obtain space-efficient model checking methods. Since the maximal models that we construct include fairness conditions, we extend the automata-theoretic method of Kupferman et al. [2000] to yield space-efficient fair model-checking algorithms. We then show how performing fair model checking over maximal models can solve the satisfiability, validity, and implication problems for [inverted] ACTL and [inverted] ACTL*. Our results show that these problems are computationally easier than the analogous problems for CTL and CTL*. For example, while all three problems are EXPTIME-complete for CTL, we have that satisfiability and implication are PSPACE-complete and validity is NP-complete for [inverted] ACTL.
By relating the implication problem with the branching modular model-checking problem, we show that the same two fundamental techniques of maximal models and space-efficient fair model checking also yield a solution to the latter problem. We prove that the problem is PSPACE-complete for [inverted] ACTL and is EXPSPACE-complete for [inverted] ACTL*. We show that the increase in complexity is solely due to the assumption part of the specification. This suggests that modular model checking in the branching temporal framework can be practical only for very small assumptions.
We turn on to investigate the linear-branching modular model-checking problem. Recall that the problem is a special case of the branching modular model-checking problem. While this suggests an EXPSPACE upper bound for the problem, which we prove to be tight, we show that the linear-branching setting is essentially simpler. Using the automata-theoretic framework for linear temporal logics [Vardi and Wolper 1986], we describe an algorithm for the linear-branching modular model-checking problem that allows the branching guarantee to be any CTL or CTL* formula (that is, it is not restricted to their universal fragments) and avoids the construction of maximal models. An even simpler construction, which avoids the use of determinization, is described in Vardi [1995].
2. PRELIMINARIES
2.1 The Temporal Logics LTL, CTL*, and CTL
The logic LTL is a linear temporal logic. Formulas of LTL are built from a set AP of atomic proposition using the usual Boolean operators and the temporal operators X ("next time"), U ("until"), and U ("duality of until"). We present here a positive normal form in which negation may be applied only to atomic propositions. Given a set AP, an LTL formula is defined as follows:
--true, false, p, or ??p, for p [element of] AP.
--[Psi] [disjunction] [Psi], [Psi] [conjunction] [Psi], X[Psi], [Psi]U[Psi], or [Psi]U[Psi], where [Psi] and [Psi] are LTL formulas.
We define the semantics of LTL with respect to a computation [Pi] = [[Sigma].sub.0], [[Sigma].sub.1], [[Sigma].sub.2], ..., where for every j [is greater than or equal to] 0, we have that [[Sigma].sub.j] is a subset of AP, denoting the set of atomic propositions that hold in the jth position of [Pi]. We denote the suffix [[Sigma].sub.j], [[Sigma].sub.j]+1, ... of [Pi] by [[Pi].sup.j]. We use [Pi] ?? [Psi] to indicate that an LTL formula [Psi] holds in the path [Pi].
The relation ?? is inductively defined as follows:
--For all [Pi], we have that [Pi] ?? true and [Pi] ?? false.
--For an atomic proposition p [element of] AP, we have [Pi] ?? p if and only if p [element of] [[Sigma].sub.0] and Pi] ?? ??p if and only if p [is not an element of] [[Sigma].sub.0].
--[Pi] ?? [Psi] [disjunction] [Psi] if and only if [Pi] ?? [Psi] or [Pi] ?? [Psi].
--[Pi] ?? [Psi] [conjunction] [Psi] if and only if [Pi] ?? [Psi] and [Pi] ?? [Psi].
--[Pi] ?? X [Psi] if and only [[Phi].sup.1] ?? [Psi].
--[Pi] ?? [Psi]U[Psi] if and only if there exists k [is greater than or equal to] such that [[Pi].sup.k] ?? [Psi] and [[Pi].sup.i] ?? [Psi] for all [is less than or equal to] i [is less than] k.
--[Pi] ?? [Psi]U[Psi] if and only if for every k [is greater than or equal to] for which [[Pi].sup.k] ?? [Psi], there exists [is less than or equal to] i [is less than] k such that [[Pi].sup.??] ?? [Psi].
We denote the length of a formula [Psi] by |[Psi]|, and we use the following abbreviations in writing formulas:
--[right arrow] and [equivalence], interpreted in the usual way (that is [Psi] [right arrow] [Psi]=[Psi] [disjunction] ??[Psi], and [Psi] [equivalence] [Psi] = [Psi] [right arrow] [Psi] [conjunction] [Psi] [right arrow] [Psi]).
--F[Psi] = true U[Psi] ("eventually").
--G[Psi] = false U[Psi] ("always").
The logic CTL* is a branching temporal logic. A path quantifier, E ("for some path") or A ("for all paths"), can prefix an assertion composed of an arbitrary combination of linear time operators. There are two types of formulas in CTL*: state formulas, whose satisfaction is related to a specific state, and path formulas, whose satisfaction is related to a specific path. Formally, let AP be a set of atomic proposition names. ACTL* state formula (again, in a positive normal form) is either
--true, false, p or ??p, for p [element of] AP,
--[Psi] [disjunction] [Psi] or [Psi] [conjunction] [Psi] where [Psi] and [Psi] are CTL* state formulas, or
--E[Psi] or A[Psi], where [Psi] is a CTL* path formula.
ACTL* path formula is either
--ACTL* state formula, or
--[Psi] [disjunction] [Psi], [Psi] [conjunction] [Psi], X[Psi], [Psi]U[Psi], or [Psi]U[Psi], where [Psi] and [Psi] are CTL* path formulas.
The logic CTL* consists of the set of state formulas generated by the above rules. The logic CTL is a restricted subset of CTL*. In CTL, the temporal operators X, U, and U must be immediately preceded by a path quantifier. Formally, it is the subset of CTL* obtained by restricting the path formulas to be X[Psi], [Psi]U[Psi], or [Psi]U[Psi], where [Psi] and [Psi] are CTL state formulas.
The logic [inverted] ACTL* is a restricted subset of CTL* that allows only the universal path quantifier A. Note that since negation in CTL* can be applied only to atomic propositions, assertions of the form ??A[Psi], which is equivalent to E??[Psi], are not possible. Thus, the logic [inverted] ACTL* is not closed under negation. The logic [inverted] ACTL is defined similarly, as the restricted subset of CTL that allows the universal path quantifier only. The logics [exists]CTL* and [exists]CTL are defined analogously, as the existential fragments of CTL* and CTL, respectively. Note that negating a [inverted] ACTL* formula results in an [exists]CTL* formula. For example, ??ApU(AXq) is equivalent to E(??p)U(EX ??q). Conversely, negating a [exists]CTL* formula results in an [inverted] ACTL* formula.
The closure cl([Psi]) of a CTL* formula [Psi] is the set of all state subformulas of [Psi](including [Psi] but excluding true and false). For example, cl(E(pU(AXq))) = {E(pU(AXq)),p, AXq, q}. It is easy to see that the size of cl([Psi]) is linear in the size of [Psi]. We say that a CTL* formula [Psi] is a U-formula if it is of the form [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] or [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. The subformula [[Psi].sub.2] is then called the eventuality of [Psi]. Similarly, [Psi] is a U-formula if it is of the form [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. We denote by AU([Psi]) the set of formulas of the from [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] in cl([Psi]). The sets EU([Psi]), AU([Psi]), and EU([Psi]) are defined similarly.
We define the semantics of CTL* (and its sublanguages) with respect to fair Rabin modules (fair modules, for short). A fair module M = (AP, W, R, [W.sub.0], L, [Alpha]) consists of a set AP of atomic propositions, a set W of states, a transition relation R [subset or equal to] W x W, a set [W.sub.0] [subset or equal to] W of initial states, a labeling function L: W [right arrow] [2.sup.AP], and a Rabin fairness condition [Alpha] [subset or equal to] [2.sup.Q] x [2.sup.Q] that defines a subset of [W.sup.w] (the exact semantics of [Alpha] is given shortly). Our choice of this type of fairness condition is technically motivated, as will be clarified in the sequel. For a state w [element of] W, we use bd(w) to denote the branching degree of w, i.e., the number of different R-successors that w has.
A computation of a fair module is an infinite sequence of states, [Pi] = [w.sub.0], [w.sub.1], ... such that for every i [is greater than or equal to] 0, we have that <[w.sub.i],[w.sub.i+1] [element of] R. We extend the labeling function L to computations and denote by L([Pi]) the word L([w.sub.0]) [multiplied by] L([w.sub.1]).... For a computation [Pi], let inf([Pi]) denote the set of states that repeat infinitely often in [Pi], i.e.,
inf([Pi]) = {w: for infinitely many i [is greater than or equal to] 0, we have [w.sub.i] = w}.
A computation of M is fair if and only if it satisfies the fairness condition [Alpha]. Thus, if [Alpha] = { , ..., }, then [Pi] is fair if and only if there exists 1 [is less than or equal to] i [is less than or equal to] k such that inf([Pi]) [intersection] [G.sub.i] [is not equal to] and inf([Pi]) [intersection] [B.sub.i] = 0, in other words, if and only if [Pi] visits [G.sub.i] infinitely often and visits [B.sub.i] only finitely often. We say that a fair module is nonempty if and only if there exists a fair computation that starts at an initial state. A module is a fair module with no fairness condition. That is, all the computations of a module are considered fair. We denote a module by M = . We define the size |M|, of a fair module or a module M as above as |W|+|R|+|[W.sub.0|. Thus, the definition of |M| ignores the labeling function and the fairness condition. When the module is fair, we refer to the number of pairs in [Alpha] as the degree of M.
We use w ?? [Psi] to indicate that a state formula [Pi] holds at state w (assuming an agreed fair module M). The relation ?? is inductively defined as follows (the relation [Pi] ?? [Psi] for a path formula [Psi] is the same as for [Psi] in LTL).
--For all w, we have that w ?? true and w ?? false.
--For an atomic proposition p [element of] AP, we have w ?? p if and only if p [element of] L(w) and w ?? ??p if and only if p [is not an element of] L(w).
--w ?? [Psi] [disjunction] [Psi] if and only if w ?? [Psi] or w ?? [Psi].
--w ?? [Psi] [conjunction] [Psi] if and only if w ?? [Psi] and w ?? [Psi].
--w ?? E[Psi] if and only if there exists a fair computation [Pi] = [w.sub.0], [w.sub.1], ... such that [w.sub.0] = w and [Pi] ?? [Psi].
--w ?? A[Psi] if and only if for all fair computations [Pi] = [w.sub.0], [w.sub.1], ... such that [w.sub.0] = w, we have [Psi] ?? [Psi].
--[Pi] ?? [Psi] for a computation [Pi] = [w.sub.0], [w.sub.1], ... and a state formula [Psi] if and only if [w.sub.0] ?? [Psi].
A fair module M satisfies a formula [Psi] if and only if [Psi] holds in all initial states of M. The problem of determining whether M satisfies [Psi] is the fair model-checking problem.
For technical convenience, we assume that the relation R is total; thus every state has at least one successor. We can ensure that R is total by adding to W a sink state [w.sub.sink] labeled by some atomic proposition sink not in AP, and adding transitions from all states to [w.sub.sink]. The atomic proposition sink then enables us to exclude computations that are not "real" computations of the original module. For example, by replacing an existential formula E[Psi], for a path formula [Psi], by the formula E([Psi] [conjunction] G??sink), we can make sure that the property [Psi] is satisfied along a computation of the original module. For a detailed description of this transformation see the treatment of the atomic proposition ?? in Section 3.2, where we restrict path quantification to computations in which ?? always holds. In particular, as noted there, the transformation involves only a linear blow up, and it can be enhanced (still with only a linear blow up) so that if the formula we start with is a CTL formula, so is the formula we end up with.
2.2 Simulation Relation and Composition of Modules
In the context of modular verification, it is helpful to define an order relation between fair modules [Grumberg and Long 1994]. Intuitively, the order captures what it means for a fair module M' to have "more behaviors" than a fair module M. Let M = and M' - be two fair modules for which AP' [subset or equal to] AP, and let w and w' be states in W and W', respectively. A relation H [subset or equal to]W x W' is a simulation relation from to if and only if the following conditions hold:
(1) H(w, w').
(2) For all s and s', we have that H(s, s') implies the following:
(a) L(s) [intersection] AP' = L(s').
(b) For every fair computation [Pi] = [s.sub.0], [s.sub.1], ... in M, with [s.sub.0] = s, there exists a fair computation [Pi]' = [s.sub.0], [s.sub.1], ... in M', with [s'.sub.0] = s', such that for all i [is greater than or equal to] 0, we have H([s.sub.i], [s'.sub.i]).
A simulation relation H is a simulation from M to M' if and only if for every w [element of] [W.sub.0] there exists w' [element of] [W'.sub.0] such that H is a simulation relation from to . If there exists a simulation from M to M', we...
Read the full article for free courtesy of your local library.
|
Bookmark this article
Print this article
Link to this article
Email this article
Digg It!
Add to del.icio.us
RSS
