从无限词上的有理规范合成可计算函数
Synthesizing Computable Functions from Rational Specifications over Infinite Words
AI总结：
本文研究从无限词有理规范合成可计算函数，证明一般情形不可判定，但对确定性有理规范子类可判定且为ExpTime完全，并给出基于奇偶博弈的可靠归约方法。
摘要：
合成问题要求从正确输入-输出对的规范中自动生成算法（如果存在的话）。本文考虑无限词上可计算函数的合成问题，采用经典图灵可计算性概念处理无限输入。我们考虑的规范是无限词上的有理关系，即由非确定性奇偶转换器定义的规范。我们证明了从有理规范合成可计算函数的问题是不可判定的。我们提供了一个不完整但可靠的归约到某个奇偶博弈，使得如果Eve赢得该博弈，则有理规范可由可计算函数实现。我们证明该函数甚至可由确定性双向转换器计算。我们给出了后者博弈归约完备的充分条件。这导致了可计算函数合成问题的可判定性，我们证明对于有理规范的一个大子类，即确定性有理规范，该问题是ExpTime完全的。该子类包含无限词上的自动关系类，这是反应式合成中的一个基准。
英文摘要：
The synthesis problem asks to automatically generate, if it exists, an algorithm from a specification of correct input-output pairs. In this paper, we consider the synthesis of computable functions of infinite words, for a classical Turing computability notion over infinite inputs. We consider specifications which are rational relations of infinite words, i.e., specifications defined non-deterministic parity transducers. We prove that the synthesis problem of computable functions from rational specifications is undecidable. We provide an incomplete but sound reduction to some parity game, such that if Eve wins the game, then the rational specification is realizable by a computable function. We prove that this function is even computable by a deterministic two-way transducer. We provide a sufficient condition under which the latter game reduction is complete. This entails the decidability of the synthesis problem of computable functions, which we prove to be ExpTime-complete, for a large subclass of rational specifications, namely deterministic rational specifications. This subclass contains the class of automatic relations over infinite words, a yardstick in reactive synthesis.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
