Abstract. This paper shows how multiagent systems can be modeled by a combination
of UML statecharts and hybrid automata. This allows formal system
specication 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.