Fairness, assumptions, and guarantees for extended bounded response LTL+P synthesis
Software Engineering and Formal Methods: 19th International Conference, SEFM 2021, Virtual Event, December 6–10, 2021, Proceedings(2023)
摘要
Realizability and reactive synthesis from temporal logics are fundamental problems in formal verification. The complexity of these problems for linear temporal logic with past (LTL+P ) led to the identification of fragments with lower complexities and simpler algorithms. Recently, the logic of extended bounded response LTL+P ( _ for short) has been introduced. It allows one to express safety languages definable in LTL+P and it is provided with an efficient, fully symbolic algorithm for reactive synthesis. This paper features four related contributions. First, we introduce GR-EBR , an extension of _ with fairness conditions, assumptions, and guarantees that, on the one hand, allows one to express properties beyond the safety fragment and, on the other, it retains the efficiency of _ in practice. Second, we the expressiveness of GR-EBR starting from the expressiveness of its fragments. In particular, we prove that: (1) _ is expressively complete with respect to the safety fragment of LTL+P , (2) the removal of past operators from _ results into a loss of expressive power, and (3) GR-EBR is expressively equivalent to the logic GR(1) of Bloem et al. Third, we provide a fully symbolic algorithm for the realizability problem from GR-EBR specifications, that reduces it to a number of safety subproblems. Fourth, to ensure soundness and completeness of the algorithm, we propose and exploit a general framework for safety reductions in the context of realizability of (fragments of) LTL+P . The experimental evaluation shows promising results.
更多查看译文
关键词
Reactive synthesis, Temporal logics, Safety reductions, Expressiveness
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要