An Approach to Compositional Verification of Reactive Multiagent Systems
Jean–Michel Contet, Pablo Gruer, Franck Gechter, Abderrafìâa Koukam · 2010
This paper presents an approach to the verification of reactive multia-gent system (RMAS) applications. Many of those applications require high levels of confidence about their safety of execution. In those cases, model-checking appears as an adequate verification tool. However, the complexity of RMAS models generally forbids the direct application of model-checking, due to the combinatory explosion problem. Avoiding this kind of inconvenience is frequently possible by applying methods such as abstraction or composition. This work presents a compositional method adapted to the verification of RMAS models belonging to a wide class of applications. The method is adapted to the verificationas of safety proper-ties. In this paper, the approach is put to practice by considering a vehicle platoon application with linear configuration. The crucial safety property being verified is the absence of collisions between platoon vehicles. A formal specification model is written with the SAL (Symbolic Analysis Laboratory) transition system language and compositional verification is performed with the SAL toolbox, by applying SAL model checkers. 1