Synthesis of distributed control systems

Abstract

This paper presents an indexed computation tree logic formula template that encodes under certain mild restrictions and provides a format for specifying safety and progress properties for the system as a whole. It then presents a simple method of converting a synthesized finite-state model of such a formula into a message-passing controller and a communication protocol for its clients. Finally, it proves the correctness of the resulting distributed control system.