Decentralized State Estimation and Opacity Verification Based on Partially Ordered Observation Sequences

TL;DR

This paper introduces a new framework for decentralized state estimation and opacity verification in discrete event systems using a CSS structure, enabling efficient analysis of system behavior and privacy properties.

Contribution

It proposes the CSS structure for concise state evolution representation and develops estimators for offline state estimation and opacity verification in decentralized settings.

Findings

CSS structure reduces complexity of state estimation.

Effective verification of initial-state and current-state opacity.

Framework applicable to systems with partially ordered observations.

Abstract

In this paper, we investigate state estimation and opacity verification problems within a decentralized observation architecture. Specifically, we consider a discrete event system whose behavior is recorded by a set of observation sites. These sites transmit the partially ordered sequences of observations that they record to a coordinator whenever a synchronization occurs. To properly analyze the system behavior from the coordinator's viewpoint, we first introduce the notion of a Complete Synchronizing Sequence structure (CSS structure), which concisely captures the state evolution of each system state upon different information provided by the observation sites. Based on the CSS structure, we then construct corresponding current-state and initial-state estimators for offline state estimation at the coordinator. When used to verify state-isolation properties under this decentralized architecture, the use of CSS structure demonstrates a significant reduction in complexity compared with existing approaches in the literature. In particular, we discuss how to verify initial-state opacity at the coordinator, as well as a novel opacity notion, namely current-state-at-synchronization opacity.