Model Checking Flat Freeze LTL on One-Counter Automata

Authors Antonia Lechner, Richard Mayr, Joël Ouaknine, Amaury Pouly, James Worrell



PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2016.29.pdf
  • Filesize: 0.61 MB
  • 14 pages

Document Identifiers

Author Details

Antonia Lechner
Richard Mayr
Joël Ouaknine
Amaury Pouly
James Worrell

Cite As Get BibTex

Antonia Lechner, Richard Mayr, Joël Ouaknine, Amaury Pouly, and James Worrell. Model Checking Flat Freeze LTL on One-Counter Automata. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 29:1-29:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.CONCUR.2016.29

Abstract

Freeze LTL is a temporal logic with registers that is suitable for specifying properties of data words.  In this paper we study the model checking problem for Freeze LTL on one-counter automata. This problem is known to be undecidable in full generality and PSPACE-complete for the special case of deterministic one-counter automata. Several years ago, Demri and Sangnier investigated the model checking problem for the flat fragment of Freeze LTL on several classes of counter automata and posed the decidability of model checking flat Freeze LTL on one-counter automata as an open problem. In this paper we resolve this problem positively, utilising a known reduction to a reachability problem on one-counter automata with parameterised equality and disequality tests. Our main technical contribution is to show decidability of the latter problem by translation to Presburger arithmetic.

Subject Classification

Keywords
  • one-counter automata
  • disequality tests
  • reachability
  • freeze LTL
  • Presburger arithmetic

Metrics

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

References

  1. P. Bouyer, N. Markey, J. Ouaknine, and J. Worrell. On expressiveness and complexity in real-time model checking. In Proceedings of ICALP, volume 5126 of LNCS, pages 124-135. Springer, 2008. Google Scholar
  2. H. Comon and V. Cortier. Flatness is not a weakness. In Proceedings of CSL, volume 1862 of LNCS. Springer, 2000. Google Scholar
  3. S. Demri and R. Lazić. LTL with the freeze quantifier and register automata. In Proceedings of LICS, pages 17-26. IEEE Computer Society, 2006. Google Scholar
  4. S. Demri, R. Lazić, and D. Nowak. On the freeze quantifier in constraint LTL: decidability and complexity. In Proceedings of TIME, pages 113-121, 2005. Google Scholar
  5. S. Demri, R. Lazić, and A. Sangnier. Model checking freeze LTL over one-counter automata. In Proceedings of FOSSACS, volume 4962 of LNCS, pages 490-504, 2008. Google Scholar
  6. S. Demri and A. Sangnier. When model-checking freeze LTL over counter machines becomes decidable. In Proceedings of FOSSACS, volume 6014 of LNCS, pages 176-190, 2010. Google Scholar
  7. John Fearnley and Marcin Jurdzinski. Reachability in two-clock timed automata is PSPACE-complete. Inf. Comput., 243:26-36, 2015. Google Scholar
  8. T. French. Quantified propositional temporal logic with repeating states. In Proceedings of TIME-ICTL, pages 155-165. IEEE Computer Society, 2003. Google Scholar
  9. C. Haase, S. Kreutzer, J. Ouaknine, and J. Worrell. Reachability in succinct and parametric one-counter automata. In Proceedings of CONCUR, volume 5710 of LNCS, pages 369-383. Springer, 2009. Google Scholar
  10. O. H. Ibarra, T. Jiang, N. Tran, and H. Wang. New decidability results concerning two-way counter machines and applications. In Proceedings of ICALP, volume 700 of LNCS. Springer, 1993. Google Scholar
  11. A. Lisitsa and I. Potapov. Temporal logic with predicate lambda-abstraction. In Proceedings of TIME, pages 147-155. IEEE Computer Society, 2005. Google Scholar
  12. M. Presburger. Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In Comptes Rendus du I congrés de Mathématiciens des Pays Slaves. Warsaw, pages 92-101, 1929. 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