Robust Temporal Logic Inference for Provably Correct Fault Detection and Privacy Preservation of Switched Systems

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 t...

Full description

Saved in:
Bibliographic Details
Published in:IEEE systems journal 2019-09, Vol.13 (3), p.3010-3021
Main Authors: Xu, Zhe, Julius, A. Agung
Format: Article
Language:English
Subjects:
Computer simulation
Cyber-physical system (CPS)
Diffraction
Display systems
Fault detection
Holography
Image quality
Image reconstruction
Inference
metric temporal logic (MTL)
Occupancy
Privacy
privacy preservation
Robustness
Temporal logic
Three-dimensional displays
Trajectories
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:1932-8184
1937-9234
DOI:10.1109/JSYST.2019.2906160