Achieving distributed control through model checking
Tóm tắt
We apply model checking of knowledge properties to the design of distributed controllers that enforce global constraints on concurrent systems. The problem of synthesizing a distributed controller is undecidable in the general case. We thus look at a variant of the synthesis problem that allows adding temporary synchronizations between processes. We calculate when processes can decide autonomously, based on their knowledge, whether to take or block an action so that the global constraint is not violated. The local knowledge of processes may not suffice to control the processes so as to achieve the global constraint without introducing new deadlocks. When individual processes cannot take a decision alone based on their knowledge, one may coordinate several processes to achieve joint knowledge in order to take joint decisions. A fixed coordination among sets of processes may severely degrade concurrency. Therefore, we propose the use of temporary coordinations. Since realizing such coordinations on a distributed platform induces communication overhead, we strive to minimize their number. We show how this framework is applied to the case of synthesizing a distributed controller for enforcing a priority order. Finally, we show that the general undecidability of distributed synthesis without adding synchronization holds even for the particular problem of enforcing a priority order.
Tài liệu tham khảo
Basu A, Bensalem S, Peled D, Sifakis J (2009) Priority scheduling of distributed systems based on model checking. In: Proceedings of CAV’09. LNCS, vol 5643. Springer, Berlin, pp 79–93
Bensalem S, Bozga M, Graf S, Peled D, Quinton S (2010) Methods for knowledge-based controlling of distributed systems. In: Proceedings of ATVA’10. LNCS, vol 6252. Springer, Berlin, pp 52–66
Fagin R, Halpern JY, Vardi MY, Moses Y (1995) Reasoning about knowledge. MIT Press, Cambridge
Genrich HJ, Lautenbach K (1981) System modelling with high-level petri nets. Theor Comput Sci 13:109–136
Katz G, Peled D (2010) Code mutation in verification and automatic code correction. In: Proceedings of TACAS’10. LNCS, vol 6015. Springer, Berlin, pp 435–450
Katz G, Peled D, Schewe S (2011) Synthesis of Distributed Control through Knowledge Accumulation. In: Proceedings of CAV’11. LNCS, vol 6807. Springer, Berlin, pp 510–525
Keller RM (1976) Formal verification of parallel programs. Commun ACM 19(7):371–384
van der Meyden R (1998) Common knowledge and update in finite environment. Inf Comput 140(2):115–157
Orlin JB (1977) Contentment in graph theory: covering graphs with cliques. Indag Math 80(5):406–424
Pérez JA, Corchuelo R, Toro M (2004) An order-based algorithm for implementing multiparty synchronization. Concurr Pract Exp 16(12):1173–1206
Rudie K, Ricker SL (2000) Know means no: Incorporating knowledge into discrete-event control systems. IEEE Trans Autom Control 45(9):1656–1668
Rudie K, Wonham WM (1992) Think globally, act locally: decentralized supervisory control. IEEE Trans Autom Control 37(11):1692–1708
Thistle JG (2005) Undecidability in decentralized supervision. Syst Control Lett 54:503–509
Thomas W (1995) On the synthesis of strategies in infinite games. In: Proceedings of STACS’95. LNCS, vol 900. Springer, Berlin, pp 1–13
Tripakis S (2004) Undecidable problems of decentralized observation and control on regular languages. Inf Process Lett 90(1):21–28
Yoo TS, Lafortune S (2002) A general architecture for decentralized supervisory control of discrete-event systems. Discret Event Dyn Syst 12(3):335–377