Practical Verification of Linear Temporal Logic Modulo Theories Specifications
Speaker: Nicola Gigante, Researcher, University of Bozen-Bolzano (Italy)
Date: Wednesday, February 15, 2023
Time: 3:00pm
Location: NIA, Room 101 or via Teams link
POC: Laura Titolo, National Institute of Aerospace, laura.titolo@nianet.org
Abstract
Linear Temporal Logic (LTL) is the most common specification language for the verification of systems, with many efficient reasoning tools developed in the last decades. However, the propositional nature of LTL limits its applicability to finite-state systems, whereas more complex scenarios, whose dynamics depend on unbounded data or on complex relations between data elements, lead naturally to infinite-state formulations. For this reason, we recently introduced LTL Modulo Theories (LTLMT), a first-order extension of LTL that replaces propositions with first-order formulas interpreted over arbitrary theories, similarly to how Satisfiability Modulo Theories (SMT) extends the classical Boolean satisfiability problem. In contrast to other first-order extensions of LTL, LTLMT has been designed to be efficiently handled in practice by encoding it to SMT problems delivered to state-of-the-art SMT solvers. LTLMT reasoning procedures have been implemented in BLACK, a recently developed temporal reasoning tool for LTL and related logics, with promising results. The talk will overview LTLMT, its reasoning techniques, and the architecture and usage of the BLACK reasoner.
Bio
Nicola Gigante obtained his Ph.D. in Computer Science at the University of Udine, Italy, working on the theoretical foundations of timeline-based planning. He now is a Researcher at the University of Bozen-Bolzano, Italy, working on temporal reasoning at the border between the fields of formal verification and artificial intelligence.
Have questions?
Mary Catherine Bunde
Senior Education Administrator
National Institute of Aerospace
mary.bunde@nianet.org