Logics for time intervals provide a natural framework for representing and reasoning about timing properties in various areas of computer science. However, while various tableau methods have been de- veloped for linear and branching time point-based temporal logics, not much work has been done on tableau methods for interval-based temporal logics. In this paper, we introduce a new, very expressive propositional interval temporal logic, called (Non-Strict) Branching CDT (BCDT+) which extends most of the propositional interval temporal logics pro- posed in the literature. Then, we provide BCDT+ with a generic tableau method which combines features of explicit tableau methods for modal logics with constraint label management and the classical tableau method for ¯rst-order logic, and we prove its soundness and completeness.

A General Tableau Method for Propositional Interval Temporal Logics

SCIAVICCO, Guido
2003

Abstract

Logics for time intervals provide a natural framework for representing and reasoning about timing properties in various areas of computer science. However, while various tableau methods have been de- veloped for linear and branching time point-based temporal logics, not much work has been done on tableau methods for interval-based temporal logics. In this paper, we introduce a new, very expressive propositional interval temporal logic, called (Non-Strict) Branching CDT (BCDT+) which extends most of the propositional interval temporal logics pro- posed in the literature. Then, we provide BCDT+ with a generic tableau method which combines features of explicit tableau methods for modal logics with constraint label management and the classical tableau method for ¯rst-order logic, and we prove its soundness and completeness.
2003
9783540407874
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in SFERA 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/11392/2326771
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 15
  • ???jsp.display-item.citation.isi??? 9
social impact