Reactive property monitoring of hybrid systems with aggregation

Abstract

This work is related to our monitoring tool called ARTi-Mon for the property monitoring of hybrid systems. We explain how the aggregation operator of its language derives naturally from a generalization of the eventually operator as introduced by Maler and Nickovik for MITL[a,b]. We present its syntax and its semantics using an interval based representation of piecewise-constant functions. We define an online algorithm for its semantics calculus coupled with an elimination of irrelevant intervals in order to keep the memory resource bounded.