A unified concurrent-composition method to state/event inference and concealment in discrete-event systems

TL;DR

This paper introduces a unified concurrent-composition method for verifying state/event inference and concealment properties in discrete-event systems, streamlining analysis and improving efficiency over previous separate approaches.

Contribution

It presents a novel unified framework that simultaneously verifies inference-based and concealment-based properties without relying on assumptions, enhancing efficiency and simplicity.

Findings

Unified method verifies multiple properties simultaneously

Method is more efficient than previous approaches

Does not depend on restrictive assumptions

Abstract

Discrete-event systems usually consist of discrete states and transitions between them caused by spontaneous occurrences of labelled (aka partially-observed) events. Due to the partially-observed feature, fundamental properties therein could be classified into two categories: state/event-inference-based properties (e.g., strong detectability, diagnosability, and predictability) and state-concealment-based properties (e.g., opacity). Intuitively, the former category describes whether one can use observed output sequences to infer the current and subsequent states, past occurrences of faulty events, or future certain occurrences of faulty events; while the latter describes whether one cannot use observed output sequences to infer whether some secret states have been visited (that is, whether the DES can conceal the status that its secret states have been visited). Over the past two decades these properties were studied separately using different methods. In this review article, for labeled finite-state automata, a unified concurrent-composition method is shown to verify all above inference-based properties and concealment-based properties, resulting in a unified mathematical framework for the two categories of properties. In addition, compared with the previous methods in the literature, the concurrent-composition method does not depend on assumptions and is more efficient.