Expressiveness of Extended Bounded Response LTL

TL;DR

This paper characterizes the expressive power of Extended Bounded Response LTL with Past (LTLEBR+P), showing it is equivalent to the safety fragment of LTL+P and highlighting the importance of past modalities.

Contribution

It proves that LTLEBR+P is expressively complete for safety LTL+P and demonstrates the essential role of past modalities in its expressiveness.

Findings

LTLEBR+P is expressively complete for safety LTL+P.

LTLEBR+P and Safety-LTL are expressively equivalent.

Past modalities are crucial for the full expressiveness of LTLEBR+P.

Abstract

Extended Bounded Response LTL with Past (LTLEBR+P) is a safety fragment of Linear Temporal Logic with Past (LTL+P) that has been recently introduced in the context of reactive synthesis. The strength of LTLEBR+P is a fully symbolic compilation of formulas into symbolic deterministic automata. Its syntax is organized in four levels. The first three levels feature (a particular combination of) future temporal modalities, the last one admits only past temporal operators. At the base of such a structuring there are algorithmic motivations: each level corresponds to a step of the algorithm for the automaton construction. The complex syntax of LTLEBR+P made it difficult to precisely characterize its expressive power, and to compare it with other LTL+P safety fragments. In this paper, we first prove that LTLEBR+P is expressively complete with respect to the safety fragment of LTL+P, that is, any safety language definable in LTL+P can be formalized in LTLEBR+P, and vice versa. From this, it follows that LTLEBR+P and Safety-LTL are expressively equivalent. Then, we show that past modalities play an essential role in LTLEBR+P: we prove that the future fragment of LTLEBR+P is strictly less expressive than full LTLEBR+P.