2025-12-15T06:34:20.389476

Unambiguisability and Register Minimisation of Min-Plus Models

Almagor, Arbel, Sheinvald
We study the unambiguisability problem for min-plus (tropical) weighted automata (WFAs), and the counter-minimisation problem for tropical Cost Register Automata (CRAs), which are expressively-equivalent to WFAs. Both problems ask whether the "amount of nondeterminism" in the model can be reduced. We show that WFA unambiguisability is decidable, thus resolving this long-standing open problem. Our proof is via reduction to WFA determinisability, which was recently shown to be decidable. On the negative side, we show that CRA counter minimisation is undecidable, even for a fixed number of registers (specifically, already for 7 registers).
academic

Unambiguisability and Register Minimisation of Min-Plus Models

基本信息

  • 论文ID: 2512.09484
  • 标题: Unambiguisability and Register Minimisation of Min-Plus Models
  • 作者: Shaull Almagor, Guy Arbel, Sarai Sheinvald (Technion – Israel Institute of Technology)
  • 分类: cs.FL (Formal Languages and Automata Theory)
  • 发表时间: 2025年12月（arXiv预印本）
  • 论文链接: https://arxiv.org/abs/2512.09484

摘要

本文研究min-plus（热带）加权有限自动机（WFAs）的无歧义化问题，以及与WFAs表达能力等价的热带成本寄存器自动机（CRAs）的计数器最小化问题。这两个问题都询问模型中的"非确定性程度"是否可以降低。作者证明了WFA无歧义化问题是可判定的，从而解决了这一长期开放问题。证明方法是归约到WFA确定化问题（该问题最近被证明是可判定的）。负面结果方面，作者证明CRA计数器最小化问题是不可判定的，即使对于固定数量的寄存器（具体为7个寄存器）也是如此。

研究背景与动机

1. 研究问题

本文研究两个核心问题：

  • 无歧义化问题：给定一个加权有限自动机A，是否存在一个等价的无歧义自动机？
  • 寄存器最小化问题：给定一个k-寄存器的成本寄存器自动机，是否存在一个等价的(k-1)-寄存器自动机？

2. 问题重要性

  • 理论意义：加权有限自动机是重要的量化计算模型，定义从单词到值的函数。热带半环（Z∪{∞}, min, +）的WFAs在系统建模中有广泛应用，可用于推理资源使用的最优方式（如能耗）。
  • 实践价值：非确定性的存在使得WFAs的推理变得更困难。例如，热带WFAs的等价性问题对于非确定性自动机是不可判定的，但对确定性自动机是可判定的。
  • 历史地位：热带WFAs在解决star-height猜想中发挥了关键作用。

3. 现有方法的局限性

  • 确定化问题直到最近（2025年）才被证明可判定
  • 对于多项式歧义的热带自动机，无歧义化问题已被证明可判定，但一般情况仍是开放问题
  • 有理数域上的无歧义化问题已可判定，但热带半环上的情况未解决
  • 大多数模型中，确定化和无歧义化问题通常同时解决，但热带WFAs的情况特殊

4. 研究动机

  • 无歧义WFAs严格比确定性WFAs表达能力更强，但保留了一些良好的闭包和算法性质
  • 非确定性可以用多种方式度量：歧义性（ambiguity）和宽度（width）提供了不同视角
  • 寄存器数量对应于WFA的宽度，提供了另一种度量非确定性的方法

核心贡献

本文的主要贡献包括：

  1. 解决长期开放问题：证明了热带WFA的无歧义化问题是可判定的，这是一个长期未解决的问题。
  2. 创新的归约方法：通过归约到确定化问题来解决无歧义化问题。这在某种程度上是反直觉的，因为通常是先解决无歧义化，再解决确定化。
  3. 新的间隙刻画：引入U-type间隙见证（U-type gap witness）的概念，提供了无歧义化的完整刻画。
  4. 负面结果：证明CRA寄存器最小化问题是不可判定的，即使固定寄存器数量为7也是如此。
  5. 等价性结果：精化了k-CRA与宽度k的WFA之间的等价性关系。

方法详解

任务定义

无歧义化问题（Problem 2）：

  • 输入：一个WFA A
  • 输出：判定是否存在等价的无歧义WFA
  • 定义：WFA A是无歧义的，当且仅当每个单词至多有一条接受运行

寄存器最小化问题：

  • 输入：一个k-寄存器的CRA
  • 输出：判定是否存在等价的(k-1)-寄存器CRA

核心方法架构

1. U-type间隙刻画（Section 3）

定义5（U-type B-Gap Witness）： 对于B ∈ N，一个U-type B-gap见证由单词对x, y ∈ Σ*和状态p₁, q₁ ∈ Q, p₂, q₂ ∈ F组成，存在运行：

  • ρ: q₀ →^x p₁ →^y p₂
  • χ: q₀ →^x q₁ →^y q₂

满足：

  1. mwt(q₀ →^x Q) = wt(χx)（χ的前缀是x上的最小权重运行）
  2. mwt(q₀ →^xy F) = wt(ρ)（ρ是xy上的最小接受运行）
  3. wt(ρx) - wt(χx) > B（读完x后，ρ比最小运行高至少B）

定理6：WFA A可无歧义化当且仅当存在B ∈ N使得A的间隙被B界定。

2. 无歧义化的构造（Section 3.2）

给定间隙被B界定的WFA A，构造等价的无歧义WFA U：

状态空间：S = Q × B-Win，其中B-Win = {-∞, -B, ..., B, ∞}^Q

关键思想：

  • 跟踪规范最小运行（canonical minimal run）
  • 使用B-窗口记录每个状态相对于当前跟踪状态的权重偏移
  • 通过优先级排序（线性序⪯）在多条最小运行中选择唯一的规范运行

转移关系Λ的定义： 对于状态(q, f_q)和字母σ，考虑转移(q, σ, c, p)：

  1. 计算中间函数g(p) = min{f_q(r) + mwt(r →^σ p) - c | r ∈ Q}
  2. 一致性检查：
    • 如果g(p) < 0，不添加转移（存在更低权重运行）
    • 如果存在r ≠ q且q ⪯ r使得f_q(r) + mwt(r →^σ p) - c = g(p)，不添加转移（存在更高优先级运行）
  3. 将g截断到-B, B得到f_p

接受状态： G = {(q, f_q) | q ∈ F ∧ ∀p ∈ F, (f_q(p) > 0 ∨ (f_q(p) = 0 ∧ p ⪯ q))}

3. 归约到确定化（Section 4）

核心思想：构造WFA B使得A可无歧义化当且仅当B可确定化。

构造细节：

  • 状态：S = Q × Com，其中Com = {⊥, ↛, →}^Q（承诺函数）
  • 字母表：Γ = Σ × Updt，其中Updt = {⊥, ↛, →}^(Q×Q)（更新函数）
  • 承诺语义：
    • →：状态可达且在接受运行上
    • ↛：状态可达但不在接受运行上
    • ⊥：状态不可达

一致性条件：

  1. Δ-一致性：投影到A是有效转移
  2. 更新一致性：α正确反映σ上的可用转移
  3. 出边一致性：f(r) = → 当且仅当存在r' s.t. r → r' ∈ α
  4. 入边一致性：g(r') = → 当且仅当存在r s.t. r → r' ∈ α

关键引理：

  • 引理15：如果A中存在U-type B-gap见证，则B中存在D-type B-gap见证
  • 引理16：如果B中存在D-type B-gap见证，则A中存在U-type B-gap见证

技术创新点

  1. 间隙刻画的创新：
    • 引入U-type间隙见证，区别于已知的D-type间隙见证
    • U-type要求"低运行"也必须能继续到接受状态，这是与D-type的关键区别
  2. 规范运行的构造：
    • 通过线性序⪯从后向前逐步筛选最小运行
    • 保证唯一性的同时维持最小权重性质
  3. 归约的巧妙设计：
    • 使用承诺和更新机制强制B的D-type见证也是A的U-type见证
    • 通过一致性检查确保低运行的可扩展性
  4. 宽度与寄存器的等价性：
    • 精确建立k-CRA与宽度k WFA的双向转换
    • 在WFA→CRA方向，关键创新是重用寄存器而非为每个状态分配独立寄存器

实验设置

本文是纯理论工作，不包含实验评估。所有结果都是通过严格的数学证明获得的。

证明结构

  1. 无歧义化可判定性（Section 3-4）：
    • 第3节：证明间隙刻画的充分必要性
    • 第4节：归约到确定化问题
  2. 寄存器最小化不可判定性（Section 5）：
    • 从两计数器机的0-停机问题归约
    • 利用定理22（来自2）的构造
    • 构造宽度7的WFA，证明无法归约到宽度6

理论工具

  • 间隙见证技术：源自确定化问题的研究
  • 子集构造：用于CRA到WFA的转换
  • 矩阵表示：用于CRA的语义定义
  • 归约技术：从不可判定问题（两计数器机）到目标问题

实验结果

主要理论结果

1. 无歧义化可判定性（定理13 + 推论17）

定理13：无歧义化问题可归约到确定化问题。

推论17：WFA的无歧义化问题是可判定的。

证明要点：

  • 正向：如果B可确定化，则A可无歧义化
    • 利用引理16：B的D-type见证蕴含A的U-type见证
    • 通过承诺机制的入边一致性，保证低运行可扩展到接受状态
  • 反向：如果A可无歧义化，则B可确定化
    • 利用引理15：A的U-type见证自动是B的D-type见证
    • 通过投影保持权重和最小性

2. 寄存器最小化不可判定性（定理20）

定理20：以下问题不可判定，即使k=7：给定宽度k的WFA，判定是否存在等价的宽度k-1 WFA。

推论21：以下问题不可判定，即使k=7：给定k-CRA，判定是否存在等价的(k-1)-CRA。

证明策略：

  1. 从两计数器机M构造宽度6的WFA A（定理22）
  2. 扩展A得到宽度7的WFA A'，添加：
    • 状态q_a和q_i（i∈6）
    • 字母$, i, a, ī_i
  3. 如果A上界有界，则q_a冗余，可得宽度6的等价WFA
  4. 如果A无界，则存在ζ=x@使得q₀ →^ζ q₀权重为1
  5. 使用单词w = ζ^(6m) 1^(5m) 2^(4m) ... 5^m和后缀x = a ī₁ī₂...ī₅构造矛盾：
    • 7个前缀x₀,...,x₆使得A'(wx_i) = im
    • 鸽笼原理：至少两个前缀i<j到达同一状态t
    • 权重差(j-i)m ≤ 12||B||，与m > 12||B||矛盾

复杂性分析

无歧义化问题：

  • 下界：PSPACE-hard（继承自确定化问题的下界）
  • 上界：未知（确定化问题的复杂性上界尚未建立）
  • 归约复杂性：状态空间单指数膨胀

寄存器最小化问题：

  • 对于固定k≥7：不可判定
  • 对于k<7：开放问题
  • 对于有理数域上的CRA：可判定（6）

关键技术洞察

  1. 间隙界定的本质：
    • U-type间隙刻画了两条接受运行的"分离程度"
    • 有界间隙保证可以用有限窗口跟踪所有相关运行
  2. 确定化vs无歧义化：
    • 通常先解决无歧义化，再解决确定化
    • 热带半环上反其道而行：先解决确定化，再归约无歧义化
    • 原因：承诺机制可以"强制"D-type见证变成U-type见证
  3. 宽度的不可压缩性：
    • 7个组件（q_a和q_1,...,q_6）通过精心设计的单词和杀死字母产生不可合并的权重配置
    • 每个组件在不同时刻达到最小值，无法用6个寄存器模拟

相关工作

1. 确定化问题研究

  • 历史：可追溯到1990年代19, 20
  • 有理数域：最近被证明可判定5, 14
  • 热带半环：2025年被证明可判定1（本文作者的前期工作）
  • 间隙刻画：Filiot等人11引入D-type间隙概念

2. 歧义性研究

  • 分类：k-歧义、有限歧义、多项式歧义7
  • 多项式歧义：Kirsten和Lombardy16证明热带自动机的无歧义化可判定
  • 有理数域：Bell和Smertnig5证明可判定
  • 本文贡献：解决一般情况（任意歧义度）

3. 成本寄存器自动机

  • 引入：Alur等人4定义CRA模型
  • 表达能力：与WFA等价4
  • 寄存器最小化：
    • 有理数域：可判定6
    • 热带半环：本文证明不可判定
  • 弱CRA：Almagor等人3研究copyless CRA

4. 热带半环的应用

  • star-height问题：Hashiguchi12, 13、Kirsten15的工作
  • 限制性问题：Leung和Podolskiy18
  • 上界有界性：Almagor等人2证明不可判定（本文寄存器最小化归约的基础）

本文的独特贡献

  1. 首次解决热带WFA的一般无歧义化问题
  2. 创新方向：通过归约到确定化而非直接构造
  3. 完整图景：同时给出正面结果（无歧义化可判定）和负面结果（寄存器最小化不可判定）
  4. 精细刻画：建立k-CRA与宽度k WFA的精确对应

结论与讨论

主要结论

  1. 可判定性结果：热带WFA的无歧义化问题是可判定的，解决了长期开放问题。
  2. 不可判定性结果：CRA寄存器最小化问题即使对于固定的7个寄存器也是不可判定的。
  3. 方法论贡献：通过归约到确定化问题解决无歧义化，展示了问题间的深刻联系。
  4. 等价性精化：k-CRA与宽度k WFA精确等价。

局限性

  1. 复杂性未知：
    • 无歧义化问题的精确复杂性未确定
    • 仅知PSPACE-hard下界
    • 归约有单指数膨胀，是否必要未知
  2. 寄存器最小化的间隙：
    • k=7时不可判定
    • k<7时的可判定性仍是开放问题
    • 对于k=1（确定化）是可判定的
  3. 放松歧义性：
    • 2-歧义化、有限歧义化、多项式歧义化的一般可判定性未解决
    • 缺乏对应的间隙刻画
  4. 特殊片段：
    • copyless CRA的寄存器最小化可判定性未知
    • 其他结构限制下的情况未探索

未来方向

作者明确提出的开放问题：

  1. 放松的歧义性：
    • 能否判定给定WFA是否有等价的2-歧义/有限歧义/多项式歧义WFA？
    • 2-歧义化问题似乎非常困难，目前没有对应的间隙准则
  2. 完善寄存器最小化图景：
    • k<7时寄存器最小化是否可判定？
    • 虽然重要性较低，但完整刻画仍有价值
  3. 结构片段：
    • copyless CRA的寄存器最小化
    • 其他受限CRA类的性质
  4. 复杂性界定：
    • 确定无歧义化问题的精确复杂性
    • 一旦确定化的复杂性界定，研究归约是否可以改进（多项式时间或对数空间）

深度评价

优点

  1. 重大理论突破：
    • 解决了长期开放的无歧义化问题
    • 方法新颖：反向利用确定化解决无歧义化
    • 证明技术深刻且优雅
  2. 完整的理论图景：
    • 正面结果（可判定性）和负面结果（不可判定性）并存
    • 建立了不同模型（WFA和CRA）和不同度量（歧义性和宽度）之间的联系
  3. 技术创新显著：
    • U-type间隙刻画：精确捕捉无歧义性的本质
    • 规范运行构造：通过优先级排序实现唯一性
    • 承诺机制：巧妙地将D-type见证转化为U-type见证
    • 寄存器重用：在WFA→CRA转换中避免指数膨胀
  4. 证明严谨完整：
    • 所有定理都有详细证明
    • 引理之间逻辑清晰
    • 关键技术点（如引理8、9）有充分论证
  5. 写作质量高：
    • 结构清晰，从动机到结果层层递进
    • 直观解释与形式化定义结合良好
    • 图示（如图1-5）有助于理解

不足

  1. 复杂性界限缺失：
    • 无歧义化问题的上界未知
    • 归约的膨胀是否必要未分析
    • 实际可计算性未评估
  2. 寄存器最小化的间隙：
    • k=7的界是否紧？
    • k∈{2,3,4,5,6}的情况完全开放
    • 从k=1（可判定）到k=7（不可判定）的转折点未确定
  3. 放松歧义性问题未触及：
    • 2-歧义化等问题仅在讨论中提及
    • 没有提供任何技术线索或部分结果
  4. 缺乏实践考量：
    • 纯理论工作，无算法实现
    • 无复杂性分析或可行性讨论
    • 对实际应用的指导有限
  5. 证明技术的可推广性：
    • 方法是否适用于其他半环未讨论
    • 与有理数域上已知结果的关系未深入分析

影响力评估

  1. 理论意义重大：
    • 解决长期开放问题，预期将成为领域里程碑
    • 为后续研究提供新工具（U-type间隙、承诺机制）
    • 揭示了确定化与无歧义化的深层联系
  2. 方法论贡献：
    • 归约技术可能启发其他问题的解决
    • 间隙刻画方法可能推广到其他模型
  3. 开放问题的启发：
    • 明确指出重要的后续方向
    • 为k<7的寄存器最小化提供基准
  4. 局限性对影响的制约：
    • 缺乏复杂性界限限制了实际应用
    • 算法化和实现需要进一步工作

适用场景

  1. 理论研究：
    • 形式语言与自动机理论
    • 可判定性和复杂性理论
    • 半环上的计算模型
  2. 系统验证：
    • 需要推理资源消耗（能耗、时间）的系统
    • 量化验证中的自动机简化
  3. 算法设计：
    • 加权自动机的优化和转换
    • 非确定性的度量和控制
  4. 教学价值：
    • 展示归约技术的强大
    • 说明可判定性边界的微妙性

技术亮点总结

  1. U-type间隙的精确刻画：完美捕捉了无歧义性的组合本质
  2. 规范运行的构造：通过简单的优先级机制解决了唯一性问题
  3. 承诺机制的设计：将运行DAG显式编码到字母表中，强制一致性
  4. 寄存器重用策略：在保持等价性的同时实现精确的宽度对应
  5. 不可判定性证明的精巧性：通过7个组件的精心编排展示不可压缩性

参考文献（关键文献）

1 Almagor, Arbel, Sheinvald (2025). Determinization of min-plus weighted automata is decidable. SODA 2025.

2 Almagor, Boker, Kupferman (2020). What's decidable about weighted automata? Information and Computation.

4 Alur et al. (2013). Regular functions and cost register automata. LICS 2013.

5 Bell, Smertnig (2023). Computing the linear hull: Deciding determinizable and unambiguous for weighted automata over fields. LICS 2023.

11 Filiot et al. (2017). On delay and regret determinization of max-plus automata. LICS 2017.

16 Kirsten, Lombardy (2009). Deciding unambiguity and sequentiality of polynomially ambiguous min-plus automata. STACS 2009.

总体评价：本文是形式语言与自动机理论领域的重要理论贡献，解决了长期开放的无歧义化问题，并揭示了寄存器最小化的不可判定性。证明技术深刻且创新，特别是通过归约到确定化问题的反向思路。尽管缺乏复杂性界限和实际算法，但其理论价值和方法论贡献使其成为该领域的重要进展。对于理论计算机科学研究者，这是一篇必读的论文。