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 (TPTLb+P), a bounded variant of TPTL enriched with past operators, which has been recently introduced to formalise a meaningful class of timeline-based planning problems. TPTLb+P 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 TPTLb+P is EXPSPACE-complete. The paper deals with the satisfiability problem for TPTL and TPTLb+P 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 TPTLb+P, 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. (C) 2020 Elsevier Inc. All rights reserved.