一句话：证明单计数器自动机上平坦 Freeze LTL 的模型检测可判定，并通过 Presburger 算术解决参数化等值测试的可达性问题。
Freeze LTL 是一种带寄存器的时序逻辑，适合描述数据字上的性质。本文研究单计数器自动机上 Freeze LTL 的模型检测问题。该问题一般不可判定，而对确定性单计数器自动机是 PSPACE 完全的。此前 Demri 与 Sangnier 研究了平坦片段的模型检测，并将单计数器自动机情形列为开放问题。本文正面解决该问题：利用到带参数化等值/不等值测试的单计数器自动机可达性问题的已知归约；主要技术贡献是把后者翻译到 Presburger 算术，从而证明该可达性问题可判定，进而得到平坦 Freeze LTL 模型检测的可判定性。
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 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 the decidability of model checking flat Freeze LTL on one-counter automata as an open problem. In this paper we resolve this problem positively, utilising a known reduction to a reachability problem on one-counter automata with parameterised equality and disequality tests. Our main technical contribution is to show decidability of the latter problem by translation to Presburger arithmetic.
@article{paperbot349,
title = {Model Checking Flat Freeze LTL on One-Counter Automata},
author = {Antonia Lechner and Richard Mayr and Joël Ouaknine and Amaury Pouly and James Worrell},
journal = {Logical Methods in Computer Science},
volume = {Volume 14, Issue 4},
year = {2018},
doi = {10.23638/lmcs-14(4:20)2018}
}