Event Concealment and Concealability Enforcement in Discrete Event Systems Under Partial Observation
Wei Duan, Christoforos N. Hadjicostis, Zhiwu Li
TL;DR
The paper tackles privacy in discrete event systems under partial observation by formalizing event concealment and revealing when secret events become inferable. It develops a diagnoser-based method to verify concealability and proposes a defensive function to obfuscate observations, introducing the notion of $C$-enforceability to ensure perpetual concealment despite system activity. To maintain tractable analysis, the authors design polynomial-complexity constructions, including a verifier-perstyle framework and reduced verifiers, to derive necessary and sufficient conditions for enforceability. The results bridge concealability with diagnosability and opacity, and offer practical tools for enforcing privacy in cyber-physical systems through controlled output obfuscation. The work thus provides a rigorous foundation and scalable techniques for protecting secret-event privacy in DES with partial observation.
Abstract
Inspired by privacy problems where the behavior of a system should not be revealed to an external curious observer, we investigate event concealment and concealability enforcement in discrete event systems modeled as non-deterministic finite automata under partial observation. Given a subset of secret events in a given system, concealability holds if the occurrence of all secret events remains hidden to a curious observer (an eavesdropper). A secret event is said to be (at least under some executions) unconcealable (inferable) if its occurrence can be indirectly determined with certainty after a finite number of observations. When concealability of a system does not hold (i.e., one or more secret events are unconcealable), we analyze how a defender, placed at the interface of the system with the eavesdropper, can be used to enforce concealability. The defender takes as input each observed event of the system and outputs a carefully modified event sequence (seen by the eavesdropper) using event deletion, insertion, or replacement. The defender is said to be C-enforceable if, following the occurrence of the secret events and regardless of subsequent activity generated by the system, it can always deploy a strategy to manipulate observations and conceal the events perpetually. We discuss systematic procedures to detect the presence of unconcealable secret events and verify C-Enforceability using techniques from state estimation and event diagnosis. We also propose a polynomial complexity construction for obtaining one necessary and one sufficient condition for C-Enforceability.