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.
翻译:混合系统的监控问题引起了学术界和工程界的广泛关注。然而,监控算法面临方法学上的困难:只能观测离散时间采样信号,而实际行为是连续时间信号。为缓解采样不确定性带来的问题,我们提出了一种模型有界监控方案,利用目标系统的先验知识来剪枝插值候选。在技术上,我们使用线性混合自动机(LHAs)表达此类先验知识——这些LHAs被称为边界模型。我们引入了LHA监控语言的新概念,并将监控问题归约为监控语言的成员判定问题。我们提出了两种部分算法——一种通过归约为LHA可达性问题,另一种是直接使用多面体方法——并证明这些方法及所提出的模型有界监控方案具有高效性和实际应用价值。