A formally verified modular decentralized robot control system

This paper addresses the design, verification and implementation of a fully decentralized linear quadratic Gaussian (LQG) control system based on transputer architecture. A decentralized, information filter is developed and extended to solve the decentralized control problem, keeping consistency with information space ideas. Locally processed information is shared by all nodes, so that optimal control is computed using the best, locally determined, global state estimate. There is no central processing site, and hence the system performance degrades gracefully under structural perturbations. The designed system is modeled and verified using Communicating Sequential Process (CSP) algebra. Software is developed in Parallel ANSI C. A simulated test implementation is effected using transputer-based hardware. Validation and performance analysis are carried out. Application to intelligent control of a modular, decentralized navigating robot is considered