Design of decentralized critical observers for networks of finite state machines: A formal method approach

Motivated by safety-critical applications in cyber-physical systems, in this paper we study the notion of critical observability and design of observers for networks of Finite State Machines (FSMs). Critical observability corresponds to the possibility of detecting if the current state of an FSM is in a given region of interest, called set of critical states. A critical observer detects on-line the occurrence of critical states. When a large-scale network of FSMs is considered, the construction of such an observer is prohibitive because of the large computational effort needed. We propose a decentralized architecture for critical observers of networks of FSMs, where on-line detection of critical states is performed by local critical observers, each associated with an FSM of the network, which do not need to interact. For the efficient design of decentralized critical observers we first extend on-the-fly algorithms traditionally used in the community of formal methods for the verification and control design of FSMs. We then extend to networks of FSMs, bisimulation theory traditionally given in the community of formal methods for single FSMs. The proposed techniques provide a remarkable computational complexity reduction, as discussed throughout the paper and also demonstrated by means of illustrative examples.