一句话:证明无复制线性加权自动机有界性可判定,并把零隔离归约到正交向量加法系统,三维情形在 Schanuel 猜想下可判定。
论文研究非负有理数半环上的线性成本寄存器自动机(等价于加权自动机,可视为概率自动机的推广)的有界性与零隔离问题:前者问是否存在词序列使权重趋于无穷,后者问是否趋于零。一般模型下两问题均不可判定,作者转向无复制线性限制,证明有界性可判定。为处理零隔离,论文进一步限制模型,并构造其与正交向量加法系统(OVAS)通用覆盖性的等价关系;OVAS 是向量加法系统家族的新模型,每个正交象限有各自可用的向量。在 Schanuel 猜想成立的前提下,作者证明了三维 OVAS 通用覆盖性可判定,从而得到至多三个独立寄存器时零隔离可判定。
We consider linear cost-register automata (equivalent to weighted automata) over the semiring of nonnegative rationals, which generalise probabilistic automata. The two problems of boundedness and zero isolation ask whether there is a sequence of words that converge to infinity and to zero, respectively. In the general model both problems are undecidable so we focus on the copyless linear restriction. There, we show that the boundedness problem is decidable. As for the zero isolation problem we need to further restrict the class. We obtain a model, where zero isolation becomes equivalent to universal coverability of orthant vector addition systems (OVAS), a new model in the VAS family interesting on its own. In standard VAS runs are considered only in the positive orthant, while in OVAS every orthant has its own set of vectors that can be applied in that orthant. Assuming Schanuel’s conjecture is true, we prove decidability of universal coverability for three-dimensional OVAS, which implies decidability of zero isolation in a model with at most three independent registers.
DOI 原文 · arXiv · PDF(开放获取) · DBLP
@inproceedings{CzerwinskiLMPW22,
title = {The boundedness and zero isolation problems for weighted automata over nonnegative rationals},
author = {Wojciech Czerwiński and Engel Lefaucheux and Filip Mazowiecki and David Purser and Markus Whiteland},
booktitle = {LICS},
year = {2022},
doi = {10.1145/3531130.3533336}
}