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

Zhe Xu, A. Agung Julius

Research output: Contribution to journalArticlepeer-review

11 Scopus citations


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.

Original languageEnglish (US)
Article number8693898
Pages (from-to)3010-3021
Number of pages12
JournalIEEE Systems Journal
Issue number3
StatePublished - Sep 2019
Externally publishedYes


  • Cyber-physical system (CPS)
  • fault detection
  • metric temporal logic (MTL)
  • privacy preservation

ASJC Scopus subject areas

  • Control and Systems Engineering
  • Information Systems
  • Computer Science Applications
  • Computer Networks and Communications
  • Electrical and Electronic Engineering


Dive into the research topics of 'Robust Temporal Logic Inference for Provably Correct Fault Detection and Privacy Preservation of Switched Systems'. Together they form a unique fingerprint.

Cite this