Robust Temporal Logic Inference for Hybrid System Observation- An Application on Occupancy Detection of Smart Buildings

In modern smart buildings modeled as hybrid systems, occupancy detection can be cast as observing the discrete states of a hybrid system using the available discrete and continuous system outputs. In this paper, we present a method to construct observers of the hybrid system to distinguish between different locations of the hybrid system by inferring metric temporal logic (MTL) formulae from the simulated trajectories. We first approximate the system behavior by simulating finitely many trajectories with time-robust 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.