PaperlayerView exact revision on arXiv

Source-linked AI summary

Existential Opacity for Discrete-Event Systems with State Observations

Zhiyuan Huang, Zhao Tong, Jiakai Li, Bingzhuo Zhong

arXiv:2609.02132v1eess.SY

TL;DR

Existing state-observation opacity does not fully characterize opacity-preserving tasks when only some secret behaviors need indistinguishable alternatives. The paper introduces existential opacity and related verification approaches, showing that EO is equivalent to opacity-preserving feasibility and extends classical state-observation opacity.

  • Problem

    Existing state-observation-based opacity may not characterize systems where opacity-preserving execution requires only the existence of suitable secret behaviors.

  • Method

    The paper defines existential opacity over state sequences and develops a current-state variant with corresponding verification methods for transition systems.

  • Results

    EO is more expressive than state-observation opacity and is equivalent to feasibility of the opacity-preserving problem.

  • Takeaways & Limitations

    EO provides a system-level criterion for analyzing whether opacity-preserving task execution is feasible under state observations.

Abstract

from arXiv · show

Opacity is a fundamental system property for confidentiality in discrete-event systems (DES). Classical opacity is typically defined under event-based observations, requiring that any secret system behavior remains indistinguishable from some non-secret behavior to an external intruder. However, in many applications such as path planning or opacity-preserving tasks, the intruder observes system states rather than events. Moreover, it often suffices that the system exhibits secret behaviors that can be exploited for opacity-preserving task execution, but such a system property cannot be fully captured by existing notions of state-observation-based opacity. Motivated by this limitation, we propose a relaxed notion of existing state-observation-based opacity, called existential opacity (EO), which only requires the existence of secret behaviors (instead of all secret behaviors) that are indistinguishable from a non-secret behavior under the state observations of the intruder. We show that the notion of EO is more expressive than existing state-observation-based opacity notions. In addition, a class of EO properties together with their corresponding verification approaches are developed, enabling the analysis of existential opacity in discrete-event systems and providing a new criterion for determining the feasibility of opacity-preserving problems.

I. INTRODUCTION

The paper addresses the mismatch between state-observation-based opacity and opacity-preserving tasks in discrete-event systems. It introduces existential opacity, requiring only some secret behaviors to remain indistinguishable from non-secret behaviors.

  • Discrete-event systems support systematic modeling, analysis, and verification of event-driven dynamics across applications including robotics, traffic networks, and software.
  • Opacity traditionally requires every secret behavior to have an observationally equivalent non-secret behavior for an external intruder.
  • State observations matter in practical opacity-preserving problems, but existing approaches focus on executions or controllers without characterizing the underlying system property guaranteeing them.
  • Existential opacity requires the existence of indistinguishable secret and non-secret behaviors under state observations, rather than requiring this for all secret behaviors.
  • The paper develops a current-step existential opacity class and verification method that provides a criterion for opacity-preserving problem feasibility.

A. Motion ability abstraction

The system’s motion is abstracted as a finite deterministic transition system over workspace regions. Paths are sequences of states generated by admissible control inputs.

  • A. Motion ability abstraction: The workspace is partitioned into finitely many regions represented as states of a finite transition system.
  • A. Motion ability abstraction: The model includes initial states, control inputs, transitions, movement costs, atomic propositions, and a labeling function for regional properties.
  • A. Motion ability abstraction: Determinism ensures that any state and control input have at most one successor state.
  • A. Motion ability abstraction: An infinite path is a state sequence beginning in an initial state, while an n-step finite path is its prefix through state π(n).

B. Intruder model and Opacity

The paper models a passive intruder that observes state-related outputs and defines opacity over admissible, secret, and non-secret paths. Classical state-observation opacity is sufficient but not necessary for opacity-preserving feasibility.

  • B. Intruder model and Opacity: The intruder observes state-related outputs while having full knowledge of the transition-system model.
  • B. Intruder model and Opacity: Admissible paths satisfy selected tasks, secret paths exhibit secret behaviors, and non-secret paths are admissible paths outside the secret set.
  • B. Intruder model and Opacity: State-observation opacity requires every secret path to have a non-secret path with the same observation sequence.
  • B. Intruder model and Opacity: The opacity-preserving problem designs control inputs so the controlled system remains opaque, with feasibility defined by the existence of a suitable control strategy.
  • B. Intruder model and Opacity: State-observation opacity guarantees feasibility but is not necessary, because feasible control may exploit only selected secret paths rather than all secret paths.

III. MOTIVATION AND PROBLEM FORMULATION

A motivating workspace example shows that some secret paths are uniquely identifiable while others remain indistinguishable from non-secret paths. Therefore, failure of universal opacity does not determine whether opacity-preserving execution is feasible.

  • III. MOTIVATION AND PROBLEM FORMULATION: Physical constraints, environmental topology, and task requirements can make certain secret behaviors uniquely distinguishable to the intruder.
  • III. MOTIVATION AND PROBLEM FORMULATION: In the example, observation O1O2O2 identifies the path q1q2q4 because no other non-secret path produces the same observation.
  • III. MOTIVATION AND PROBLEM FORMULATION: For path q1q1q2, a non-secret path q1q3q4 produces the same observation O1O1O2, preventing the intruder from inferring the secret visit.
  • III. MOTIVATION AND PROBLEM FORMULATION: The example demonstrates that state-observation opacity can fail while secret paths still have indistinguishable non-secret alternatives.

A. Existential Opacity

Existential opacity (EO) requires at least one secret path to have an indistinguishable non-secret counterpart under state observations. It is more expressive than universal state-observation opacity and exactly characterizes feasibility of the opacity-preserving problem.

  • Definition: EO holds when at least one secret path and one non-secret path have identical intruder observations.The definition requires ∃τ ∈φs and ∃τ′ ∈¯φs such that H(τ) = H(τ′).
  • Relation to opacity: EO is more expressive than the original opacity notion because universal opacity implies EO, but the converse does not generally hold.Original opacity covers every secret path, whereas EO requires only one indistinguishable secret/non-secret pair.
  • Opacity-preserving feasibility: EO is equivalent to feasibility of the opacity-preserving problem.The forward direction uses an EO secret path and system determinism to obtain a control strategy generating it; the converse follows from a feasible strategy.
  • Applications: EO can represent different security properties by specifying admissible paths and secret paths for tasks, secret states, initial states, or secret specifications.Admissible paths may satisfy a task specification, while secret paths may encode visits to secret states, secret initial states, or other secret requirements.

V. VERIFICATION OF EXISTENTIAL OPACITY

The verification discussion specializes existential opacity to path-based secrets, where secrecy occurs when a path visits a designated secret state. This specialization uses secret and non-secret state sets to support verification.

  • Verification scope: Verification of EO directly determines opacity-preserving feasibility for the corresponding admissible and secret path sets.The paper focuses on path-based secrets in which a secret is incurred by visiting a designated secret state.
  • Path-based secrets: Secret states are represented by Πs ⊂Π, and non-secret states are defined as Πns = Π \ Πs.This state partition provides the basis for identifying path-based secret behavior.

A. Current-State Existential Opacity

Current-state existential opacity (CSEO) requires one system path whose secret states remain observationally compatible with non-secret states at every relevant prefix. CSEO therefore implies EO for the associated finite-path sets.

  • Path sets: The admissible set for CSEO consists of finite prefixes τ(0,n) of infinite system paths.The corresponding secret set contains prefixes whose final state π(n) belongs to Πs.
  • Definition: CSEO requires a path such that every secret state along it has a same-prefix observation matched by a non-secret state.For each step k with π(k) ∈Πs, a path τ′ must satisfy π′(k) ∉Πs and H(τ(0,k)) = H(τ′(0,k)).
  • Current-state inference: CSEO bases secret inference on observation sequences of path prefixes up to the current step.The intruder evaluates whether the system is currently secret using H(τ(0,n)).
  • Relation to EO: If T is CSEO, then T is EO under D(T) = DCSO(T) and the associated secret-path definition.This establishes CSEO as a sufficient condition for the broader existential-opacity property.

B. Verification Methods

The verification method constructs an observer transition system that tracks the actual state, observationally consistent states, and a marker identifying whether secret states have non-secret observational alternatives. For CSEO, verification reduces to checking reachability in a reduced observer transition system after removing violating marker states.

  • Observer transition system: The observer transition system (OTS) augments each transition-system state with its consistent-state set and a marker representing opacity status.An observer state is a triple πo = (π, C(π), m), with markers {1}, {2}, or ∅ determined by the relationship between the current state and its observationally consistent alternatives.
  • Observer transition system: The OTS updates consistent-state sets by retaining reachable successor states whose observation histories remain consistent with the intruder’s observations.Its paths combine the motion transitions of the original system with the observation information available to the intruder.
  • Consistency characterization: Theorem 2 establishes that C(π(k)) is exactly the set of reachable states consistent with the observed execution prefix H(τ(0, k)).Corollary 2 further associates every state in this set with a path in the original transition system producing the same observation prefix.
  • CSEO verification: CSEO holds iff there exists an OTS path where every secret observer state has marker {1}, indicating at least one non-secret observationally consistent state.Marker {2} denotes a secret state whose consistent-state set contains only secret states and therefore violates the CSEO requirement.

VI. CASE STUDY

The case study evaluates CSEO under two different initial and secret-state configurations. Case I is CSEO because an acceptable marked state is reachable in the ROTS, whereas Case II is not because that state is unavailable there.

  • Case I: In Case I, Π0 = {q1} and Πs = {q2}; the ROTS reaches (q2, {q2, q4}, {1}), so the transition system is CSEO.The ROTS is formed by removing the states and transitions marked in red in the OTS.
  • Case II: In Case II, Π0 = {q2} and Πs = {q4}; every path visiting (q4, {q2, q4}, {1}) also visits (q4, {q4}, {2}), so the system is not CSEO.The marker-{1} state is not reachable in the ROTS after marker-{2} states and incident transitions are removed.

VII. CONCLUSION

The paper studies state-observation-based opacity and introduces existential opacity as a relaxed property for transition systems observed by a passive intruder. It also defines CSEO with a verification method, while leaving additional existential-opacity types and their relationships to specific problems for future work.

  • Conclusion: The paper introduces existential opacity to address limitations of state-observation-based opacity and examines its relationship with opacity-preserving problem feasibility.It also studies the relationship between existential opacity and state-observation-based opacity.
  • Conclusion: The paper defines CSEO, a specific existential-opacity type, and proposes a method to verify whether a system satisfies it.The supplied conclusion identifies CSEO verification as a concrete outcome of the work.
  • Conclusion: Future work will explore additional existential-opacity types, develop corresponding verification approaches, and study their relation to specific opacity-preserving problems.The conclusion states this as the paper’s planned extension.
Loading 2609.02132v1…