Using Formal Modeling With an Automated Analysis Tool to Design and Parametrically Analyze a Multirobot Coordination Protocol: A Case Study

Many robot systems employ logic-based or reactive controllers, making them hybrid systems (i.e., mixed discrete continuous). However, designing such control laws in a systematic manner remains a challenging task. In this paper, we apply the formal modeling paradigm to a team of mobile robots. The linear hybrid automata modeling framework is used to describe the high-level design, and the verification software HyTech is used for symbolic analysis of the description. The goal is to symbolically quantify system-level performance as a function of the design parameters, for the purpose of optimizing and synthesizing design parameters, verifying safe operation, and quantitatively exploring tradeoff issues. In order to make the analysis tractable, a series of restrictive assumptions and simplifications must be made-some dictated by the linear hybrid automata model and others necessitated by computational cost. We comment on the restrictiveness of these assumptions and the overall utility of this automated analysis approach in designing complex robotic systems