文章基本信息

标题：Model Checking Flat Freeze LTL on One-Counter Automata
本地全文：下载
作者：Worrell, James ; Pouly, Amaury ; Ouaknine, Joël 等
期刊名称：Logical Methods in Computer Science
印刷版ISSN：1860-5974
电子版ISSN：1860-5974
出版年度：2018
卷号：14
期号：4
DOI：10.23638/LMCS-14(4:20)2018
语种：English
出版社：Technical University of Braunschweig
摘要：Freeze LTL is a temporal logic with registers that is suitable for specifyingproperties of data words. In this paper we study the model checking problem forFreeze LTL on one-counter automata. This problem is known to be undecidable ingeneral and PSPACE-complete for the special case of deterministic one-counterautomata. Several years ago, Demri and Sangnier investigated the model checkingproblem for the flat fragment of Freeze LTL on several classes of counterautomata and posed the decidability of model checking flat Freeze LTL onone-counter automata as an open problem. In this paper we resolve this problempositively, utilising a known reduction to a reachability problem onone-counter automata with parameterised equality and disequality tests. Ourmain technical contribution is to show decidability of the latter problem bytranslation to Presburger arithmetic.
关键词：Computer Science - Logic in Computer Science;Computer Science - Formal Languages and Automata Theory