一句话：刻画有限值、函数型、无歧义非确定性有限转换器的关系何时可由确定性双带自动机验证，并证明判定不可判定。
本文类比 P vs NP 中“主动产生”与“事后验证”的差异，研究有限转换器与自动机之间的关系验证问题。每个非确定性有限转换器定义二元关系，将输入词映射到它可成功产生的所有输出词；有限值转换器要求每个输入对应的输出词数量有有限上界。作者刻画了有限值、函数型和无歧义的非确定性转换器，其关系何时能被确定性双带自动机验证；若存在这样的自动机，则给出构造方法，并证明该判定准则本身是不可判定的。该工作为有限状态转换关系的能力边界提供了自动机式的验证视角。
The question whether P equals NP revolves around the discrepancy between active production and mere verification by Turing machines. In this paper, we examine the analogous problem for finite transducers and automata. Every nondeterministic finite transducer defines a binary relation associating each input word with all output words that the transducer can successfully produce on the given input. Finite-valued transducers are those for which there is a finite upper bound on the number of output words that the relation associates with every input word. We characterize finite-valued, functional, and unambiguous nondeterministic transducers whose relations can be verified by a deterministic two-tape automaton, show how to construct such an automaton if one exists, and prove the undecidability of the criterion.
DOI 原文 ·
@inproceedings{paperbot6158,
title = {From Finite-Valued Nondeterministic Transducers to Deterministic Two-Tape Automata},
author = {Elisabet Burjons and Fabian Frei and Martin Raszyk},
booktitle = {LICS},
year = {2021},
doi = {10.1109/lics52264.2021.9470688}
}