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.I documenti in SFERA sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
