Model checking flat freeze LTL on one-counter automata
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 det...
| Prif Awduron: | , , , , |
|---|---|
| Fformat: | Conference item |
| Cyhoeddwyd: |
Schloss Dagstuhl – Leibniz Center for Informatics
2016
|