LFCS Seminar: Thursday 20 June - Luca Bortolussi

Title: From Syntax to Semantics and Back: Real-Valued Embeddings of Temporal Logic Formulae

Abstract: Temporal logic is a simple, yet powerful language, and a recent line of work (requirement or temporal rule mining) aims at learning temporal logic properties that play the role of explainable classifiers or descriptors of sets of trajectories (typically real-valued). Learning is performed in the syntactic space of formulae, and framed as a combinatorial optimisation problem.

In this talk, we will take a different perspective: by defining real-valued (easy to compute) embeddings of logic formulae capturing semantic similarity, we frame the learning problem of temporal logic formulae as a continuous optimisation one, solvable by state-of-the-art (stochastic) gradient methods (recasted in a Bayesian Optimisation framework).

Such embeddings, being semantically consistent, can also be used to cast model checking into a machine learning problem, achieving high accuracy.

On the minus side, embeddings are constructed leveraging kernel methods, hence they are not invertible (i.e. one can map formulae to real vectors, but not go back). Our solution is to learn a pseudo-inverse function leveraging graph neural networks (and diffusion models) or to rely on information retrieval strategies to perform approximate inversions.

In the talk, we will first introduce the embeddings and then discuss some of the afore-mentioned applications.

Short Bio:

Luca Bortolussi is currently full professor of computer science at the University of Trieste, where he leads the AI lab (https://ai-lab.units.it). Previously, he served as associate professor (2015-2021) and assistant professor (2006-2015) at the same university. In 2014-2015, he was professor of Modelling and Simulation at Saarland University, and guest professor in 2026 and 2018-2021. In 2012, he was a visiting researcher at the School of Informatics, University of Edinburgh. He graduated in Mathematics from Trieste in 2003 and he earned a PhD in Computer Science in 2007 from the University of Udine.

His research interests span artificial intelligence, including probabilistic and deep machine learning, neuro-symbolic AI, formal methods in computer science, simulation, and control. He is also interested in cyber-physical systems, collective adaptive systems, explainable artificial intelligence, and various applications in medicine, insurance, industry, sustainability, and climate change.