The propositional interval logic of temporal neighborhood (PNL for short) features two modalities that make it possible to access intervals adjacent to the right (modality ⟨ A⟩) and to the left (modality ⟨ A¯ ⟩) of the current interval. PNL stands at a central position in the realm of interval temporal logics, as it is expressive enough to encode meaningful temporal conditions and decidable (undecidability rules over interval temporal logics, while PNL is NEXPTIME-complete). Moreover, it is expressively complete with respect to the two-variable fragment of first-order logic extended with a linear order FO 2[<]. Various extensions of PNL have been studied in the literature, including metric, hybrid, and first-order ones. Here, we study the effects of the addition of an equivalence relation ∼ to Metric PNL (MPNL∼). We first show that the finite satisfiability problem for PNL extended with ∼ is still NEXPTIME-complete. Then, we prove that the same problem for MPNL∼ can be reduced to the decidable 0–0 reachability problem for vector addition systems and vice versa (EXPSPACE-hardness immediately follows).

Metric propositional neighborhood logic with an equivalence relation

MONTANARI, Angelo;
2016-01-01

Abstract

The propositional interval logic of temporal neighborhood (PNL for short) features two modalities that make it possible to access intervals adjacent to the right (modality ⟨ A⟩) and to the left (modality ⟨ A¯ ⟩) of the current interval. PNL stands at a central position in the realm of interval temporal logics, as it is expressive enough to encode meaningful temporal conditions and decidable (undecidability rules over interval temporal logics, while PNL is NEXPTIME-complete). Moreover, it is expressively complete with respect to the two-variable fragment of first-order logic extended with a linear order FO 2[<]. Various extensions of PNL have been studied in the literature, including metric, hybrid, and first-order ones. Here, we study the effects of the addition of an equivalence relation ∼ to Metric PNL (MPNL∼). We first show that the finite satisfiability problem for PNL extended with ∼ is still NEXPTIME-complete. Then, we prove that the same problem for MPNL∼ can be reduced to the decidable 0–0 reachability problem for vector addition systems and vice versa (EXPSPACE-hardness immediately follows).
File in questo prodotto:
File Dimensione Formato  
ActaMontanariPazzagliaSala.pdf

accesso aperto

Descrizione: articolo principale
Tipologia: Documento in Pre-print
Licenza: Creative commons
Dimensione 422.02 kB
Formato Adobe PDF
422.02 kB Adobe PDF Visualizza/Apri

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/11390/1110493
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? 0
social impact