On the Expressiveness of QCTL

Authors Amélie David, Francois Laroussinie, Nicolas Markey



PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2016.28.pdf
  • Filesize: 0.6 MB
  • 15 pages

Document Identifiers

Author Details

Amélie David
Francois Laroussinie
Nicolas Markey

Cite As Get BibTex

Amélie David, Francois Laroussinie, and Nicolas Markey. On the Expressiveness of QCTL. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 28:1-28:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.CONCUR.2016.28

Abstract

QCTL extends the temporal logic CTL with quantification over atomic propositions. While the algorithmic questions for QCTL and its fragments with limited quantification depth are well-understood (e.g. satisfiability of QkCTL, with at most k nested blocks of quantifiers, is (k+1)-EXPTIME-complete), very few results are known about the expressiveness of this logic.
We address such expressiveness questions in this paper. We first consider the distinguishing power of these logics (i.e., their ability to separate models), their relationship with behavioural equivalences, and their ability to capture the behaviours of finite Kripke structures with so-called characteristic formulas. We then consider their expressive power (i.e., their ability to express a property), showing that in terms of expressiveness the hierarchy QkCTL collapses at level 2 (in other terms, any QCTL formula can be expressed using at most two nested blocks of quantifiers).

Subject Classification

Keywords
  • Specification
  • Verification
  • Temporal Logic
  • Expressiveness
  • Tree automata

Metrics

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

References

  1. D. Berwanger and A. Blumensath. The monadic theory of tree-like structures. In Automata, Logics, and Infinite Games, volume 2500 of LNCS, pages 285-302. Springer, 2002. Google Scholar
  2. M. C. Browne, E. M. Clarke, and O. Grumberg. Characterizing finite Kripke structures in propositional temporal logic. Theoretical Computer Science, 59(1-2):115-131, 1988. Google Scholar
  3. E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In LOP'81, volume 131 of LNCS, pages 52-71. Springer, 1982. Google Scholar
  4. A. Da Costa, F. Laroussinie, and N. Markey. Quantified CTL: Expressiveness and model checking. In CONCUR'12, volume 7454 of LNCS, pages 177-192. Springer, 2012. Google Scholar
  5. G. D'Agostino and M. Hollenberg. Logical questions concerning the μ-calculus: Interpolation, lyndon and łoś-tarski. Journal of Symbolic Logic, 65(1):310-332, 2000. Google Scholar
  6. E. A. Emerson and J. Y. Halpern. "Sometimes" and "not never" revisited: On branching versus linear time temporal logic. Journal of the ACM, 33(1):151-178, 1986. Google Scholar
  7. T. French. Decidability of quantified propositional branching time logics. In AJCAI'01, volume 2256 of LNCS, pages 165-176. Springer, 2001. Google Scholar
  8. T. French. Quantified propositional temporal logic with repeating states. In TIME-ICTL'03, pages 155-165. IEEE Comp. Soc. Press, 2003. Google Scholar
  9. T. French. Bisimulation Quantifiers for Modal Logics. Ph.D. thesis, School of Computer Science &Software Engineering, University of Western Australia, 2006. Google Scholar
  10. M. C. B. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32(1), 1985. Google Scholar
  11. D. Janin and G. Lenzi. On the relationship between monadic and weak monadic second order logic on arbitrary trees. Fundamenta Informaticae, 61(3-4):247-265, 2004. Google Scholar
  12. D. Janin and I. Walukiewicz. Automata for the modal μ-calculus and related results. In MFCS'95, volume 969 of LNCS, pages 552-562. Springer, 1995. Google Scholar
  13. J. Johannsen and M. Lange. CTL^+ is complete for double exponential time. In ICALP'03, volume 2719 of LNCS, pages 767-775. Springer, 2003. Google Scholar
  14. O. Kupferman. Augmenting branching temporal logics with existential quantification over atomic propositions. In CAV'95, volume 939 of LNCS, pages 325-338. Springer, 1995. Google Scholar
  15. F. Laroussinie and N. Markey. Quantified CTL: expressiveness and complexity. Logicical Methods in Computer Science, 10(4), 2014. Google Scholar
  16. F. Laroussinie and N. Markey. Augmenting ATL with strategy contexts. Information and Computation, 245:98-123, 2015. Google Scholar
  17. A. C. Patthak, I. Bhattacharya, A. Dasgupta, P. Dasgupta, and P. P. Chakrabarti. Quantified computation tree logic. Information Processing Letters, 82(3):123-129, 2002. Google Scholar
  18. A. Pnueli. The temporal logic of programs. In FOCS'77, pages 46-57. IEEE Comp. Soc. Press, 1977. Google Scholar
  19. J.-P. Queille and J. Sifakis. Specification and verification of concurrent systems in CESAR. In SOP'82, volume 137 of LNCS, pages 337-351. Springer, 1982. Google Scholar
  20. A. P. Sistla. Theoretical Issues in the Design and Verification of Distributed Systems. PhD thesis, Harvard University, Cambridge, Massachussets, USA, 1983. Google Scholar
  21. M. Y. Vardi. Nontraditional applications of automata theory. In TACS'94, volume 789 of LNCS, pages 575-597. Springer, 1994. Google Scholar
  22. M. Y. Vardi and P. Wolper. Automata theoretic techniques for modal logics of programs. Journal of Computer and System Sciences, 32(2):183-221, 1986. Google Scholar
  23. I. Walukiewicz. Monadic second order logic on tree-like structures. Theoretical Computer Science, 275(1-2):311-346, 2002. Google Scholar
  24. F. Zanasi. Expressiveness of Monadic Second-Order Logics on Infinite Trees of Arbitrary Branching Degrees. Master’s thesis, Amsterdam University, the Netherlands, 2012. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail