Symbolic Synthesis of Observability Requirements for Diagnosability

Given a partially observable dynamic system and a diagnoser observing its evolution over time, diagnosability analysis formally verifies (at design time) if the diagnosis system will be able to infer (at runtime) the required information on the hidden part of the dynamic state. In this paper, we address a problem that generalizes diagnosability to discovering a set of parameters to be observed that is sufficient to guarantee diagnosability. We propose a novel approach to the synthesis of observability requirements, with the following characterizing features. First, it fully covers a comprehensive formal framework for diagnosability analysis, and extends it to define cost-optimized configurations of observables. Second, we propose two complementary algorithms for the synthesis of observables. Third, we describe an implementation that takes full advantage of mature symbolic model checking techniques. The proposed approach is thoroughly evaluated over a comprehensive suite of realistic benchmarks taken from the aerospace domain.