Abstract
Discrete-event systems (DESs) usually consist of discrete states and transitions between them caused by spontaneous occurrences of labelled events. In this review article, we study DESs modeled by labeled (nondeterministic) finite-state automata (LFSAs). Due to the partially-observed feature of DESs, fundamental properties therein can 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 describe 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 describe whether one cannot use observed output sequences to infer whether 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, and particularly, in most works inference-based properties were verified based on two fundamental assumptions of deadlock-freeness and divergence-freeness, where the former implies that an automaton will always run, the latter implies that an automaton has no reachable unobservable cycle, hence the running of such an automaton will always be eventually observed. In this article, for LFSAs, a unified concurrent-composition method is shown to verify all above inference-based 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 currently the most efficient. Finally, based on concurrent composition, we represent the negations of the above inference-based properties as linear temporal logic (LTL) formulae; by combining the concurrent composition and an additional tool called observer (i.e., the classical powerset construction for LFSAs), we also represent the above concealment-based properties as LTL formulae. Although LTL formulae model checking algorithms do not provide more efficient verification for these inference-based and concealment-based properties, the obtained LTL formulae show common similarities among these properties.