# Augmenting branching temporal logics with existential quantification over atomic propositions

## 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## References

- [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 - [BCM+92]J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 10
^{20}states and beyond.*Information and Computation*, 98(2):142–170, June 1992.CrossRefGoogle Scholar - [Bry86]R.E. Bryant. Graph-based algorithms for boolean-function manipulation.
*IEEE Trans. on Computers*, C-35(8), 1986.Google Scholar - [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 - [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 - [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 - [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 - [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 - [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 - [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 - [Eme90]E.A. Emerson. Temporal and modal logic.
*Handbook of theoretical computer science*, pages 997–1072, 1990.Google Scholar - [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 - [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 - [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 - [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 - [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 - [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 - [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 - [Lon93]D.E. Long.
*Model checking, abstraction and compositional verification*. PhD thesis, Carnegie-Mellon University, Pittsburgh, 1993.Google Scholar - [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 - [Pnu81]A. Pnueli. The temporal semantics of concurrent programs.
*Theoretical Computer Science*, 13:45–60, 1981.CrossRefGoogle Scholar - [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 - [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 - [Sav70]W.J. Savitch. Relationship between nondeterministic and deterministic tape complexities.
*J. on Computer and System Sciences*, 4:177–192, 1970.Google Scholar - [Sis83]A.P. Sistla.
*Theoretical issues in the design of distributed and concurrent systems*. PhD thesis, Harward University, Cambridge, MA, 1983.Google Scholar - [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 - [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 - [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 - [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 - [Wol83]P. Wolper. Temporal logic can be more expressive.
*Information and Control*, 56(1–2):72–99, 1983.CrossRefGoogle Scholar