Methods for Knowledge Based Controlling of Distributed Systems

S. Bensalem, M. Bozga, S. Graf, D. Peled & S. Quinton.
International Symposium on Automated Technology for Verification and Analysis, ATVA 2010, September 2010, Singapore, LNCS 6252, pages 52-66
Controlling concurrent systems to impose some global invariant, is an undecidable problem. One can gain decidability at the expense of reducing concurrency. Even under this flexible design assumption, the synthesis problem remains highly intractable. One practical method for designing controllers is based on checking knowledge properties upon which the processes can make their decisions whether to allow or block transitions. A major deficiency of this synthesis method lies in calculating the knowledge based on the system that we want to control, and not on the resulted system. The original system has less knowledge, and as a result, we may introduce far more synchronization than needed. In this paper we show techniques to reduce this overhead.