Model-bounded monitoring of hybrid systems

TL;DR

This paper introduces a model-bounded monitoring scheme for hybrid systems using prior knowledge expressed by linear hybrid automata, improving the accuracy and practicality of monitoring continuous-time behaviors from sampled data.

Contribution

It proposes a novel monitoring framework that leverages bounding models to reduce sampling uncertainties in hybrid systems, with two efficient algorithms for implementation.

Findings

The proposed methods are efficient and practically relevant.

The monitoring scheme effectively reduces sampling uncertainties.

Algorithms are based on reachability and polyhedral computations.

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.