Model Checking Hybrid Multiagent Systems for the RoboCup

Abstract. This paper shows how multiagent systems can be modeled by a combination of UML statecharts and hybrid automata. This allows formal system cation on different levels of abstraction on the one hand, and expressing real-time system behavior with continuous variables on the other hand. It is shown how multi-robot systems can be modeled by hybrid and hierarchical state machines and how model checking techniques for hybrid automata can be applied. An enhanced synchronization concept is introduced that allows synchronization taking time and avoids state explosion to a certain extent. 1 Multiagent Systems Specifying behaviors for (physical) multiagent systems and multi-robot systems is a sophisticated and demanding task. Due to the high complexity of the interactions among agents and the dynamics of the environment the need for precise modeling arises. Since the behavior of agents usually can be understood as driven by external events and internal states, an obvious way of modeling m...

• Type: Conference
• Year: 2007
• Where: ROBOCUP
• Authors: Ulrich Furbach, Jan Murray, Falk Schmidsberger, Frieder Stolzenburg
• Keywords: Hybrid Automata, Multiagent Systems, ROBOCUP 2007, State Transition Diagrams