×

Design of decentralized critical observers for networks of finite state machines: a formal method approach. (English) Zbl 1375.93014

Summary: 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 online 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 online 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.

MSC:

93A15 Large-scale systems
93B07 Observability
68P30 Coding and information theory (compaction, compression, models of communication, encoding schemes, etc.) (aspects in computer science)
68Q80 Cellular automata (computational aspects)

Software:

UMDES
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Cassandras, C. G.; Lafortune, S., Introduction to discrete event systems (1999), Kluwer Academic Publishers · Zbl 0934.93001
[2] Contant, O.; Lafortune, S.; Teneketzis, D., Diagnosability of discrete event systems with modular structure, Discrete Event Dynamic Systems, 16, 9-37 (2006) · Zbl 1134.93306
[3] Courcoubetis, C.; Vardi, M.; Wolper, P.; Yannakakis, M., Memory-efficient algorithms for the verification of temporal properties, Formal Methods in System Design, 1, 2-3, 275-288 (1992)
[5] De Santis, E.; Di Benedetto, M. D.; Di Gennaro, S.; D’Innocenzo, A.; Pola, G., (Critical observability of a class of hybrid systems and application to air traffic management. Critical observability of a class of hybrid systems and application to air traffic management, Lecture notes on control and information sciences (2005), Springer Verlag), (Book Chapter) · Zbl 1130.93319
[6] Di Benedetto, M. D.; Di Gennaro, S.; D’Innocenzo, A., Discrete state observability of hybrid systems, International Journal of Robust and Nonlinear Control, Special Issue on Observability and Observer Design for Hybrid Systems, 19, 14, 1564-1580 (2008) · Zbl 1298.93079
[7] Lin, F.; Wonham, W., On observability of discrete-event systems, Information Sciences, 44, 173-198 (1988) · Zbl 0644.93008
[9] Milner, R., Communication and concurrency (1989), Prentice Hall · Zbl 0683.68008
[10] Paige, R.; Tarjan, R., Three partition refinement algorithms, SIAM Journal on Computing, 16, 6, 987-989 (1987) · Zbl 0654.68072
[11] Park, D. M.R., (Concurrency and automata on infinite sequences. Concurrency and automata on infinite sequences, Lecture notes in computer science, vol. 104 (1981), Springer-Verlag), 167-183 · Zbl 0457.68049
[14] Rudie, K.; Lafortune, S.; Lin, F., Minimal communication in a distributed discrete-event system, IEEE Transactions on Automatic Control, 48, 957-975 (2003) · Zbl 1364.93482
[15] Rudie, K.; Wonham, W., Think globally, act locally: decentralized supervisor control, IEEE Transactions on Automatic Control, 37, 11, 1692-1708 (1989) · Zbl 0778.93002
[16] Sampath, M.; Sengupta, R.; Lafortune, S.; Sinnamohideen, K.; Teneketzis, D., Diagnosability of discrete-event systems, IEEE Transactions on Automatic Control, 40, 9, 1555-1575 (1995) · Zbl 0839.93072
[17] Schmidt, K. W., Verification of modular diagnosability with local specifications for discrete-event systems, IEEE Transactions on Systems, Man and Cybernetics, 43(5), 1130-1140 (2013)
[18] Shu, S.; Lin, F.; Ying, H., Detectability of discrete event systems, IEEE Transactions on Automatic Control, 52, 12, 2356-2359 (2007) · Zbl 1366.93366
[19] Su, R.; Wonham, W. M., Global and local consistencies in distributed fault diagnosis for discrete-event systems, IEEE Transactions on Automatic Control, 50, 12, 1923-1935 (2005) · Zbl 1365.93303
[20] Tripakis, S.; Altisen, K., On-the-fly controller synthesis for discrete and dense-time systems, (World congress on formal methods in the development of computing systems. World congress on formal methods in the development of computing systems, Lecture notes in computer science, vol. 1708 (1999), Springer Verlag: Springer Verlag Berlin), 233-252 · Zbl 1037.93522
[21] Wang, W.; Girard, A. R.; Lafortune, S.; Lin, F., On codiagnosability and coobservability with dynamic observations, IEEE Transactions on Automatic Control, 56, 7, 1551-1566 (2011) · Zbl 1368.93392
[22] Wang, W.; Lafortune, S.; Girard, A. R.; Lin, F., Optimal sensor activation for diagnosing discrete event systems, Automatica, 46, 1165-1175 (2010) · Zbl 1194.93140
[23] Wang, W.; Lafortune, S.; Lin, F., An algorithm for calculating indistinguishable states and clusters in finite-state automata with partially observable transitions, Systems & Control Letters, 56, 656-661 (2007) · Zbl 1155.93387
[24] Wang, W.; Lafortune, S.; Lin, F.; Girard, A. R., Minimization of dynamic sensor activation in discrete event systems for the purpose of control, IEEE Transactions on Automatic Control, 55, 2447-2461 (2010) · Zbl 1368.93393
[25] Zad, S. H.; Kwong, R. H.; Wonham, W. M., Fault diagnosis in discrete-event systems: framework and model reduction, IEEE Transactions on Automatic Control, 48, 7, 51-65 (2003) · Zbl 1364.93464
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.