Document Open Access Logo

Synchronized CTL over One-Counter Automata

Authors Shaull Almagor , Daniel Assa, Udi Boker

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2023.19.pdf
  • Filesize: 1.1 MB
  • 22 pages

Document Identifiers

Author Details

Shaull Almagor
  • Department of Computer Science, Technion, Israel
Daniel Assa
  • Reichman University, Herzliya, Israel
Udi Boker
  • Reichman University, Herzliya, Israel

Funding

  • Almagor, Shaull: supported by the Israel Science Foundation grant 989/22.
  • Boker, Udi: supported by the Israel Science Foundation grant 2410/22.

Cite As Get BibTex

Shaull Almagor, Daniel Assa, and Udi Boker. Synchronized CTL over One-Counter Automata. In 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 284, pp. 19:1-19:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.FSTTCS.2023.19

Abstract

We consider the model-checking problem of Synchronized Computation-Tree Logic (CTL+Sync) over One-Counter Automata (OCAs). CTL+Sync augments CTL with temporal operators that require several paths to satisfy properties in a synchronous manner, e.g., the property "all paths should eventually see p at the same time". The model-checking problem for CTL+Sync over finite-state Kripke structures was shown to be in 𝖯^{NP^NP}. OCAs are labelled transition systems equipped with a non-negative counter that can be zero-tested. Thus, they induce infinite-state systems whose computation trees are not regular. The model-checking problem for CTL over OCAs was shown to be PSPACE-complete. 
We show that the model-checking problem for CTL+Sync over OCAs is decidable. However, the upper bound we give is non-elementary. We therefore proceed to study the problem for a central fragment of CTL+Sync, extending CTL with operators that require all paths to satisfy properties in a synchronous manner, and show that it is in EXP^NEXP (and in particular in EXPSPACE), by exhibiting a certain "segmented periodicity" in the computation trees of OCAs.

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
Keywords
  • CTL
  • Synchronization
  • One Counter Automata
  • Model Checking

Metrics

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

Related Versions

References

  1. Shaull Almagor, Udi Boker, and Orna Kupferman. Formalizing and reasoning about quality. Journal of the ACM, 63(3):24:1-24:56, 2016. Google Scholar
  2. Roland Axelsson, Matthew Hague, Stephan Kreutzer, Martin Lange, and Markus Latte. Extended computation tree logic. In Logic for Programming, Artificial Intelligence, and Reasoning: 17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10-15, 2010. Proceedings 17, pages 67-81. Springer, 2010. Google Scholar
  3. Udi Boker, Krishnendu Chatterjee, Thomas A. Henzinger, and Orana Kupferman. Temporal specifications with accumulative values. ACM Trans. Comput. Log., 15(4):27:1-27:25, 2014. Google Scholar
  4. Krishnendu Chatterjee and Laurent Doyen. Computation tree logic for synchronization properties. In Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi, editors, 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy, volume 55 of LIPIcs, pages 98:1-98:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. Google Scholar
  5. Michael R Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K Micinski, Markus N Rabe, and César Sánchez. Temporal logics for hyperproperties. In Principles of Security and Trust: Third International Conference, POST 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings 3, pages 265-284. Springer, 2014. Google Scholar
  6. Michael R Clarkson and Fred B Schneider. Hyperproperties. Journal of Computer Security, 18(6):1157-1210, 2010. Google Scholar
  7. Byron Cook, Heidy Khlaaf, and Nir Piterman. Verifying increasingly expressive temporal logics for infinite-state systems. Journal of the ACM (JACM), 64(2):1-39, 2017. Google Scholar
  8. David C Cooper. Theorem proving in arithmetic without multiplication. Machine intelligence, 7(91-99):300, 1972. Google Scholar
  9. Stéphane Demri, Alain Finkel, Valentin Goranko, and Govert van Drimmelen. Model-checking CTL* over flat Presburger counter systems. Journal of Applied Non-Classical Logics, 20(4):313-344, 2010. Google Scholar
  10. Alain Finkel, Jérôme Leroux, and Grégoire Sutre. Reachability for two-counter machines with one test and one reset. In FSTTCS 2018-38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, volume 122, pages 31-1. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018. Google Scholar
  11. Michael J Fischer and Michael O Rabin. Super-exponential complexity of Presburger arithmetic. In Quantifier Elimination and Cylindrical Algebraic Decomposition, pages 122-135. Springer, 1998. Google Scholar
  12. Seymour Ginsburg and Edwin H Spanier. Bounded ALGOL-like languages. Transactions of the American Mathematical Society, 113(2):333-368, 1964. Google Scholar
  13. Stefan Göller and Markus Lohrey. Branching-time model checking of one-counter processes and timed automata. SIAM J. Comput., 42(3):884-923, 2013. Google Scholar
  14. Christoph Haase. A survival guide to Presburger arithmetic. ACM SIGLOG News, 5(3):67-82, 2018. Google Scholar
  15. Christoph Haase, Stephan Kreutzer, Joël Ouaknine, and James Worrell. Reachability in succinct and parametric one-counter automata. In CONCUR 2009 - Concurrency Theory: 20th International Conference, CONCUR 2009, Bologna, Italy, September 1-4, 2009. Proceedings 20, pages 369-383. Springer, 2009. Google Scholar
  16. Jérôme Leroux and Grégoire Sutre. Flat counter automata almost everywhere! In International Symposium on Automated Technology for Verification and Analysis, pages 489-503. Springer, 2005. Google Scholar
  17. Jérôme Leroux and Grégoire Sutre. Reachability in two-dimensional vector addition systems with states: One test is for free. In 31st International Conference on Concurrency Theory (CONCUR 2020). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. Google Scholar
  18. Marvin L. Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, Englewood Cliffs, N.J., 1967. Google Scholar
  19. Mojzesz Presburger. Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. Comptes Rendus du I Congrès de Mathématiciens des Pays Slaves, pages 92-101, 1929. Google Scholar
  20. Leslie G Valiant and Michael S Paterson. Deterministic one-counter automata. Journal of Computer and System Sciences, 10(3):340-350, 1975. Google Scholar
  21. Igor Walukiewicz. Model checking CTL properties of pushdown systems. In International Conference on Foundations of Software Technology and Theoretical Computer Science, pages 127-138. Springer, 2000. 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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact