The design of controllers for hybrid systems (i.e. mixed discrete-continuous systems) in a systematic manner remains a challenging task. In this case study, we apply formal modeling to the design of communication and control strategies for a team of autonomous robots to attain specified goals in a coordinated manner. The model of linear hybrid automata is used to describe the high-level design, and the verification software HyTech is used for symbolic analysis of the description. The goal of the project is to understand tradeoffs among various design alternatives by generating constraints among parameters using symbolic analysis. In this paper, we report on difficulties in modeling a team of robots using linear hybrid automata, results of analysis experiments, promise of the approach, and challenges for future research.
Proceedings of the World Congress on Formal Methods (FM'99), Lecture Notes in Computer Science 1708, Springer, pp. 212--232, 1999.