论文标题
综合实现不可交通规格的实现
Synthesizing Approximate Implementations for Unrealizable Specifications
论文作者
论文摘要
规范的不确定性通常是由于假设环境的行为是不受限制的。在本文中，我们介绍了在有限环境中合成的算法，在该算法中，环境只能生成最终是具有有限大小的有限表示的输入序列。我们提供了自动理论和符号方法来解决这一综合问题，还研究了来自不可交通规范的近似实现的综合。此类实现总体上可能违反规范，但可以保证满足至少有限大小的套索的指定部分的规范。我们在不同的仲裁体规范上评估算法。
The unrealizability of a specification is often due to the assumption that the behavior of the environment is unrestricted. In this paper, we present algorithms for synthesis in bounded environments, where the environment can only generate input sequences that are ultimately periodic words (lassos) with finite representations of bounded size. We provide automata-theoretic and symbolic approaches for solving this synthesis problem, and also study the synthesis of approximative implementations from unrealizable specifications. Such implementations may violate the specification in general, but are guaranteed to satisfy the specification on at least a specified portion of the bounded-size lassos. We evaluate the algorithms on different arbiter specifications.
