Advertisement

From pre-historic to post-modern symbolic model checking

Regular Papers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1427)

Abstract

Symbolic model checking, which enables the automatic verification of large systems, proceeds by calculating with expressions that represent state sets. Traditionally, symbolic model-checking tools arc based on backward state traversal; their basic operation is the function pre, which given a set of states, returns the set of all predecessor states. This is because specifiers usally employ formalisms with future-time modalities. which are naturally evaluated by iterating applications of pre. It has been recently shown experimentally that symbolic model checking can perform significantly better if it is based, instead, on forward state traversal; in this case, the basic operation is the function post, which given a set of states, returns the set of all successor states. This is because forward state traversal can ensure that only those parts of the state space are explored which are reachable from an initial state and relevant for satisfaction or violation of the specification; that is, errors can be detected as soon as possible.

In this paper, we investigate which specifications can be checked by symbolic forward state traversal. We formulate the problems of symbolic backward and forward model checking by means of two μ-calculi. The pre-μ calculus is based on the pre operation; the post-μ calculus, on the post operation. These two μ-calculi induce query logics, which augment fixpoint expressions with a boolean emptiness query. Using query logics, we are able to relate and compare the symbolic backward and forward approaches. In particular, we prove that all ω-regular (linear-time) specifications can be expressed as post-μ queries, and therefore checked using symbolic forward state traversal. On the other hand, we show that there are simple branching-time specifications that cannot be checked in this way.

Keywords

Model Check Linear Temporal Logic Kripke Structure Query Logic Symbolic Model Check 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. [BC96]
    G. Bhat and R. Cleavland. Efficient model checking via the equational μ-calculus. In Proc. 11th IEEE Symposium on Logic in Computer Science, pp. 304–312, 1996.Google Scholar
  2. [BCG88]
    M.C. Browne, E.M. Clarke, and O. Grumberg. Characterizing finite Kripke structures in propositional temporal logic. Theoretical Computer Science, 59:115–131, 1988.Google Scholar
  3. [BCM+92]
    J.R. Bunch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142–170, 1992.CrossRefGoogle Scholar
  4. [BHSV+96]
    R.K. Brayton, G.D. Hachtel, A. Sangiovanni-Vincentelli, F. Somenzi, A. Aziz, S.-T. Cheng, S. Edwards, S. Khatri, T Kukimoto, A. Pardo, S. Qadeer, R.K. Ranjan, S. Sarwary, T.R. Shiple, G. Swamy, and T. Villa. VIS: a system for verification and synthesis. In CAV 96: Computer Aided Verification, LNCS 1102, pp. 428–432, Springer, 1996.Google Scholar
  5. [Bry86]
    R.E. Bryant. Graph-based algorithms for boolean-function manipulation. IEEE Trans. on Computers, C-35(8), 1986.Google Scholar
  6. [CD88]
    E.M. Clarke and I.A. Draghicescu. Expressibility results for linear-time and branching-time logics. In Proc. Workshop on Linear Time, Branching Time, and Partial Order in Logics and Models for Concurrency, LNCS 354, pp. 428–437, Springer, 1988.Google Scholar
  7. [CE81]
    E.M. Clarke and E.A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proc. Workshop on Logic of Programs, LNCS 131, pp. 52–71, Springer, 1981.Google Scholar
  8. [CGH94]
    E.M. Clarke, O. Grumberg, and K. Hamaguchi. Another look at LTL model checking. In CAV 94: Computer Aided Verification, LNCS 818, pp. 415–427, Springer, 1994.Google Scholar
  9. [CGL93]
    E.M. Clarke, O. Grumberg, and D. Long. Verification tools for finite-slate concurrent systems. In Decade of Concurrency — Reflections and Perspectives (Proc. REX School), LNCS 803, pp. 124–175, Springer, 1993.Google Scholar
  10. [CS91]
    R. Cleaveland and B. Steffen. A linear-time model-checking algorithm for the alternation-free modal μ-calculus. In CAV 91: Computer Aided Verification, LNCS 575, pp. 48–58, Springer, 1991.Google Scholar
  11. [Dam94]
    M. Dam. CTL+ and ECTL+ as fragments of the modal μ-calculus. Theoretical Computer Science, 126:77–96, 1994.CrossRefMathSciNetGoogle Scholar
  12. [Dil96]
    David L. Dill. The Murø Verification System. In CAV 96: Computer Aided Verification, LNCS 1102, pp. 390–393, Springer, 1996.Google Scholar
  13. [EL86]
    E.A. Emerson and C.-L. Lei. Efficient model checking in fragments of the propositional μ-calculus. In Proc. 1st Symposium on Logic in Computer Science, pp. 267–278, 1986.Google Scholar
  14. [GK94]
    O. Grumberg and R.P. Kurshan. Flow linear can branching-time be. In Proc. 1st International Conference on Temporal Logic, LNAI 827, pp. 180–194, Springer, 1994.Google Scholar
  15. [GPVW95]
    R. Gerth, D. Peled, M.Y. Vardi, and R Wolper. Simple on-the-fly automatic verification of linear temporal logic. In Protocol Specification, Testing, and Verification, pp. 3–18, Chapman, 1995.Google Scholar
  16. [Hol97]
    G.J. Holzmann. The model checker SPIN. IEEE Trans. on Software Engineering, 23(5):279–295, 1997.CrossRefGoogle Scholar
  17. [IN97]
    H. Iwashita and T. Nakata. Forward model checking techniques oriented to buggy designs. In Proc. IEEE/ACM International Conference on Computer Aided Design, pp. 400–404, 1997.Google Scholar
  18. [INH96]
    H. Iwashita, T. Nakata, and F. Hirose. CTL model checking based on forward state traversal. In Proc. IEEE/ACM International Conference out Computer Aided Design, pp. 82–87, 1996.Google Scholar
  19. [Koz83]
    D. Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27:333–354, 1983.CrossRefGoogle Scholar
  20. [KP95]
    O. Kupferman and A. Pnueli. Once and for all. In Proc. 10th IEEE Symposium on Logic in Computer Science, pp. 25–35, 1995.Google Scholar
  21. [KV98]
    O. Kupferman and M.Y. Vardi. Freedom, weakness, and determinism: from linear-time to branching-lime. In Proc. 13th IEEE Symposium on Logic in Computer Science, 1998.Google Scholar
  22. [LPZ85]
    O. Lichtenstein, A. Pnueli, and L. Zuck. The glory of the past. In Logics of Programs, LNCS 193, pp. 196–218, Springer, 1985.Google Scholar
  23. [McM93]
    K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.Google Scholar
  24. [MP92]
    Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, 1992.Google Scholar
  25. [Pel94]
    D. Peled. Combining partial order reductions with on-the-fly model-checking. In CAV 94: Computer Aided Verification, LNCS 818, pp. 377–390, Springer, 1994.Google Scholar
  26. [QS81]
    J.P. Queille and J. Sifakis. Specification and verification of concurrent systems in Cesar. In Proc. 5th International Symp. on Programming, LNCS 137, pp. 337–351, Springer, 1981. [Var98] M.Y. Vardi. Reasoning about the past with two-way automata. In Proc. 25th International Coll. on Automata, Languages, and Programming, LNCS, Springer, 1998.Google Scholar
  27. [VW94]
    M.Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1–37, 1994.CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  1. 1.Department of EECSUniversity of California at BerkeleyUSA

Personalised recommendations