Extending Temporal Logics with Data Variable Quantifications

Authors Fu Song, Zhilin Wu

Thumbnail PDF


  • Filesize: 0.56 MB
  • 13 pages

Document Identifiers

Author Details

Fu Song
Zhilin Wu

Cite AsGet BibTex

Fu Song and Zhilin Wu. Extending Temporal Logics with Data Variable Quantifications. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 253-265, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)


Although data values are available in almost every computer system, reasoning about them is a challenging task due to the huge data size or even infinite data domains. Temporal logics are the well-known specification formalisms for reactive and concurrent systems. Various extensions of temporal logics have been proposed to reason about data values, mostly in the last decade. Among them, one natural idea is to extend temporal logics with variable quantifications ranging over an infinite data domain. In this paper, we focus on the variable extensions of two widely used temporal logics, Linear Temporal Logic (LTL) and Computation Tree Logic (CTL). Grumberg, Kupferman and Sheinvald recently investigated the extension of LTL with variable quantifications. They defined the extension as formulas in the prenex normal form, that is, all the variable quantifications precede the LTL formulas. Our goal in this paper is to do a relatively complete investigation on this topic. For this purpose, we define the extensions of LTL and CTL by allowing arbitrary nestings of variable quantifications, Boolean and temporal operators (the resulting logics are called respectively variable-LTL, in brief VLTL, and variable-CTL, in brief VCTL), and identify the decidability frontiers of both the satisfiability and model checking problem. In particular, we obtain the following results: 1) Existential variable quantifiers or one single universal quantifier in the beginning already entails undecidability for the satisfiability problem of both VLTL and VCTL, 2) If only existential path quantifiers are used in VCTL, then the satisfiability problem is decidable, no matter which variable quantifiers are available. 3) For VLTL formulas with one single universal variable quantifier in the beginning, if the occurrences of the non-parameterized atomic propositions are guarded by the positive occurrences of the quantified variable, then its satisfiability problem becomes decidable. Based on these results of the satisfiability problem, we deduce the (un)decidability results of the model checking problem.
  • Temporal logics with variable quantifications
  • satisfiability and model checking
  • alternating register automata
  • data automata


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. R. Alur, P. Cerny, and S. Weinstein. Algorithmic analysis of array-accessing programs. ACM Trans. Comput. Logic, 13(3):27:1-27:29, 2012. Google Scholar
  2. M. Bojanczyk, C. David, A. Muscholl, T. Schwentick, and L. Segoufin. Two-variable logic on data words. ACM Trans. Comput. Log., 12(4), 2011. Google Scholar
  3. E. Damaggio, A. Deutsch, R. Hull, and V. Vianu. Automatic verification of data-centric business processes. In BPM, 2011. Google Scholar
  4. N. Decker, P. Habermehl, M. Leucker, and D. Thoma. Ordered navigation on multi-attributed data words. In CONCUR, 2014. Google Scholar
  5. S. Demri, D. Figueira, and M. Praveen. Reasoning about data repetitions with counter systems. In LICS, 2013. Google Scholar
  6. S. Demri and R. Lazić. LTL with the freeze quantifier and register automata. ACM Trans. Comput. Logic, 10(3):16:1-16:30, 2009. Google Scholar
  7. E. A. Emerson and K. S. Namjoshi. On reasoning about rings. Int. J. Found. Comput. Sci., 14(4):527-550, 2003. Google Scholar
  8. D. Figueira. Alternating register automata on finite words and trees. Logical Methods in Computer Science, 8(1), 2012. Google Scholar
  9. D. Figueira. Decidability of downward XPath. ACM Trans. Comput. Log., 13(4):34, 2012. Google Scholar
  10. O. Grumberg, O. Kupferman, and S. Sheinvald. Model checking systems and specifications with parameterized atomic propositions. In ATVA, 2012. Google Scholar
  11. O. Grumberg, O. Kupferman, and S. Sheinvald. An automata-theoretic approach to reasoning about parameterized systems and specifications. In ATVA, 2013. Google Scholar
  12. O. Grumberg, O. Kupferman, and S. Sheinvald. Personal communication, June 2014. Google Scholar
  13. I. M. Hodkinson, F. Wolter, and M. Zakharyaschev. Decidable and undecidable fragments of first-order branching temporal logics. In LICS, 2002. Google Scholar
  14. I. M. Hodkinson, F. Wolter, and M. Zakharyaschev. Decidable fragment of first-order temporal logics. Ann. Pure Appl. Logic, 106(1-3):85-134, 2000. Google Scholar
  15. M. Kaminski and N. Francez. Finite-memory automata. Theor. Comput. Sci., 134(2):329-363, 1994. Google Scholar
  16. A. Kara, T. Schwentick, and T. Zeume. Temporal logics on words with multiple data values. In FSTTCS, 2010. Google Scholar
  17. O. Kupferman. Variations on safety. In TACAS, 2014. Google Scholar
  18. O. Sheinvald, S. Grumberg and O. Kupferman. A game-theoretic approach to simulation of data-parameterized systems. In ATVA, 2014. Google Scholar
  19. F. Song and T. Touili. LTL model-checking for malware detection. In TACAS, 2013. Google Scholar
  20. F. Song and T. Touili. Pushdown model checking for malware detection. STTT, 16(2):147-173, 2014. Google Scholar
  21. M. Y. Vardi. An automata-theoretic approach to linear temporal logic. In Conference on Logics for Concurrency : Structure Versus Automata, pages 238-266, 1996. Google Scholar
  22. V. Vianu. Automatic verification of database-driven systems: a new frontier. In ICDT, 2009. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail