TY - JOUR
T1 - Robust Temporal Logic Inference for Provably Correct Fault Detection and Privacy Preservation of Switched Systems
AU - Xu, Zhe
AU - Agung Julius, A.
N1 - Funding Information:
Manuscript received May 12, 2018; revised January 2, 2019 and March 10, 2019; accepted March 16, 2019. Date of publication April 18, 2019; date of current version August 23, 2019. This work was supported in part by the National Science Foundation under Grants CNS-1550029 and CNS-1618369. (Corresponding author: Zhe Xu.) Z. Xu is with the Institute for Computational Engineering and Sciences, University of Texas at Austin, Austin, TX 78712 USA (e-mail:,zhexu@utexas.edu). A. A. Julius is with the Department of Electrical, Computer, and Systems Engineering, Rensselaer Polytechnic Institute, Troy, NY 12180 USA (e-mail:, juliua2@rpi.edu). This paper has supplementary material available at http://ieeexplore.ieee.org. Digital Object Identifier 10.1109/JSYST.2019.2906160
Publisher Copyright:
© 2007-2012 IEEE.
PY - 2019/9
Y1 - 2019/9
N2 - In complex cyber-physical system operations, fault detection needs to be performed using limited state information for practicality and privacy concerns. While a well-designed observation can distinguish a faulty behavior from the normal behavior, it can also represent the action of hiding some of the state information or discrete mode switchings. In this paper, we present a method for constructing the observation maps in the form of metric temporal logic (MTL) formulas that can be formally proven to detect fault in a switched system, while preserving certain privacy conditions. We provide a theoretical framework of robust temporal logic inference for classification of switched system trajectories with spatial and temporal uncertainties. We simulate finitely many nominal trajectories and use the robust neighborhoods around the simulated trajectories to cover the infinite trajectories that constitute the system behavior. Thus, the designed observation maps with the inferred MTL formulas can detect fault and preserve privacy in a provably correct fashion. Our approach is implemented on the simulation model of a smart building testbed to detect thermal leakage in the room, while preserving multiple privacy conditions of the room occupancy.
AB - In complex cyber-physical system operations, fault detection needs to be performed using limited state information for practicality and privacy concerns. While a well-designed observation can distinguish a faulty behavior from the normal behavior, it can also represent the action of hiding some of the state information or discrete mode switchings. In this paper, we present a method for constructing the observation maps in the form of metric temporal logic (MTL) formulas that can be formally proven to detect fault in a switched system, while preserving certain privacy conditions. We provide a theoretical framework of robust temporal logic inference for classification of switched system trajectories with spatial and temporal uncertainties. We simulate finitely many nominal trajectories and use the robust neighborhoods around the simulated trajectories to cover the infinite trajectories that constitute the system behavior. Thus, the designed observation maps with the inferred MTL formulas can detect fault and preserve privacy in a provably correct fashion. Our approach is implemented on the simulation model of a smart building testbed to detect thermal leakage in the room, while preserving multiple privacy conditions of the room occupancy.
KW - Cyber-physical system (CPS)
KW - fault detection
KW - metric temporal logic (MTL)
KW - privacy preservation
UR - http://www.scopus.com/inward/record.url?scp=85071644275&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85071644275&partnerID=8YFLogxK
U2 - 10.1109/JSYST.2019.2906160
DO - 10.1109/JSYST.2019.2906160
M3 - Article
AN - SCOPUS:85071644275
VL - 13
SP - 3010
EP - 3021
JO - IEEE Systems Journal
JF - IEEE Systems Journal
SN - 1932-8184
IS - 3
M1 - 8693898
ER -