Fairness, assumptions, and guarantees for extended bounded response LTL+P synthesis

Abstract

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 (LTLEBR+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 LTLEBR+P 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 LTLEBR+P in practice. Second, we the expressiveness of GR-EBR starting from the expressiveness of its fragments. In particular, we prove that: (1) LTLEBR+P is expressively complete with respect to the safety fragment of LTL+P, (2) the removal of past operators from LTLEBR+P 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.