论文标题
通过符号自动机声明的反应性合成
Reactive Synthesis for DECLARE via symbolic automata
论文作者
论文摘要
鉴于对有限轨迹（LTLF）解释的线性时间逻辑的规范，反应性合成问题要求找到一个有限的替代，终止的控制器，该控制器对环境的不可控制作用做出反应，以便强制执行所需的系统规范。在本文中，我们首次研究了声明的反应性合成问题 - LTLF的片段在理论和实践中都广泛用于指定声明性的，基于约束的业务流程。我们提供三倍的贡献。首先，我们为此问题提供了一种幼稚的，双重指数的时间合成算法。其次，我们展示了如何将任意声明规范紧凑地编码到LTLF中的同等纯纯度，并利用它来定义一种优化的，单独的指数时间算法来声明合成。第三，我们通过将纯past颞式公式的新颖翻译引入符号确定性有限自动机中，从而得出了该算法的符号版本。
Given a specification of linear-time temporal logic interpreted over finite traces (LTLf), the reactive synthesis problem asks to find a finitely-representable, terminating controller that reacts to the uncontrollable actions of an environment in order to enforce a desired system specification. In this paper we study, for the first time, the reactive synthesis problem for DECLARE - a fragment of LTLf extensively used both in theory and practice for specifying declarative, constraint-based business processes. We provide a threefold contribution. First, we give a naive, doubly exponential time synthesis algorithm for this problem. Second, we show how an arbitrary DECLARE specification can be compactly encoded into an equivalent pure past one in LTLf, and we exploit this to define an optimized, singly exponential time algorithm for DECLARE synthesis. Third, we derive a symbolic version of this algorithm, by introducing a novel translation of pure-past temporal formulas into symbolic deterministic finite automata.
