Formal Modeling and Analysis of Hybrid Systems: A Case Study in Multi-robot Coordination

Abstract. The design of controllers for hybridsystemsi.e. mixeddiscretecontinuous 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 speci ed goals in a coordinated manner. The model of linear hybrid automata is used to describe the high-level design, and the veri cation software HyTechis used for symbolic analysis of the description. The goal of the project is to understand tradeo s among various design alternatives by generating constraints among parameters using symbolic analysis. In this paper, we report on di culties in modeling a team of robots using linear hybrid automata, results of analysis experiments, promise of the approach, and challenges for future research.

• Type: Conference
• Year: 1999
• Where: FM
• Authors: Rajeev Alur, Joel M. Esposito, M. Kim, Vijay Kumar, Insup Lee
• Keywords: FM 1999, Formal Methods, Linear Hybrid Automata, Symbolic Analysis, Veri Cation Software