On Epistemic Properties in Discrete-Event Systems: A Uniform Framework and Its Applications

TL;DR

This paper introduces a unified framework for verifying epistemic properties in discrete-event systems with two independent observers, enabling analysis of information inference and knowledge-based security properties.

Contribution

It formalizes a general notion of epistemic properties for partially-observed systems and provides systematic verification methods, including efficient fragments for practical use.

Findings

Formalization of high-order opacity as an epistemic property

Systematic approach for verifying epistemic properties in DES

Identification of fragments with more efficient verification methods

Abstract

In this paper, we investigate the property verification problem for partially-observed DES from a new perspective. Specifically, we consider the problem setting where the system is observed by two agents independently, each with its own observation. The purpose of the first agent, referred to as the low-level observer, is to infer the actual behavior of the system, while the second, referred to as the high-level observer, aims to infer the knowledge of Agent 1 regarding the system. We present a general notion called the epistemic property capturing the inference from the high-level observer to the low-level observer. A typical instance of this definition is the notion of high-order opacity, which specifies that the intruder does not know that the system knows some critical information. This formalization is very general and supports any user-defined information-state-based knowledge between the two observers. We demonstrate how the general definition of epistemic properties can be applied in different problem settings such as information leakage diagnosis or tactical cooperation without explicit communications. Finally, we provide a systematic approach for the verification of epistemic properties. Particularly, we identify some fragments of epistemic properties that can be verified more efficiently.