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

Abstract

In this chapter, we have shown a framework to formally specify and verify physical multiagent systems by means of hybrid automata, especially for those agents that are defined through their capability to continuously react to a physical environment, while respecting some time constraints. The framework provided two different views of behaviors' specifications, namely, the concurrent and the hierarchical view. In the concurrent view, it has been demonstrated how to avoid the composition of the agents before getting involved into the verification phase,which, in turn can relieve the state explosion problem that may raise as the result of specifying multi-agent systems. On the other hand, in the hierarchical view, we show how multi-agent systems can be hierarchically specified and formally verified without flattening the hierarchy, as it is commonly done. We have shown the implementations of both views