Show all publications

Compositional Verification for Reactive Multi-Agent Systems Applied to Platoon Non Collision Verification

Download PDFDownload Bibliography in Open DocumentDownload Bibliography in HTMLDownload BibTeXDownload RISDownload Bibliographical Ontology (RDF)
In Studia Informatica Universalis, vol. 10(3), 2012.
This paper presents a methodology for the verification of reactive multi-agent systems (RMAS). High level of confidence about a safe operation is a mandatory in many reactive applications. Model-checking appear as an adequate tool for the verification of safety properties. However, model-checking can be confronted with the problem of intractable state space sizes. To avoid this kind of limitation, it is possible to apply verification methods based on abstraction or composition. This paper presents a compositional verification method adapted to a wide range of RMAS applications. This method is appropriate for the verification of safety property. The application considered in this paper is a platoon of vehicles with linear configuration. The safety property to be verified is the non collision between platoon vehicles. The SAL tool-kit has been adopted as a verification tool, by applying SAL model checkers. The verification method bases on a compositional verification rule.
Multi-agent systems Model-checking Compositional verification Platoon application
Publication Category:
International journal with reading committee
Copyright 2010-2019 © Laboratoire Connaissance et Intelligence Artificielle Distribu√©es - Université Bourgogne Franche-Comté - Privacy policy