On Language-Based Opacity Verification Problem in Discrete Event Systems Under Orwellian Observation

Opacity is an important information flow property that is concerned with the secret leakage of a system to a malicious observer called an “intruder”. Usually, opacity analyses are made under static or dynamic observation, i.e., the observability of events in a system is fixed or changeable over time by a mask. In this paper, we address the verification of language-based opacity in the context of discrete-event systems under Orwellian observation. We consider an Orwellian partial observability model, where some unobservable events, not visible when occurring, may become noticeable in the future. Specifically, we propose a set of unobservable events that are no longer unobservable once an event in another particular disjoint event subset is triggered. First, we define and solve an integer linear programming problem to verify language-based opacity in discrete event systems using labeled Petri nets. We then propose a new Orwellian projection function that is event-based, i.e., the system is allowed to re-interpret the observation of the already triggered events when a particular observable event occurs. Finally, the verification of language-based opacity in discrete event systems under Orwellian projection is addressed.