In this paper, we present a mechanism for building hybrid system observers to differentiate between specific positions of the hybrid system. The mechanism is designed through inferring metric temporal logic (MTL) formulae from simulated trajectories from the hybrid system. We first approximate the system behavior by simulating finitely many trajectories with timerobust tube segments around them. These time-robust tube segments account for both spatial and temporal uncertainties that exist in the hybrid system with initial state variations. The inferred MTL formulae classify different time-robust tube segments and thus can be used for classifying the hybrid system behaviors in a provably correct fashion. We implement our approach on a model of a smart building testbed to distinguish two cases of room occupancy.
Download