When: Thursday, September 22, 2022, 11am (CEST).

Where: Zoom online, check the address in the Google Calendar Event.

Topic: Symbolic tableaux for LTL/LTLf satisfiability

Speaker: Dr. Nicola Gigante, Researcher (RTD/a) at Free University of Bozen-Bolzano, Italy.

Abstract

Tableau methods are among the first techniques studied to solve the satisfiability problem for a variety of logics, including linear temporal logic (LTL). Recent developments in the field of tableau methods for LTL include a tree-shaped tableau by Reynolds which improved the state of the art in various directions. However, in the practical usage, tableau methods for LTL usually still suffer on formulas that require complex propositional reasoning, because of the huge size of the tableau tree which, especially in unsatisfiable instances, has to be explicitly explored entirely. In this talk, we introduce the “symbolic tableau” approach, where a propositional encoding of the Reynolds tableau, solved by efficient state-of-the-art SAT solvers, is used to symbolically traverse the tableau tree. The approach combines the advantages of tableau methods (in particular the termination guarantees) with the efficiency of bounded model checking-like approaches. The approach has been implemented in BLACK (Bounded Ltl sAtisfiability ChecKer), a robust and featureful tool that supports LTL, LTLf, and other linear-time logics.

Short Bio

Nicola Gigante got his PhD at the University of Udine in 2019, and after a couple of years there as a postdoc, he is now a researcher at the Free University of Bozen-Bolzano. His main research interests lie at the intersection between AI and formal methods, with a focus on temporal reasoning, including temporal logics, planning, and reactive synthesis.

Material