Fault Detection of Discrete-Time Stochastic Systems Subject to Temporal Logic Correctness Requirements

This paper studies the fault detection of discrete-time stochastic systems with linear-time temporal logic (LTL) as correctness requirement-A fault is a violation of LTL specification. The temporal logic allows system correctness properties to be specified compactly and in a user-friendly manner (being close to natural-languages), and supports automatic translation into other formal models such as automata. We introduce the notion of input-output stochastic hybrid automaton (I/O-SHA) and show that the refinement of a continuous physical system (modeled as stochastic difference equations) against a certain class of LTL correctness requirement can be modeled as an I/O-SHA. The refinement preserves the behaviors of the physical system and also captures requirement-violation as a reachability property. Probability distribution over the discrete locations of hybrid system is estimated recursively by computing the distributions for continuous variables for each discrete location. This is then used to compute the likelihood of fault, a statistic that we employ for the purpose of fault detection. The performance of the detection scheme is measured in terms of false alarm (FA) and missed detection (MD) rates, and the condition for the existence of a detector to achieve any desired rates of FA and MD is captured in form of Stochastic-Diagnosability, a notion that we introduce in this paper for stochastic hybrid systems. The proposed method of fault detection is illustrated by a practical example.