平坦冻结线性时序逻辑的复杂性
The Complexity of Flat Freeze LTL
AI总结：
本文研究单计数器自动机上平坦冻结LTL的模型检验问题，证明其NEXPTIME完全，并通过交替双向自动机模拟实现NP可达性算法，同时为参数定时自动机可达性提供新证明。
摘要：
我们考虑单计数器自动机（OCA）上冻结线性时序逻辑（freeze LTL）的模型检验问题。冻结LTL通过冻结量词扩展了LTL，该量词允许将运行中的不同计数器值存储在寄存器中，以便相互比较。由于模型检验问题在一般情况下是不可判定的，我们聚焦于冻结LTL的平坦片段，其中冻结量词的使用受到限制。在先前的工作中，Lechner等人证明了在计数器更新采用二进制编码的OCA上，平坦冻结LTL的模型检验是可判定的，且属于2NEXPTIME复杂度类。在本文中，我们证明该问题实际上是NEXPTIME完全的，无论计数器更新采用一元编码还是二进制编码。与Lechner等人一样，我们依赖于将问题归约到带参数化测试的OCA（OCA(P)）中的可达性问题。新的方面在于，我们通过交替双向字自动机来模拟OCA(P)。这蕴含了参数值的指数上界，我们利用该上界为具有一元更新的OCA(P)中的可达性设计了一个NP算法。我们由此推论得出主要结果。作为另一个应用，借助Bundala和Ouaknine的归约，我们获得了已知事实的另一种证明：具有一个参数时钟的闭参数定时自动机中的可达性属于NEXPTIME。
英文摘要：
We consider the model-checking problem for freeze LTL on one-counter automata (OCA). Freeze LTL extends LTL with the freeze quantifier, which allows one to store different counter values of a run in registers so that they can be compared with one another. As the model-checking problem is undecidable in general, we focus on the flat fragment of freeze LTL, in which the usage of the freeze quantifier is restricted. In a previous work, Lechner et al. showed that model checking for flat freeze LTL on OCA with binary encoding of counter updates is decidable and in 2NEXPTIME. In this paper, we prove that the problem is, in fact, NEXPTIME-complete no matter whether counter updates are encoded in unary or binary. Like Lechner et al., we rely on a reduction to the reachability problem in OCA with parameterized tests (OCA(P)). The new aspect is that we simulate OCA(P) by alternating two-way automata over words. This implies an exponential upper bound on the parameter values that we exploit towards an NP algorithm for reachability in OCA(P) with unary updates. We obtain our main result as a corollary. As another application, relying on a reduction by Bundala and Ouaknine, one obtains an alternative proof of the known fact that reachability in closed parametric timed automata with one parametric clock is in NEXPTIME.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
