Model Checking Flat Freeze LTL on One-Counter Automata

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

doi:10.4230/LIPIcs.CONCUR.2016.29

Model Checking Flat Freeze LTL on One-Counter Automata

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract / Description of output

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.

Original language	English
Title of host publication	Proceedings of the 27th International Conference on Concurrency Theory (CONCUR 2016)
Editors	Josée Desharnais, Radha Jagadeesan
Publisher	Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany
Pages	29:1-29:14
Number of pages	14
ISBN (Electronic)	978-3-95977-017-0
DOIs	https://doi.org/10.4230/LIPIcs.CONCUR.2016.29
Publication status	Published - 26 Aug 2016
Event	27th International Conference on Concurrency Theory - Québec City, Canada Duration: 23 Aug 2016 → 26 Aug 2016 https://www.concur2016.ulaval.ca/no_cache/home/

Publication series

Name	Leibniz International Proceedings in Informatics (LIPIcs)
Publisher	Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
Volume	59
ISSN (Print)	1868-896

Conference

Conference	27th International Conference on Concurrency Theory
Abbreviated title	CONCUR 2016
Country/Territory	Canada
City	Québec City
Period	23/08/16 → 26/08/16
Internet address	https://www.concur2016.ulaval.ca/no_cache/home/

Keywords / Materials (for Non-textual outputs)

Formal Languages and Automata Theory

Access to Document

10.4230/LIPIcs.CONCUR.2016.29

1606.02643v2Accepted author manuscript, 710 KBLicence: Creative Commons: Attribution (CC-BY)
LIPIcs-CONCUR-2016-29Final published version, 632 KBLicence: Creative Commons: Attribution (CC-BY)

http://drops.dagstuhl.de/opus/volltexte/2016/6184/

Cite this

Mayr, R., Lechner, A., Ouaknine, J., Pouly, A., & Worrell, J. (2016). Model Checking Flat Freeze LTL on One-Counter Automata. In J. Desharnais, & R. Jagadeesan (Eds.), Proceedings of the 27th International Conference on Concurrency Theory (CONCUR 2016) (pp. 29:1-29:14). Article 29 (Leibniz International Proceedings in Informatics (LIPIcs); Vol. 59). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany. https://doi.org/10.4230/LIPIcs.CONCUR.2016.29

Mayr, Richard ; Lechner, Antonia ; Ouaknine, Joël et al. / Model Checking Flat Freeze LTL on One-Counter Automata. Proceedings of the 27th International Conference on Concurrency Theory (CONCUR 2016). editor / Josée Desharnais ; Radha Jagadeesan. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, 2016. pp. 29:1-29:14 (Leibniz International Proceedings in Informatics (LIPIcs)).

@inproceedings{7c8a7c7965c043a38288944e6bad6d3e,

title = "Model Checking Flat Freeze LTL on One-Counter Automata",

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. ",

keywords = "Formal Languages and Automata Theory",

author = "Richard Mayr and Antonia Lechner and Jo{\"e}l Ouaknine and Amaury Pouly and James Worrell",

year = "2016",

month = aug,

day = "26",

doi = "10.4230/LIPIcs.CONCUR.2016.29",

language = "English",

series = "Leibniz International Proceedings in Informatics (LIPIcs)",

publisher = "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany",

pages = "29:1--29:14",

editor = "Jos{\'e}e Desharnais and Radha Jagadeesan",

booktitle = "Proceedings of the 27th International Conference on Concurrency Theory (CONCUR 2016)",

note = "27th International Conference on Concurrency Theory, CONCUR 2016 ; Conference date: 23-08-2016 Through 26-08-2016",

url = "https://www.concur2016.ulaval.ca/no_cache/home/",

}

Mayr, R, Lechner, A, Ouaknine, J, Pouly, A & Worrell, J 2016, Model Checking Flat Freeze LTL on One-Counter Automata. in J Desharnais & R Jagadeesan (eds), Proceedings of the 27th International Conference on Concurrency Theory (CONCUR 2016)., 29, Leibniz International Proceedings in Informatics (LIPIcs), vol. 59, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, pp. 29:1-29:14, 27th International Conference on Concurrency Theory, Québec City, Canada, 23/08/16. https://doi.org/10.4230/LIPIcs.CONCUR.2016.29

Model Checking Flat Freeze LTL on One-Counter Automata. / Mayr, Richard; Lechner, Antonia; Ouaknine, Joël et al.
Proceedings of the 27th International Conference on Concurrency Theory (CONCUR 2016). ed. / Josée Desharnais; Radha Jagadeesan. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, 2016. p. 29:1-29:14 29 (Leibniz International Proceedings in Informatics (LIPIcs); Vol. 59).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Model Checking Flat Freeze LTL on One-Counter Automata

AU - Mayr, Richard

AU - Lechner, Antonia

AU - Ouaknine, Joël

AU - Pouly, Amaury

AU - Worrell, James

PY - 2016/8/26

Y1 - 2016/8/26

N2 - 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.

AB - 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.

KW - Formal Languages and Automata Theory

U2 - 10.4230/LIPIcs.CONCUR.2016.29

DO - 10.4230/LIPIcs.CONCUR.2016.29

M3 - Conference contribution

T3 - Leibniz International Proceedings in Informatics (LIPIcs)

SP - 29:1-29:14

BT - Proceedings of the 27th International Conference on Concurrency Theory (CONCUR 2016)

A2 - Desharnais, Josée

A2 - Jagadeesan, Radha

PB - Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany

T2 - 27th International Conference on Concurrency Theory

Y2 - 23 August 2016 through 26 August 2016

ER -

Mayr R, Lechner A, Ouaknine J, Pouly A, Worrell J. Model Checking Flat Freeze LTL on One-Counter Automata. In Desharnais J, Jagadeesan R, editors, Proceedings of the 27th International Conference on Concurrency Theory (CONCUR 2016). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany. 2016. p. 29:1-29:14. 29. (Leibniz International Proceedings in Informatics (LIPIcs)). doi: 10.4230/LIPIcs.CONCUR.2016.29

Model Checking Flat Freeze LTL on One-Counter Automata

Abstract / Description of output

Publication series

Conference

Keywords / Materials (for Non-textual outputs)

Access to Document

Fingerprint

Cite this