Logo del repository
  1. Home
 
Opzioni

GR(1) is equivalent to R(1)

Cimatti A.
•
Geatti L.
•
Gigante N.
altro
Tonetta S.
2023
  • journal article

Periodico
INFORMATION PROCESSING LETTERS
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.
DOI
10.1016/j.ipl.2022.106319
WOS
WOS:000860990000002
Archivio
https://hdl.handle.net/11390/1234988
info:eu-repo/semantics/altIdentifier/scopus/2-s2.0-85138077273
https://ricerca.unityfvg.it/handle/11390/1234988
Diritti
metadata only access
Soggetti
  • Expressive power

  • Formal Method

  • LTL

  • Reactivity

  • Temporal hierarchy

google-scholar
Get Involved!
  • Source Code
  • Documentation
  • Slack Channel
Make it your own

DSpace-CRIS can be extensively configured to meet your needs. Decide which information need to be collected and available with fine-grained security. Start updating the theme to match your nstitution's web identity.

Need professional help?

The original creators of DSpace-CRIS at 4Science can take your project to the next level, get in touch!

Realizzato con Software DSpace-CRIS - Estensione mantenuta e ottimizzata da 4Science

  • Impostazioni dei cookie
  • Informativa sulla privacy
  • Accordo con l'utente finale
  • Invia il tuo Feedback