Tableau methods for linear-time temporal logics
tutorial at IJCAI-ECAI 2022
Saturday, July 23
Luca Geatti - Free University of Bozen-Bolzano, Italy
Nicola Gigante - Free University of Bozen-Bolzano, Italy
Angelo Montanari - University of Udine, Italy
Temporal logic is one of the most used formalisms to express properties of computations, plans, processes, in AI, formal verification and other fields. Reasoning in temporal logic is one of the most studied task in the literature. Tableau methods are among the first reasoning techniques studied for this purpose, and provide both interesting theoretical insights and practical algorithmic techniques. Despite being a field that has been studied for decades, development of tableau methods for temporal logics continues to this date. In particular, while classic tableau methods for linear-time temporal logics are graph-shaped, recently much work have been focused on tree-shaped tableaux, which proved to have many practical advantages.
This tutorial aims at providing a detailed overview of classical results and recent advanced developments in the area of tableau methods for linear-time temporal logics. Focus will be given on both theoretical foundations and practical aspects, from classic graph-shaped tableaux to recent tree-shaped ones, and their recent SAT encodings. All the topics will be introduced together with their needed background, hence no particular prerequisite is needed to attend the tutorial. The treated topics can be of interest to researchers and practitioners alike in the areas of automated reasoning, planning, (temporal) knowledge representation, and formal verification.
SlidesDownload the slides here.
- Introduction to Temporal Logics and Tableau Methods
- Classic graph-shaped tableau for LTL
- Tree-shaped tableaux by Reynolds
- Model-theoretic view of Reynolds' PRUNE rule
- Tableaux for Timed Propositional Temporal Logic (TPTL)
- Reynolds-style tree-shaped tableau for TPTL
- Efficient implementations: SAT encodings of tree-shaped tableaux
- Introduction to the BLACK satisfiability checker
- Open problems and conclusions