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 general and PSPACE-complete for the special case of determinist...

Full beskrivning

Bibliografiska uppgifter

Huvudupphov:	Antonia Lechner, Richard Mayr, Joël Ouaknine, Amaury Pouly, James Worrell
Materialtyp:	Artigo
Språk:	Inglês
Utgiven:	Logical Methods in Computer Science e.V. 2018-12-01
Serie:	Logical Methods in Computer Science
Ämnen:	computer science - logic in computer science computer science - formal languages and automata theory
Länkar:	https://lmcs.episciences.org/3106/pdf
Taggar:	Lägg till en tagg Inga taggar, Lägg till första taggen!