Speaker: Prof. Martina Maggio
4 Giugno 2026 | 9:00
DEIB, Sala Riunioni PT1 (Ed. 20A)
Contatti: Prof. Maria Prandini
Sommario
On June 4th, 2026, at 9:00 am the seminar on "Over-approximation of weakly-hard constraints for control systems verification" will take place in DEIB PT1 Meeting Room (Building 20A).A hard real-time system cannot miss any deadline. A weakly-hard real-time system, on the contrary, is designed to tolerate a specific number of deadline misses. For instance, the AnyMiss(2, 300) weakly-hard constraint stipulates that in every window of 300 consecutive jobs, at most 2 deadlines are missed. The weakly-hard model is the state-of-the-art for industrial dependability-by-design of control systems that tolerate deterministic failures.
Weakly-hard constraints correspond to regular languages. The size of the minimal finite state machine that recognizes whether a string satisfies the constraint (about 45k states for AnyMiss(2, 300)) is a notorious impediment for the verification of control system properties. This talk discusses an over-approximation of the language that allows us to provide sound safety guarantees for control systems under deadline misses that would be out of reach using the minimal finite state machine. We present a compressed language acceptor and prove that it simulates the original finite state machine. We study language cardinality properties, and report on empirical results that show how the new acceptor can be embedded in the control design workflow, leading to verifying safety for systems for which the state-of-the-art tools do not provide answers.
Biografia
Martina Maggio is a Professor of Computer Science at Saarland University and a Professor of Automatic Control at Lund University.Her research sits at the intersection of real-time systems and control theory, examining what guarantees can still be made about feedback controllers once textbook assumptions—perfect periodicity, reliable communication, predictable execution—no longer hold in real implementations.