Learning Temporal Specifications from Examples of System Behavior

5^th November 2026, 11:00 Ashton 208
Raj Roy
Liverpool

Abstract

While formal verification provides rigorous methodologies for certifying the correctness of systems, these approaches require requirements to be expressed precisely in formal specification languages. However, writing such specifications manually is often error-prone and tedious.

In this talk, we will see how this challenge can be mitigated by automatically learning formal specifications—focusing on different temporal logics—from examples of system behavior. We discuss how this problem must be adapted to practical settings, where data may be noisy, negative examples may be unavailable, and observations may be uncertain. We present symbolic learning algorithms based on constraint optimization and discuss the rigorous guarantees that these methods can provide. We also outline how specification learning can be integrated with frameworks such as runtime monitoring, AI planning, and related approaches.