Decentralized Critical Observers of Networks of Finite State Machines and Model Reduction

Abstract

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 is a property of FSMs that corresponds to the possibility of detecting if the current state of an FSM belongs to a set of critical states modeling operations that may be unsafe or, in general, operations of specific interest in a particular application. A critical observer is an observer that 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. In this paper 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. 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 formal 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. Finally, we propose an example in the context of biological networks, which illustrates the applicability of our results and also the interest arising from concrete application domains.