Safraless LTL Synthesis Considering Maximal Realizability
Safraless LTL Synthesis Considering Maximal Realizability
复制标题
考虑最大可实现性的Safraless LTL合成
DOI：
10.1007/s00236-016-0280-3
复制
发表时间：
2016
期刊：
影响因子：
0.6
通讯作者：
Naoki Yonezaki
中科院分区：
文献类型：
--
作者：
Takashi Tomita;Atsushi Ueno;Masaya Shimakawa;Shigeki Hagihara;Naoki Yonezaki
线性时序逻辑(LTL)综合是一种形式化的方法，用于自动组成一个反应性系统，如果该规范是可实现的，则该系统实现了用LTL描述的给定行为规范。即使整个规范无法实现，最好是合成一个尽力而为的反应系统。也就是说，最大限度地实现其部分规范的系统。因此，我们将规范分为必须规范(不应违反)和期望规范(违反可能不可避免)。在这篇文章中，我们提出了一种方法来合成一个反应系统，它实现了所有必须的规范，并努力满足每一个期望的规范。没有假设的理想规范的一般形式是，意思是“始终成立”。在我们的方法中，最好的努力是在交互中最大化令人满意的步数。为了定量评估步数，我们使用了基于LTL公式的平均收益目标。我们的方法应用无安全方法来根据给定的必须和期望的规范构造安全游戏，其中必须规范可以用完整的LTL编写，并且可以包括假设。然后将由期望规格构造的安全对策转化为均值支付对策，最终构成一个反应系统，作为对策的同步乘积的最优策略。
Linear temporal logic (LTL) synthesis is a formal method for automatically composing a reactive system that realizes a given behavioral specification described in LTL if the specification is realizable. Even if the whole specification is unrealizable, it is preferable to synthesize a best-effort reactive system. That is, a system that maximally realizes its partial specifications. Therefore, we categorized specifications into must specifications (which should never be violated) and desirable specifications (the violation of which may be unavoidable). In this paper, we propose a method for synthesizing a reactive system that realizes all must specifications and strongly endeavors to satisfy each desirable specification. The general form of the desirable specifications without assumptions is, which means “always holds”. In our approach, the best effort to satisfyis to maximize the number of steps satisfyingin the interaction. To quantitatively evaluate the number of steps, we used a mean-payoff objective based on LTL formulae. Our method applies the Safraless approach to construct safety games from given must and desirable specifications, where the must specification can be written in full LTL and may include assumptions. It then transforms the safety games constructed from the desirable specifications into mean-payoff games and finally composes a reactive system as an optimal strategy on a synchronized product of the games.