Critical Observability of Networks of Finite State Machines

This paper deals with the analysis of critical observability for networks of Finite State Machines (FSMs). Critical observability is a property of FSMs that corresponds to the possibility of detecting whether the current state of an FSM is, or is not, in a set of critical states modeling unsafe operations. The study of this property is relevant in safety-critical applications, as for example Air Traffic Management (ATM) systems where the timely recovery of human operators errors and technical devices disruption is of primary importance in ensuring safety of the ATM procedures. In general, for checking this property, a critical observer is designed which detects on-line the occurrence of critical situations. When a large-scale network of FSMs is considered, the construction of such an observer is prohibitive because of the large computational effort needed. In this paper we present an approach based on bisimulation equivalence which reduces the original network to a smaller one while preserving the critical observability property. Further, we show that a critical observer designed for the reduced network can be utilized for the original network. The advantages of the proposed approach in terms of computational complexity are discussed in the paper.