International Conference on Analytic
Tableaux and Related Methods (TABLEAUX'99),
LNCS 1617, Springer,
A Tableau Calculus for a Temporal Logic with Temporal Connectives
The paper presents a tableau calculus for a linear time temporal
logic for reasoning about processes and events in concurrent
systems. The logic is based on temporal connectives in the style of
Transaction Logic and explicit
quantification over states. The language extends first-order logic
with sequential and parallel conjunction, parallel disjunction, and
temporal implication. Explicit quantification over states via state
variables allows to express temporal properties which cannot be
formulated in modal logics.
Using the tableau representation of temporal Kripke structures
presented for CTL which represents
states by prefix terms, explicit quantification over states is
integrated into the tableau calculus by an adaptation of the
delta-rule from first-order tableau calculi to the linear
ordering of the universe of states.
Complementing the CTL calculus, the paper shows that this tableau
representation is both suitable for modal temporal logics and
for logics using temporal connectives.