paperbot · PL 论文追踪

全部论文 待读 收藏

P2 On delay and regret determinization of max-plus automata

关于 max-plus 自动机的延迟与遗憾确定化
LICS 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2017匹配度 2/10 · 该论文研究 max-plus 自动机的延迟/后悔确定化,属于纯自动机与形式语言理论,与形式验证/静态分析仅有间接的理论关联;它不涉及 LLM/Agent、浮点程序分析或贝叶斯程序分析等用户核心方向,也无工程落地或 benchmark 设计。引用 17 inbox
Emmanuel Filiot, Ismael Jecker, Nathan Lhote, Guillermo A. Perez, Jean-Francois Raskin
crossref: 2026-09-12dblp: 2026-09-12arxiv: 2026-09-12

AI 速览

一句话:提出 k-delay 与 r-regret 确定化,证明其 EXPTIME 完全性并刻画与一般确定化的关系。

max-plus 半环上加权自动机的确定化问题长期未决。本文通过限制确定性自动机的搜索空间提出 k-delay 与 r-regret 两种受限确定化:前者要求确定性接受运行在每个同长度前缀上与 N 的最大运行权重差不超过 k,后者要求在线消解非确定性使运行值与 N 的值差不超过 r。作者证明 WA 可确定化当且仅当它对某个 k 是 k-delay 可确定化的,因此判定该 k 与一般确定化问题难度相同。当 k 和 r 给定时,两个判定问题均为 EXPTIME 完全;判定是否存在某个 r 使 WA 为 r-regret 可确定化属于 EXPTIME。

问题
max-plus 半环上加权自动机(WA)的确定化问题长期未决;本文通过 k-delay 与 r-regret 约束确定性自动机的搜索空间来研究该问题。
方法
定义 k-delay 与 r-regret 确定化,将确定性运行与 N 的最大运行或在线非确定性消解进行比较,并分析相应判定问题的可判定性与复杂度。
评估
以理论复杂度结果为评估:证明 k,r 输入时 k-delay 与 r-regret 确定化判定均为 EXPTIME 完全,且存在 r 的 r-regret 判定属于 EXPTIME。
原文摘要(Abstract)

Decidability of the determinization problem for weighted automata over the semiring (ℤ∪{−∞}, max; +), WA for short, is a long-standing open question. We propose two ways of approaching it by constraining the search space of deterministic WA: k-delay and r-regret. A WA N is k-delay determinizable if there exists a deterministic automaton D that defines the same function as N and for all words α in the language of N, the accepting run of D on α is always at most k-away from a maximal accepting run of N on α. That is, along all prefixes of the same length, the absolute difference between the running sums of weights of the two runs is at most k. A WA N is r-regret determinizable if for all words α in its language, its non-determinism can be resolved on the fly to construct a run of N such that the absolute difference between its value and the value assigned to α by N is at most r. We show that a WA is determinizable if and only if it is k-delay determinizable for some k. Hence deciding the existence of some k is as difficult as the general determinization problem. When k and r are given as input, the k-delay and r-regret determinization problems are shown to be EXPTIME-complete. We also show that determining whether a WA is r-regret determinizable for some r is in EXPTIME.

链接与引用

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

BibTeX
@inproceedings{FiliotJLPR17,
  title = {On delay and regret determinization of max-plus automata},
  author = {Emmanuel Filiot and Ismael Jecker and Nathan Lhote and Guillermo A. Perez and Jean-Francois Raskin},
  booktitle = {LICS},
  year = {2017},
  doi = {10.1109/lics.2017.8005096}
}