基于确定树自动机的结构化反应程序综合
Synthesizing Structured Reactive Programs via Deterministic Tree Automata
摘要：
现有的反应系统的合成方法通常涉及过渡系统，如Mealy自动机的建设。然而，为了获得所需系统的简洁表示，结构化程序可能是更合适的模型。2011年，Madhusudan提出了一种算法，可以在不首先合成转换系统的情况下，为给定的omega正则规范构造结构化反应程序。他的程序是基于有限树上的双向交替欧米茄自动机，它可以识别“正确”的程序集。我们提出了一个更基本和直接的方法，只使用确定性的自下而上的树自动机，计算所谓的签名为一个给定的程序。在这样做时，我们扩展Madhusudan的结果，以更广泛的类的程序有界延迟，这可能会读取几个输入符号，然后产生一个输出符号（反之亦然）。作为一个正式的基础，我们归纳定义这样的程序的语义。
英文摘要：
Existing approaches to the synthesis of reactive systems typically involve the construction of transition systems such as Mealy automata. However, in order to obtain a succinct representation of the desired system, structured programs can be a more suitable model. In 2011, Madhusudan proposed an algorithm to construct a structured reactive program for a given omega-regular specification without synthesizing a transition system first. His procedure is based on two-way alternating omega-automata on finite trees that recognize the set of "correct" programs. We present a more elementary and direct approach using only deterministic bottom-up tree automata that compute so-called signatures for a given program. In doing so, we extend Madhusudan's results to the wider class of programs with bounded delay, which may read several input symbols before producing an output symbol (or vice versa). As a formal foundation, we inductively define a semantics for such programs.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
