Advertisement

Augmenting branching temporal logics with existential quantification over atomic propositions

  • Orna Kupferman (Bernholtz)
Session 10: Invited Talk
Part of the Lecture Notes in Computer Science book series (LNCS, volume 939)

Abstract

In temporal-logic model checking, we verify the correctness of a program with respect to a desired behavior by checking whether a structure that models the program satisfies a temporal logic formula that specifies this behavior. One of the ways to overcome the expressiveness limitation of temporal logics is to augment them with quantification over atomic propositions. In this paper we consider the extension of branching temporal logics with existential quantification over atomic propositions. Once we add existential quantification to a branching temporal logic, it becomes sensitive to unwinding. That is, unwinding a structure into an infinite tree does not preserve the set of formulas it satisfies. Accordingly, we distinguish between two semantics, two practices as specification languages, and two versions of the model-checking problem for such a logic. One semantics refers to the structure that models the program, and the second semantics refers to the infinite computation tree that the program induces. We examine the complexity of the model-checking problem in the two semantics for the logics CTL and CTL* augmented with existential quantification over atomic propositions. Following the cheerless results that we get, we examine also the program complexity of model checking; i.e., the complexity of this problem in terms of the program, assuming the formula is fixed. We show that while fixing the formula dramatically reduces model-checking complexity in the tree semantics, its influence on the structure semantics is poor.

Keywords

Model Check Temporal Logic Linear Temporal Logic Atomic Proposition Structure Semantic 
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. [BBG+94]
    I. Beer, S. Ben-David, D. Geist, R. Gewirtzman, and M. Yoeli. Methodology and system for practical formal verification of reactive hardware. In Proc. 6th Workshop on Computer Aided Verification, volume 818 of Lecture Notes in Computer Science, pages 182–193, Stanford, June 1994.Google Scholar
  2. [BCM+92]
    J.R. Burch, 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, June 1992.CrossRefGoogle Scholar
  3. [Bry86]
    R.E. Bryant. Graph-based algorithms for boolean-function manipulation. IEEE Trans. on Computers, C-35(8), 1986.Google Scholar
  4. [BVW94]
    O. Bernholtz, M.Y. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. In Computer Aided Verification, Proc. 6th Int. Workshop, Stanford, California, June 1994. Lecture Notes in Computer Science, Springer-Verlag, full version available from authors.Google Scholar
  5. [CES86]
    E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, January 1986.CrossRefGoogle Scholar
  6. [CKS81]
    A.K. Chandra, D.C. Kozen, and L.J. Stockmeyer. Alternation. Journal of the Association for Computing Machinery, 28(1):114–133, January 1981.Google Scholar
  7. [CLM89]
    E.M. Clarke, D.E. Long, and K.L. McMillan. Compositional model checking. In Proc. 4th IEEE Symposium on Logic in Computer Science, pages 353–362, 1989.Google Scholar
  8. [CVWY92]
    C. Courcoubetis, M.Y. Vardi, P. Wolper, and M. Yannakakis. Memory efficient algorithms for the verification of temporal properties. Formal Methods in System Design, 1:275–288, 1992.CrossRefGoogle Scholar
  9. [EJ88]
    E.A. Emerson and C. Jutla. The complexity of tree automata and logics of programs. In Proceedings of the 29th IEEE Symposium on Foundations of Computer Science, White Plains, October 1988.Google Scholar
  10. [EL85]
    E.A. Emerson and C.-L. Lei. Modalities for model checking: Branching time logic strikes back. In Proceedings of the Twelfth ACM Symposium on Principles of Programming Languages, pages 84–96, New Orleans, January 1985.Google Scholar
  11. [Eme90]
    E.A. Emerson. Temporal and modal logic. Handbook of theoretical computer science, pages 997–1072, 1990.Google Scholar
  12. [ES84]
    E.A. Emerson and A. P. Sistla. Deciding branching time logic. In Proceedings of the 16th ACM Symposium on Theory of Computing, Washington, April 1984.Google Scholar
  13. [FL79]
    M.J. Fischer and R.E. Ladner. Propositional dynamic logic of regular programs. J. of Computer and Systems Sciences, 18:194–211, 1979.CrossRefGoogle Scholar
  14. [GL91]
    O. Grumberg and D.E. Long. Model checking and modular verification. In Proc. 2nd Conferance on Concurrency Theory, volume 527 of Lecture Notes in Computer Science, pages 250–265, Springer-Verlag, 1991.Google Scholar
  15. [HK94]
    J.Y. Halpern and B. Kapron. Zero-one laws for modal logic. Annals of Pure and Applied Logic, 69:157–193, 1994.Google Scholar
  16. [Imm81]
    N. Immerman. Number of quantifiers is better than number of tape cells. Journal of Computer and System Sciences, 22(3):384–406, 1981.Google Scholar
  17. [KP95]
    O. Kupferman and A. Pnueli. Once and for all. In Proc. 10th IEEE Symposium on Logic in Computer Science, San Diego, June 1995. To appear.Google Scholar
  18. [Lam80]
    L. Lamport. Sometimes is sometimes “not never” — on the temporal logic of programs. In Proceedings of the 7th ACM Symposium on Principles of Programming Languages, pages 174–185, January 1980.Google Scholar
  19. [Lon93]
    D.E. Long. Model checking, abstraction and compositional verification. PhD thesis, Carnegie-Mellon University, Pittsburgh, 1993.Google Scholar
  20. [LP85]
    O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Proceedings of the Twelfth ACM Symposium on Principles of Programming Languages, pages 97–107, New Orleans, January 1985.Google Scholar
  21. [Pnu81]
    A. Pnueli. The temporal semantics of concurrent programs. Theoretical Computer Science, 13:45–60, 1981.CrossRefGoogle Scholar
  22. [PR89]
    A. Pnueli and R. Rosner. On the synthesis of a reactive module. In Proceedings of the Sixteenth ACM Symposium on Principles of Programming Languages, Austin, Januery 1989.Google Scholar
  23. [PW84]
    S. Pinter and P. Wolper. A temporal logic for reasoning about partially ordered computations. In Proc. 3rd ACM Symposium on Principles of Distributed Computing, pages 28–37, Vancouver, August 1984.Google Scholar
  24. [Sav70]
    W.J. Savitch. Relationship between nondeterministic and deterministic tape complexities. J. on Computer and System Sciences, 4:177–192, 1970.Google Scholar
  25. [Sis83]
    A.P. Sistla. Theoretical issues in the design of distributed and concurrent systems. PhD thesis, Harward University, Cambridge, MA, 1983.Google Scholar
  26. [SVW87]
    A.P. Sistla, M.Y. Vardi, and P. Wolper. The complementation problem for Büchi automata with applications to temporal logic. Theoretical Computer Science, 49:217–237, 1987.CrossRefGoogle Scholar
  27. [VS85]
    M.Y. Vardi and L. Stockmeyer. Improved upper and lower bounds for modal logics of programs. In Proc 17th ACM Symp. on Theory of Computing, pages 240–251, 1985.Google Scholar
  28. [VW86]
    M.Y. Vardi and P. Wolper. Automata-theoretic techniques for modal logics of programs. Journal of Computer and System Science, 32(2):182–21, April 1986.Google Scholar
  29. [WG93]
    P. Wolper and P. Godefroid, Partial-order methods for temporal verification. In Proc. 4th Conferance on Concurrency Theory, volume 715 of Lecture Notes in Computer Science, pages 233–246, Hildesheim, August 1993. Springer-Verlag.Google Scholar
  30. [Wol83]
    P. Wolper. Temporal logic can be more expressive. Information and Control, 56(1–2):72–99, 1983.CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Orna Kupferman (Bernholtz)
    • 1
  1. 1.Department of Computer ScienceThe TechnionHaifaIsrael

Personalised recommendations