paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Determinisability of register and timed automata

寄存器自动机与时间自动机的可确定性
LMCS vol.Volume 18, Issue 22022匹配度 1/10 · 该论文属于自动机理论与可判定性/复杂度研究,讨论寄存器自动机与时间自动机的确定化成员问题,与用户关注的静态分析、LLM/Agent、浮点程序分析、贝叶斯程序分析等方向几乎没有直接交集。虽然形式化方法与验证理论可能间接相关,但并非当前研究画像的核心。引用 2 inbox
Lorenzo Clemente, Sławomir Lasota, Radosław Piórkowski
crossref: 2026-09-10

AI 速览

一句话:完整刻画寄存器自动机与时间自动机确定性成员问题的可判定性与复杂度版图。

本文研究确定性成员问题:给定非确定性寄存器自动机或时间自动机所定义的语言,能否由相应的确定性自动机识别。作者分别针对寄存器自动机和时间自动机,系统刻画该问题的可判定性边界。对寄存器自动机,证明当输入为非确定单寄存器自动机(允许 ε 迁移)且输出确定自动机的寄存器数固定时问题可判定;并证明该结果最优:输入含两个及以上寄存器(即使无 ε 迁移)、使用猜测、或输出寄存器数不固定时不可判定。对时间自动机,证明当输入为无 ε 迁移的单时钟非确定时间自动机且输出确定自动机时钟数固定时可判定;若输入有两个及以上时钟、使用 ε 迁移、或输出时钟数不固定则不可判定。

问题
给定非确定寄存器自动机或时间自动机,判定其语言能否被确定性寄存器自动机或时间自动机识别,即确定性成员问题。
方法
通过理论证明给出特定参数组合下的可判定算法,并利用不可判定性结果证明这些可判定条件的紧致性,从而绘制完整版图。
评估
理论证明:分别对寄存器自动机与时间自动机建立可判定情形,并证明其余情形不可判定,以说明所得结果的 optimality。
原文摘要(Abstract)

The deterministic membership problem for timed automata asks whether the timed language given by a nondeterministic timed automaton can be recognised by a deterministic timed automaton. An analogous problem can be stated in the setting of register automata. We draw the complete decidability/complexity landscape of the deterministic membership problem, in the setting of both register and timed automata. For register automata, we prove that the deterministic membership problem is decidable when the input automaton is a nondeterministic one-register automaton (possibly with epsilon transitions) and the number of registers of the output deterministic register automaton is fixed. This is optimal: We show that in all the other cases the problem is undecidable, i.e., when either (1) the input nondeterministic automaton has two registers or more (even without epsilon transitions), or (2) it uses guessing, or (3) the number of registers of the output deterministic automaton is not fixed. The landscape for timed automata follows a similar pattern. We show that the problem is decidable when the input automaton is a one-clock nondeterministic timed automaton without epsilon transitions and the number of clocks of the output deterministic timed automaton is fixed. Again, this is optimal: We show that the problem in all the other cases is undecidable, i.e., when either (1) the input nondeterministic timed automaton has two clocks or more, or (2) it uses epsilon transitions, or (3) the number of clocks of the output deterministic automaton is not fixed.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot1702,
  title = {Determinisability of register and timed automata},
  author = {Lorenzo Clemente and Sławomir Lasota and Radosław Piórkowski},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 18, Issue 2},
  year = {2022},
  doi = {10.46298/lmcs-18(2:9)2022}
}