Conference item icon

Conference item

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

Expand abstract
Publication status:
Published
Peer review status:
Peer reviewed

Actions


Access Document


Files:
Publisher copy:
10.4230/LIPIcs.CONCUR.2016.29

Authors


More by this author
Institution:
University of Oxford
Division:
MPLS
Department:
Computer Science
Role:
Author
More by this author
Institution:
University of Oxford
Oxford college:
Green Templeton College
Role:
Author
Publisher:
Schloss Dagstuhl – Leibniz Center for Informatics Publisher's website
Host title:
43rd International Colloquium on Automata, Languages and Programming (ICALP 2016)
Journal:
43rd International Colloquium on Automata, Languages and Programming (ICALP 2016) Journal website
Publication date:
2016-08-01
Acceptance date:
2016-04-15
DOI:
ISSN:
1868-8969
Keywords:
Pubs id:
pubs:627106
UUID:
uuid:45951abe-d7ac-4424-a7f5-4111c53736a6
Local pid:
pubs:627106
Deposit date:
2017-08-01

Terms of use


Views and Downloads






If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP