The organization of temporal properties into a Temporal Hierarchy proposed by Manna and Pnueli is central in the study of the expressive power of fragments of Linear Temporal Logic with Past (LTL+P). A crucial role is played by the Reactivity class, which itself forms a hierarchy consisting of the classes Reactivity(1), Reactivity(2), and so on, and it is proved to be expressively equivalent to LTL+P. The logic of Generalized Reactivity(1) (GR(1) for short), introduced in the context of reactive synthesis, expands the Reactivity(1) class (abbreviated R(1)) with safety formulas and multiple fairness conditions. In this paper, we prove that GR(1) is expressively equivalent to R(1). We first define a simple normal form for GR(1) formulas, and then we prove the expressive equivalence between GR(1) (in such a normal form) and R(1). In addition, we show that all the involved translations require only a linear increase in size. Finally, we lift these results to the general case proving that GR(N) is equivalent to R(N), for all N≥1.

GR(1) is equivalent to R(1)

Alessandro Cimatti;Luca Geatti;Angelo Montanari;Stefano Tonetta
2023-01-01

Abstract

The organization of temporal properties into a Temporal Hierarchy proposed by Manna and Pnueli is central in the study of the expressive power of fragments of Linear Temporal Logic with Past (LTL+P). A crucial role is played by the Reactivity class, which itself forms a hierarchy consisting of the classes Reactivity(1), Reactivity(2), and so on, and it is proved to be expressively equivalent to LTL+P. The logic of Generalized Reactivity(1) (GR(1) for short), introduced in the context of reactive synthesis, expands the Reactivity(1) class (abbreviated R(1)) with safety formulas and multiple fairness conditions. In this paper, we prove that GR(1) is expressively equivalent to R(1). We first define a simple normal form for GR(1) formulas, and then we prove the expressive equivalence between GR(1) (in such a normal form) and R(1). In addition, we show that all the involved translations require only a linear increase in size. Finally, we lift these results to the general case proving that GR(N) is equivalent to R(N), for all N≥1.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11582/335944
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact