Model-bounded Monitoring of Hybrid Systems

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 modelbounded 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 algorithmsone is via reduction to reachability in LHAs and the other is a direct one using polyhedra-and showthat these methods, and thus the proposed model-bounded monitoring scheme, are efficient and practically relevant.