Fairness, Assumptions, and Guarantees for Extended Bounded Response LTL+P Synthesis

Realizability and reactive synthesis from temporal logics are fundamental problems in the formal verification field. The complexity of the Linear-time Temporal Logic with Past (LTL+P) case led to the definition of fragments with lower complexities and simpler algorithms. Recently, the logic of Extended Bounded Response LTL+P (LTLEBR+ P ) has been introduced. It allows one to express any safety language definable in LTL and it is provided with an efficient, fully-symbolic algorithm for reactive synthesis. In this paper, we extend LTLEBR+ P with fairness conditions, assumptions, and guarantees. The resulting logic, called GR-EBR, preserves the main strength of LTLEBR+ P, that is, efficient realizability, and makes it possible to specify properties beyond safety. We study the problem of reactive synthesis for GR-EBR and devise a fully-symbolic algorithm that reduces it to a number of safety subproblems. To ensure soundness and completeness, we propose a general framework for safety reductions in the context of realizability of (fragments of) LTL+P. The experimental evaluation shows the feasibility of the approach.