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
Version:
Publisher's version

Actions


Access Document


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

Authors


More by this author
Department:
Oxford, MPLS, Computer Science
Role:
Author
More by this author
Department:
Green Templeton College
Role:
Author
Publisher:
Schloss Dagstuhl – Leibniz Center for Informatics Publisher's website
Publication date:
2016-08-05
Acceptance date:
2016-04-15
DOI:
ISSN:
1868-8969
Pubs id:
pubs:627106
URN:
uri:45951abe-d7ac-4424-a7f5-4111c53736a6
UUID:
uuid:45951abe-d7ac-4424-a7f5-4111c53736a6
Local pid:
pubs:627106

Terms of use


Metrics


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