One-Pass and Tree-Shaped Tableau Systems for TPTL and TPTLb+Past

TL;DR

This paper introduces a new one-pass, tree-shaped tableau method for TPTL and TPTLb+P, simplifying verification of real-time systems with complex past operators while maintaining EXPSPACE-complete complexity.

Contribution

It presents a unified tableau system for TPTL and TPTLb+P, providing a syntactic embedding and simplified proofs of soundness and completeness.

Findings

The tableau system is sound and complete for TPTL and TPTLb+P.

The complexity of the tableau system is EXPSPACE-complete.

The approach simplifies existing proofs for tableau systems in temporal logic.

Abstract

In this paper, we propose a novel one-pass and tree-shaped tableau method for Timed Propositional Temporal Logic and for a bounded variant of its extension with past operators. Timed Propositional Temporal Logic (TPTL) is a real-time temporal logic, with an EXPSPACE-complete satisfiability problem, which has been successfully applied to the verification of real-time systems. In contrast to LTL, adding past operators to TPTL makes the satisfiability problem for the resulting logic (TPTL+P) non-elementary. In this paper, we devise a one-pass and tree-shaped tableau for both TPTL and bounded TPTL+P (TPTLb+P), a syntactic restriction introduced to encode timeline-based planning problems, which recovers the EXPSPACE-complete complexity. The tableau systems for TPTL and TPTLb+P are presented in a unified way, being very similar to each other, providing a common skeleton that is then specialised to each logic. In doing that, we characterise the semantics of TPTLb+P in terms of a purely syntactic fragment of TPTL+P, giving a translation that embeds the former into the latter. Soundness and completeness of the system are proved fully. In particular, we give a greatly simplified model-theoretic completeness proof, which sidesteps the complex combinatorial argument used by known proofs for the one-pass and tree-shaped tableau systems for LTL and LTL+P.