One-pass and tree-shaped tableau systems for TPTL and TPTLb+Past

Linear Temporal Logic (LTL) is one of the most commonly used formalisms for representing and reasoning about temporal properties of computations. Its application domains range from formal verification to artificial intelligence. Many real-time extensions of LTL have been proposed over the years, including Timed Propositional Temporal Logic (TPTL), that makes it possible to constrain the temporal ordering of pairs of events as well as the exact time elapsed between them. The paper focuses on TPTL and Bounded TPTL with Past ([Formula presented]), a bounded variant of TPTL enriched with past operators, which has been recently introduced to formalise a meaningful class of timeline-based planning problems. [Formula presented] allows one to refer to the past while keeping the computational complexity under control: in contrast to the full TPTL with Past (TPTL+P), whose satisfiability problem is non-elementary, the satisfiability problem for [Formula presented] is [Formula presented]-complete. The paper deals with the satisfiability problem for TPTL and [Formula presented] by providing an original tableau system for each of them that suitably generalises Reynolds' one-pass and tree-shaped tableau for LTL. First, we show how to handle past operators, by devising a one-pass and tree-shaped tableau system for LTL with Past (LTL+P). Then, we adapt it to TPTL and [Formula presented], providing full proofs of the soundness and completeness of the resulting systems. In particular, completeness is proved by exploiting a novel model-theoretic argument that, compared to the one originally employed for the LTL system, provides a deeper understanding of the crucial role of the prune rule of the system.