TY - GEN
T1 - Robust Temporal Logic Inference for Hybrid System Observation- An Application on Occupancy Detection of Smart Buildings
AU - Xu, Zhe
AU - Deng, Yi
AU - Julius, Agung
N1 - Funding Information:
This research was partially supported by the National Science Foundation through grants CNS-1218109, CNS-1550029 and CNS-1618369
Funding Information:
Zhe Xu and Agung Julius are with the Department of Electrical, Computer, and Systems Engineering, Rensselaer Polytechnic Institute, Troy, NY, USA, E-mail: xuz8@rpi.edu, juliua2@rpi.edu. Yi Deng is with East China Institute of Computing Technology, Shanghai, China, E-mail: dengyi267@gmail.com. This research was partially supported by the National Science Foundation through grants CNS-1218109, CNS-1550029 and CNS-1618369.
Publisher Copyright:
© 2018 AACC.
PY - 2018/8/9
Y1 - 2018/8/9
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85052607514&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85052607514&partnerID=8YFLogxK
U2 - 10.23919/ACC.2018.8431834
DO - 10.23919/ACC.2018.8431834
M3 - Conference contribution
AN - SCOPUS:85052607514
SN - 9781538654286
T3 - Proceedings of the American Control Conference
SP - 610
EP - 615
BT - 2018 Annual American Control Conference, ACC 2018
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 2018 Annual American Control Conference, ACC 2018
Y2 - 27 June 2018 through 29 June 2018
ER -