Show all publications

An Approach to Compositional Verification of Reactive Multiagent Systems

Download PDFDownload Bibliography in Open DocumentDownload Bibliography in HTMLDownload BibTeXDownload RISDownload Bibliographical Ontology (RDF)
Authors:
Details:
In Proc. of Working Notes of the Twenty-Fourth AAAI Conference on Artificial Intelligence (AAAI), Workshop on Model Checking and Artificial Intelligence, 2010.
Abstract:
This paper presents an approach to the verification of reactive multiagent 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 properties. 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.
Keywords:
-
Publication Category:
International conference with proceedings
Copyright 2010-2019 © Laboratoire Connaissance et Intelligence Artificielle Distribu√©es - Université Bourgogne Franche-Comté - Privacy policy