A Unified Framework for Verification of Observational Properties for Partially-Observed Discrete-Event Systems
In this paper, 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. Furthermore, our unified framework also brings new insights for classifying observational properties for partially-observed DES in terms of their verification complexity.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
A unified concurrent-composition method to state/event inference and concealment in discrete-event systems
Discrete-event systems usually consist of discrete states and transitions between them caused by spontaneous occurrences of labelled (aka partially-observed) events. Due to the partially-observed feature, fundamental pro…
Traversing the Local Polytopes of ReLU Neural Networks: A Unified Approach for Network Verification
Although neural networks (NNs) with ReLU activation functions have found success in a wide range of applications, their adoption in risk-sensitive settings has been limited by the concerns on robustness and interpretabil…
Towards Partial Monitoring: It is Always too Soon to Give Up
Runtime Verification is a lightweight formal verification technique. It is used to verify at runtime whether the system under analysis behaves as expected. The expected behaviour is usually formally specified by means of…
Orthogonal Structure Search for Efficient Causal Discovery from Observational Data
The problem of inferring the direct causal parents of a response variable among a large set of explanatory variables is of high practical importance in many disciplines. Recent work exploits stability of regression coeff…
Causal DiscoveryregressionNeural Network Branching for Neural Network Verification
Formal verification of neural networks is essential for their deployment in safety-critical areas. Many available formal verification methods have been shown to be instances of a unified Branch and Bound (BaB) formulatio…
Graph Neural Network