Document Open Access Logo

The Complexity of Flat Freeze LTL

Authors Benedikt Bollig, Karin Quaas, Arnaud Sangnier

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2017.33.pdf
  • Filesize: 0.59 MB
  • 16 pages

Document Identifiers

Author Details

Benedikt Bollig
Karin Quaas
Arnaud Sangnier

Cite AsGet BibTex

Benedikt Bollig, Karin Quaas, and Arnaud Sangnier. The Complexity of Flat Freeze LTL. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 33:1-33:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.CONCUR.2017.33

Abstract

We consider the model-checking problem for freeze LTL on one-counter automata (OCAs). Freeze LTL extends LTL with the freeze quantifier, which allows one to store different counter values of a run in registers so that they can be compared with one another. As the model-checking problem is undecidable in general, we focus on the flat fragment of freeze LTL, in which the usage of the freeze quantifier is restricted. Recently, Lechner et al. showed that model checking for flat freeze LTL on OCAs with binary encoding of counter updates is decidable and in 2NEXPTIME. In this paper, we prove that the problem is, in fact, NEXPTIME-complete no matter whether counter updates are encoded in unary or binary. Like Lechner et al., we rely on a reduction to the reachability problem in OCAs with parameterized tests (OCAPs). The new aspect is that we simulate OCAPs by alternating two-way automata over words. This implies an exponential upper bound on the parameter values that we exploit towards an NP algorithm for reachability in OCAPs with unary updates. We obtain our main result as a corollary.
Keywords
  • one-counter automata
  • freeze LTL
  • model checking

Metrics

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

References

  1. S. Akshay, B. Bollig, P. Gastin, M. Mukund, and K. Narayan Kumar. Distributed timed automata with independently evolving clocks. Fundamenta Informaticae, 130(4):377-407, 2014. Google Scholar
  2. R. Alur, T. A. Henzinger, and M. Y. Vardi. Parametric real-time reasoning. In Proceedings of STOC'93, pages 592-601. ACM, 1993. Google Scholar
  3. M. Bojańczyk, C. David, A. Muscholl, T. Schwentick, and L. Segoufin. Two-variable logic on data words. ACM Trans. Comput. Log., 12(4):27:1-27:26, 2011. Google Scholar
  4. P. Bouyer, N. Markey, J. Ouaknine, and J. Worrell. On expressiveness and complexity in real-time model checking. In Proceedings of ICALP'08, Part II, volume 5126 of LNCS, pages 124-135. Springer, 2008. Google Scholar
  5. D. Bundala and J. Ouaknine. On parametric timed automata and one-counter machines. Inf. Comput., 253:272-303, 2017. Google Scholar
  6. T. Cachat. Two-way tree automata solving pushdown games. In Automata, Logics, and Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar, February 2001], volume 2500 of LNCS, pages 303-317. Springer, 2002. Google Scholar
  7. H. Comon and V. Cortier. Flatness is not a weakness. In Proceedings of CSL'00, volume 1862 of LNCS, pages 262-276. Springer, 2000. Google Scholar
  8. C. Dax and F. Klaedtke. Alternation elimination by complementation. In Proceedings of LPAR'08, volume 5330 of LNCS, pages 214-229. Springer, 2008. Google Scholar
  9. S. Demri and R. Gascon. The effects of bounding syntactic resources on presburger LTL. J. Log. Comput., 19(6):1541-1575, 2009. Google Scholar
  10. S. Demri and R. Lazic. LTL with the freeze quantifier and register automata. ACM Trans. Comput. Log., 10(3), 2009. Google Scholar
  11. S. Demri, R. Lazic, and D. Nowak. On the freeze quantifier in constraint LTL: decidability and complexity. Inf. Comput., 205(1):2-24, 2007. Google Scholar
  12. S. Demri, R. Lazic, and A. Sangnier. Model checking memoryful linear-time logics over one-counter automata. Theor. Comput. Sci., 411(22-24):2298-2316, 2010. Google Scholar
  13. S. Demri and A Sangnier. When model-checking freeze LTL over counter machines becomes decidable. In Proceedings of FoSSaCS'10, volume 6014 of LNCS, pages 176-190. Springer, 2010. Google Scholar
  14. J. Fearnley and M. Jurdzinski. Reachability in two-clock timed automata is pspace-complete. In Proceedings of ICALP'13, Part II, volume 7966 of Lecture Notes in Computer Science, pages 212-223. Springer, 2013. Google Scholar
  15. S. Feng, M. Lohrey, and K. Quaas. Path checking for MTL and TPTL over data words. In Proceedings of DLT'15, volume 9168 of LNCS, pages 326-339. Springer, 2015. Google Scholar
  16. T. French. Quantified propositional temporal logic with repeating states. In Proceedings of TIME-ICTL'03, pages 155-165. IEEE Computer Society, 2003. Google Scholar
  17. Z. Galil. Hierarchies of complete problems. Acta Inf., 6:77-88, 1976. Google Scholar
  18. S. Göller, C. Haase, J. Ouaknine, and J. Worrell. Model checking succinct and parametric one-counter automata. In Proceedings of ICALP'10, Part II, volume 6199 of LNCS, pages 575-586. Springer, 2010. Google Scholar
  19. S. Göller, C. Haase, J. Ouaknine, and J. Worrell. Branching-time model checking of parametric one-counter automata. In Proceedings of FOSSACS'12, volume 7213 of LNCS, pages 406-420. Springer, 2012. Google Scholar
  20. S. Göller and M. Lohrey. Branching-time model checking of one-counter processes and timed automata. SIAM J. Comput., 42(3):884-923, 2013. Google Scholar
  21. C. Haase. On the complexity of model checking counter automata. PhD thesis, University of Oxford, 2012. Google Scholar
  22. C. Haase, S. Kreutzer, J. Ouaknine, and J. Worrell. Reachability in succinct and parametric one-counter automata. In Proceedings of CONCUR'09, volume 5710 of LNCS, pages 369-383. Springer, 2009. Google Scholar
  23. P. Hofman, S. Lasota, R. Mayr, and P. Totzke. Simulation problems over one-counter nets. Logical Methods in Computer Science, 12(1), 2016. Google Scholar
  24. O. Kupferman and M. Y. Vardi. An automata-theoretic approach to reasoning about infinite-state systems. In Proceedings of CAV'00, volume 1855 of LNCS, pages 36-52. Springer, 2000. Google Scholar
  25. P. Lafourcade, D. Lugiez, and R. Treinen. Intruder deduction for AC-like equational theories with homomorphisms. In Proceedings of RTA'05, volume 3467 of LNCS, pages 308-322. Springer, 2005. Google Scholar
  26. A. Lechner, R. Mayr, J. Ouaknine, A. Pouly, and J. Worrell. Model checking flat freeze LTL on one-counter automata. In Proceedings of CONCUR'16, volume 59 of LIPIcs, pages 29:1-29:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. Google Scholar
  27. A. Lisitsa and I. Potapov. Temporal logic with predicate lambda-abstraction. In Proceedings of TIME'05, pages 147-155. IEEE Computer Society, 2005. Google Scholar
  28. O. Serre. Parity games played on transition graphs of one-counter processes. In Proceedings of FoSSaCS'06, volume 3921 of LNCS, pages 337-351. Springer, 2006. Google Scholar
  29. L. G. Valiant and M. S. Paterson. Deterministic one-counter automata. Journal of Computer and System Sciences, 10(3):340-350, 1975. Google Scholar
  30. M. Y. Vardi. Reasoning about the past with two-way automata. In Proceedings of ICALP'98, volume 1443 of LNCS, pages 628-641. Springer, 1998. 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 Imprint Privacy Contact