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

원문 초록

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 \textit{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.