2018/09/07 by Luca Geatti, Nicola Gigante, Angelo Montanari +1
Computer Science · Mathematics · #Algorithm #Boolean satisfiability problem #Bounded function #Combinatorics #Completeness (order theory) #Computation tree logic #Computer science #Decidability #Discrete mathematics #Formal Methods in Verification #Fragment (logic) #Linear temporal logic #Logic, programming, and type systems #Mathematical proof #Mathematics #Model checking #Model-Driven Software Engineering Techniques #Programming language #Satisfiability #Soundness #Temporal logic #Theoretical computer science #Tree (set theory) #cs.LO
paper · pdf · doi:10.4204/eptcs.277.13
published as EPTCS 277, 2018, pp. 176-190 · In Proceedings GandALF 2018, arXiv:1809.02416
openalex publication_date 2018/09/07 · arxiv created 2018/09/10 · arxiv updated 2018/09/11 · openalex created_date 2020/06/19 · openalex updated_date 2026/08/06
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.