折扣和自动机的精确与近似确定性化

折扣和自动机（NDA）是一种带有边权重的非确定性有限自动机，通过访问边权重的折扣和来评估一次运行的值。更准确地说，运行中第 $i$ 个位置的权重除以 $\lambda^i$，其中折扣因子 $\lambda$ 是一个固定的大于 1 的有理数。一个字的值是自动机在其上所有运行中的最小值。折扣求和是一种常见且有用的度量方案，特别是对于无限序列，它反映了早期权重比后期权重更重要的假设。遗憾的是，在形式化验证中通常必不可少的 NDA 确定性化在一般情况下是无法实现的。我们带来了好消息，表明每个具有整数折扣因子的 NDA 都是可确定性化的。我们通过证明整数恰好刻画了保证可确定性化的折扣因子来补全这一图景：对于每个非整数有理折扣因子 $\lambda$，都存在一个不可确定性化的 $\lambda$-NDA。我们还证明了具有整数折扣因子的 NDA 类在代数运算 min、max、加法和减法下具有封闭性，而这对一般 NDA 和确定性 NDA 并不成立。对于一般 NDA，我们研究了近似确定性化，由于字的后缀的影响会衰减，这总是可行的。我们表明，将自动机计算展开到足够深度的朴素方法在折扣因子上是双重指数级的。我们提供了一种替代的近似确定性化构造方法，其在折扣因子、精度和状态数上均是单指数级的。我们还证明了匹配的下界，表明对这三个参数中任何一个的指数依赖都是不可避免的。我们所有的结果对于有限字上的自动机和无限字上的自动机同样成立。