论文标题
可解释的反应性合成
Explainable Reactive Synthesis
论文作者
论文摘要
反应性合成将时间逻辑中给出的反应系统的规范转换为实现。合成的主要优点是它是自动的。主要缺点是实施通常很难理解。在本文中，我们提出了一个新的合成过程，向用户解释了综合实现。该过程从规范的简单版本和相应的简单实现开始。然后，逐一添加所需的属性，并用反例迹线来解释相应的修复实现的转换。我们提出了基于SAT的算法，用于综合维修和解释。评估算法在一系列示例中进行评估，包括从SyntComp竞争中获得的基准。
Reactive synthesis transforms a specification of a reactive system, given in a temporal logic, into an implementation. The main advantage of synthesis is that it is automatic. The main disadvantage is that the implementation is usually very difficult to understand. In this paper, we present a new synthesis process that explains the synthesized implementation to the user. The process starts with a simple version of the specification and a corresponding simple implementation. Then, desired properties are added one by one, and the corresponding transformations, repairing the implementation, are explained in terms of counterexample traces. We present SAT-based algorithms for the synthesis of repairs and explanations. The algorithms are evaluated on a range of examples including benchmarks taken from the SYNTCOMP competition.
