Scaling the formal synthesis of supervisory control software for multiple robot systems

Abstract

In this work we demonstrate a new approach for formally synthesizing control software for a set of cooperating ground robots. Existing discrete event system theory is applied to efficiently generate a set of modular supervisory controllers that are guaranteed to meet a given set of logical specifications (safety and nonblockingness). A subsequent synthesis step then chooses from the set of legal behaviors allowed by the modular supervisors. The efficiency of this planning step is improved through a novel combination of hierarchy and decomposition. Specifically, a global plan is generated off-line based on a formal abstraction of the full controlled system's behavior, while a local plan with a receding horizon is generated on-line based on an unabstracted model of the controlled system's behavior. The unabstracted model is built “on-the-fly” and only the portion of the model needed for the current local plan is stored at any given moment. This work also explains how the supervisory-level of control interacts with the robot-level algorithms that control each robot's heading and velocity. Finally, we present simulation results for a set of illustrative examples.