Interval temporal logics are difficult to deal with in many respects. In the last years, various meaningful fragments of Halpern and Shoham's modal logic of time intervals have been shown to be decidable with complexities that range from NP-complete to non-primitive recursive. However, even restricting the attention to finite interval structures, the step from model-theoretic decidability results to the actual implementations of tableau-based decision procedures is quite challenging. In this paper, we investigate the possibility of making use of automated tableau generators. More precisely, we exploit the generator MetTel2 to implement a tableau-based decision procedure for the future fragment of the logic of temporal neighborhood over finite linear orders. We explore and contrast two alternative solutions: a concrete tableau system, that operates on a concrete interval structure explicitly built over a finite, linearly-ordered set of points, and an abstract one, that operates on an interval frame which is forced to be isomorphic to a concrete interval structure by suitably constraining its accessibility relation.

First Steps towards Automated Synthesis of Tableau Systems for Interval Temporal Logics

Della Monica D;MONTANARI, Angelo;
2014-01-01

Abstract

Interval temporal logics are difficult to deal with in many respects. In the last years, various meaningful fragments of Halpern and Shoham's modal logic of time intervals have been shown to be decidable with complexities that range from NP-complete to non-primitive recursive. However, even restricting the attention to finite interval structures, the step from model-theoretic decidability results to the actual implementations of tableau-based decision procedures is quite challenging. In this paper, we investigate the possibility of making use of automated tableau generators. More precisely, we exploit the generator MetTel2 to implement a tableau-based decision procedure for the future fragment of the logic of temporal neighborhood over finite linear orders. We explore and contrast two alternative solutions: a concrete tableau system, that operates on a concrete interval structure explicitly built over a finite, linearly-ordered set of points, and an abstract one, that operates on an interval frame which is forced to be isomorphic to a concrete interval structure by suitably constraining its accessibility relation.
2014
9781612083445
File in questo prodotto:
File Dimensione Formato  
ComputationTools2014cr.pdf

non disponibili

Tipologia: Versione Editoriale (PDF)
Licenza: Non pubblico
Dimensione 279.12 kB
Formato Adobe PDF
279.12 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

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/1037349
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact