Multi-Robot Systems: Modeling, Specification, and Model Checking

Specifying behaviors of physical multi-agent systems (MAS) – also called multi-robot systems – is a demanding task, especially when they are applied in safety critical applications. For this, formal methods based on mathematical models of the system under design are helpful. They allow us not only to formally specify the system at different levels of abstraction, but also to analyze the consistency of the specified systems before implementing them. The formal specification aims at both, a precise and unambiguous description of the behavior of MAS, and a formal verification whether a given specification is satisfied. For example, it should be possible to show that unsafe regions of the state space cannot be reached, or that a particular property is satisfied. Generally, the behavior of an agent in MAS can be driven by external events and internal states. Therefore, an efficient way to model such systems is to use state transition diagrams, which are well established in software engineering. A state transition diagram describes the dynamic behaviour of an agent in terms of how the agent acts in certain scenarios of the