Model-bounded monitoring of hybrid systems
Masaki Waga, Étienne André, Ichiro Hasuo
TL;DR
The paper tackles the challenge of inferring continuous-time hybrid-system behaviors from infrequently sampled logs by introducing model-bounded monitoring, which uses Linear Hybrid Automata (LHAs) as bounding models to constrain interpolation. It defines a novel monitored language $\mathcal{L}_{\mathrm{mon}}$ and reduces monitoring to a membership problem within this language, proposing two partial, sound algorithms: one via reduction to LHA reachability (using PHAVerLite) and one based on direct polyhedra computation. The approach is validated through extensive experiments on automotive platooning, navigation, and gas-burner benchmarks, showing practical scalability and robustness, albeit with undecidability caveats and potential false alarms when the bounding model is imprecise. The work offers a principled, automata-based framework for monitoring CPS under sampling uncertainties, with clear pathways to extensions toward temporal properties, partial observations, and quantitative guarantees, highlighting its utility for real-world, safety-critical systems. Overall, model-bounded monitoring provides a scalable and sound mechanism to reason about safety under interpolation, leveraging convex polyhedra and LHA-based analysis to bound the gap between discrete logs and continuous-time behaviors.
Abstract
Monitoring of hybrid systems attracts both scientific and practical attention. However, monitoring algorithms suffer from the methodological difficulty of only observing sampled discrete-time signals, while real behaviors are continuous-time signals. To mitigate this problem of sampling uncertainties, we introduce a model-bounded monitoring scheme, where we use prior knowledge about the target system to prune interpolation candidates. Technically, we express such prior knowledge by linear hybrid automata (LHAs) -- the LHAs are called bounding models. We introduce a novel notion of monitored language of LHAs, and we reduce the monitoring problem to the membership problem of the monitored language. We present two partial algorithms -- one is via reduction to reachability in LHAs and the other is a direct one using polyhedra -- and show that these methods, and thus the proposed model-bounded monitoring scheme, are efficient and practically relevant.