ATVA 2025
Mon 27 - Fri 31 October 2025 Bengaluru, India
Wed 29 Oct 2025 14:30 - 15:00 at R102 - Monitoring and Runtime Verification Chair(s): Ichiro Hasuo

Runtime monitors assess whether a system is in an unsafe state based on a stream of observations. We study the problem where the system is subject to probabilistic uncertainty and described by a hidden Markov model. A stream of observations is then unsafe if the probability of being in an unsafe state is above a threshold. A correct monitor recognizes the set of unsafe observations. The key contribution of this paper is the first correct-by-construction synthesis method for such monitors, represented as finite automata. The contribution combines four ingredients: First, we establish the coNP-hardness of checking whether an automaton is a correct monitor, i.e., a monitor without misclassifications. Second, we provide a reduction that reformulates the search for misclassifications into a standard probabilistic system synthesis problem. Third, we integrate the verification routine into an active automata learning routine to synthesize correct monitors. Fourth, we provide a prototypical implementation that shows the feasibility and limitations of the approach on a series of benchmarks.

Wed 29 Oct

Displayed time zone: Chennai, Kolkata, Mumbai, New Delhi change

14:00 - 15:30
Monitoring and Runtime VerificationATVA Papers at R102
Chair(s): Ichiro Hasuo National Institute of Informatics, Japan
14:00
30m
Paper
Efficient Dynamic Shielding for Parametric Safety Specifications
ATVA Papers
Davide Corsi University of California, Irvine, Kaushik Mallik IST Austria, Austria, Andoni Rodríguez IMDEA Software Institute, Spain, César Sánchez IMDEA Software Institute
14:30
30m
Paper
Learning Verified Monitors for Hidden Markov Models
ATVA Papers
Luko van der Maas Radboud University Nijmegen, Netherlands, Sebastian Junges Radboud University
15:00
30m
Paper
Prompt Runtime Enforcement
ATVA Papers
Ayush Anand Indian Institute of Technology Bhubaneswar, Loïc Germerie Guizouarn University of Rennes, France / Inria, France / CNRS, France / IRISA, France, Thierry Jéron INRIA, Sayan Mukherjee Univ Rennes, Inria, CNRS, IRISA, France, Srinivas Pinisetty Indian Institute of Technology Bhubaneswar, Ocan Sankur University of Rennes, France / Inria, France / CNRS, France / IRISA, France