Document Open Access Logo

Computation Tree Logic for Synchronization Properties

Authors Krishnendu Chatterjee, Laurent Doyen

PDF

File

Thumbnail PDF
PDF
LIPIcs.ICALP.2016.98.pdf
  • Filesize: 0.52 MB
  • 14 pages

Document Identifiers

Subject Classification

Keywords
  • Computation Tree Logic
  • Synchronization
  • model-checking
  • complexity

Metrics

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

Abstract

We present a logic that extends CTL (Computation Tree Logic) with operators that express synchronization properties. A property is synchronized in a system if it holds in all paths of a certain length. The new logic is obtained by using the same path quantifiers and temporal operators as in CTL, but allowing a different order of the quantifiers. This small syntactic variation induces a logic that can express non-regular properties for which known extensions of MSO with equality of path length are undecidable. We show that our variant of CTL is decidable and that the model-checking problem is in Delta_3^P = P^{NP^{NP}}, and is hard for the class of problems solvable in polynomial time using a parallel access to an NP oracle. We analogously consider quantifier exchange in extensions of CTL, and we present operators defined using basic operators of CTL* that express the occurrence of infinitely many synchronization points. We show that the model-checking problem remains in Delta_3^P. The distinguishing power of CTL and of our new logic coincide if the Next operator is allowed in the logics, thus the classical bisimulation quotient can be used for state-space reduction before model checking.

Cite As Get BibTex

Krishnendu Chatterjee and Laurent Doyen. Computation Tree Logic for Synchronization Properties. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 98:1-98:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.ICALP.2016.98

Author Details

Krishnendu Chatterjee
Laurent Doyen

References

  1. R. Alur, T. A. Henzinger, and O. Kupferman. Alternating-time temporal logic. Journal of the ACM, 49:672-713, 2002. Google Scholar
  2. E. Bach and J. Shallit. Algorithmic Number Theory, Vol. 1: Efficient Algorithms. MIT Press, 1996. Google Scholar
  3. A. Blass and Y. Gurevich. Henkin quantifiers and complete problems. Ann. Pure Appl. Logic, 32:1-16, 1986. Google Scholar
  4. M. C. Browne, E. M. Clarke, and O. Grumberg. Characterizing finite Kripke structures in propositional temporal logic. Theor. Comput. Sci., 59:115-131, 1988. Google Scholar
  5. J. Černý. Poznámka k. homogénnym experimentom s konečnými automatmi. In Matematicko-fyzikálny Časopis, volume 14(3), pages 208-216, 1964. Google Scholar
  6. K. Chatterjee and L. Doyen. Computation tree logic for synchronization properties. CoRR, arXiv:1604.06384, 2016. Google Scholar
  7. K. Chatterjee, T. A. Henzinger, and N. Piterman. Strategy logic. Inf. Comput., 208(6):677-693, 2010. Google Scholar
  8. D. Chistikov, P. Martyugin, and M. Shirmohammadi. Synchronizing automata over nested words. In Proc. of FOSSACS: Foundations of Software Science and Computation Structures, LNCS 9634, pages 252-268. Springer, 2016. Google Scholar
  9. A. Cimatti, E. M. Clarke, F. Giunchiglia, and M. Roveri. NUSMV: A new symbolic model checker. STTT, 2(4):410-425, 2000. Google Scholar
  10. E. M. Clarke, O. Grumberg, and D. Peled. Model checking. MIT Press, 2001. Google Scholar
  11. M. R. Clarkson, B. Finkbeiner, M. Koleini, K. K. Micinski, M. N. Rabe, and C. Sánchez. Temporal logics for hyperproperties. In Proceedings of POST: Principles of Security and Trust, LNCS 8414, pages 265-284. Springer, 2014. Google Scholar
  12. M. R. Clarkson and F. B. Schneider. Hyperproperties. Journal of Computer Security, 18(6):1157-1210, 2010. Google Scholar
  13. S. A. Cook. The complexity of theorem proving procedures. In Proc. of STOC: Symposium on the Theory of Computing, pages 151-158. ACM Press, 1971. Google Scholar
  14. L. Doyen, L. Juhl, K. G. Larsen, N. Markey, and M. Shirmohammadi. Synchronizing words for weighted and timed automata. In Proc. of FSTTCS: Foundations of Software Technology and Theoretical Computer Science, LIPIcs, pages 121-132. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2014. URL: http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2014.121.
  15. L. Doyen, T. Massart, and M. Shirmohammadi. Limit synchronization in Markov decision processes. In Proc. of FoSSaCS: Foundations of Software Science and Computation Structures, LNCS 8412, pages 58-72. Springer-Verlag, 2014. Google Scholar
  16. L. Doyen, T. Massart, and M. Shirmohammadi. Robust synchronization in Markov decision processes. In Proc. of CONCUR: Concurrency Theory, volume LNCS 8704, pages 234-248. Springer, 2014. Google Scholar
  17. J. Kretínský, K. G. Larsen, S. Laursen, and J. Srba. Polynomial time decidability of weighted synchronization under partial observability. In Proc. of CONCUR: Concurrency Theory, volume 42 of LIPIcs, pages 142-154. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. URL: http://dx.doi.org/10.4230/LIPIcs.CONCUR.2015.142.
  18. A. Kučera and Jan Strejček. The stuttering principle revisited. Acta Inf., 41(7-8):415-434, 2005. Google Scholar
  19. K. G. Larsen, S. Laursen, and J. Srba. Synchronizing strategies under partial observability. In Proc. of CONCUR: Concurrency Theory, LNCS 8704, pages 188-202. Springer, 2014. Google Scholar
  20. G. Lenzi. Recent results on modal mu-calculus: a survey. Rend. Istit. Mat. Univ. Trieste, 42(2):235-255, 2010. Google Scholar
  21. H. Spakowski. Completeness for Parallel Access to NP and Counting Class Separations. PhD thesis, Heinrich-Heine-Universität Düsseldorf, 2005. Google Scholar
  22. L. J. Stockmeyer and A. R. Meyer. Word problems requiring exponential time: Preliminary report. In Proc. of STOC: Symposium on Theory of Computing, pages 1-9. ACM, 1973. Google Scholar
  23. W. Thomas. Automata on infinite objects. In Handbook of Theoretical Computer Science, Vol. B: Formal Models and Sematics, pages 133-192. MIT Press, 1990. Google Scholar
  24. W. Thomas. Languages, automata, and logic. In Handbook of Formal Languages, Vol. 3: Beyond Words, pages 389-455. Springer, 1997. Google Scholar
  25. M. V. Volkov. Synchronizing automata and the Černý conjecture. In Proc. of LATA: Language and Automata Theory and Applications, LNCS 5196, pages 11-27. Springer, 2008. Google Scholar
  26. K. W. Wagner. More complicated questions about maxima and minima, and some closures of NP. Theor. Comput. Sci., 51:53-80, 1987. Google Scholar
  27. P. Wolper. Temporal logic can be more expressive. Information and Control, 56(1/2):72-99, 1983. 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
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact