一句话：提出轨道有限维向量空间理论，并据此给出加权寄存器自动机等价性的判定过程，复杂度指数时间、固定寄存器数多项式时间。
该文研究无限字母表上的加权寄存器自动机的等价性问题。加权寄存器自动机是加权自动机与寄存器自动机的共同推广，其等价性判定此前缺乏通用方法。作者发展了由轨道有限集合张成的向量空间理论，将自动机状态空间视为具有轨道有限维度的向量空间，并在此基础上构造等价性判定算法。算法在最坏情况下为指数时间，当寄存器数目固定时为多项式时间。作为特例，该算法以相同复杂度判定无歧义寄存器自动机的语言等价性，较已有结果有三点改进：允许原子间的序比较而非仅相等比较；复杂度指数级更优；并可处理带猜测的自动机。
We develop a theory of vector spaces spanned by orbit-finite sets. Using this theory, we give a decision procedure for equivalence of weighted register automata, which are the common generalization of weighted automata and register automata for infinite alphabets. The algorithm runs in exponential time, and in polynomial time for a fixed number of registers. As a special case, we can decide, with the same complexity, language equivalence for unambiguous register automata, which improves previous results in three ways: (a) we allow for order comparisons on atoms, and not just equality; (b) the complexity is exponentially better; and (c) we allow automata with guessing.
DOI 原文 ·
@inproceedings{paperbot6197,
title = {Orbit-Finite-Dimensional Vector Spaces and Weighted Register Automata},
author = {Mikolaj Bojanczyk and Bartek Klin and Joshua Moerman},
booktitle = {LICS},
year = {2021},
doi = {10.1109/lics52264.2021.9470634}
}