A Unified Framework for Verification of Observational Properties for Partially-Observed Discrete-Event Systems

In this article, we investigate property verification problems in partially-observed discrete-event systems (DES). Particularly, we are interested in verifying observational properties that are related to the information-flow of the system. Observational properties considered here include diagnosability, predictability, detectability, and opacity, which have drawn considerable attentions in the literature. However, in contrast to existing results, where different verification procedures are developed for different properties case by case, in this work, we provide a unified framework for verifying all these properties by reducing each of them as an instance of HyperLTL model checking. Our approach is based on the construction of a Kripke structure that effectively captures the issue of unobservability as well as the finite string semantics in partially-observed DES so that HyperLTL model checking techniques can be suitably applied. Then for each observational property considered, we explicitly provide the HyperLTL formula to be checked over the Kripke structure for the purpose of verification. Our approach is uniform in the sense that all different properties can be verified with the same model checking engine and also brings new insights for classifying observational properties in terms of their verification complexity. Numerical experiments are conducted, which show that our framework is computationally more efficient for verifying properties involving quantifier alternations, such as opacity, compared with the standard subset-based approaches.