Agenda

30 Giu 2023 10:00

Practical Verification of First-Order Temporal Properties

Laboratorio ACADIA, edificio ZETA - Campus Scientifico via Torino

Speaker: Nicola Gigante, University of Bozen-Bolzano, Italy

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 Sketch:
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.

Lingua

L'evento si terrà in inglese

Organizzatore

Nicola Prezza

Cerca in agenda