HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Reports

Generic Expression in B of the Influence/Reaction Model: Specifying and Verifying Situated Multi-Agent Systems

Olivier Simonin 1 Arnaud Lanoix 2 Samuel Colin 2 Alexis Scheuer 1 François Charpillet 1
1 MAIA - Autonomous intelligent machine
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
2 DEDALE - Development of specifications
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : This paper addresses the formal specification and verification of situated multi-agent systems that can be formulated within the influence-reaction model as proposed in 1996 by Ferber & Muller. In this framework our objective is to prove the correctness of reactive multi-agent systems with respect to a certain formal specification or property, using formal methods. This is an important step to bring multi-agent systems to high quality standards as required for critical applications encountered in domains such as transport systems. A generic B writing of systems instantiating the influence reaction model is proposed, using patterns of specification. An illustration is then presented on the formal specification of a system operating electrical vehicles under precise automatic control at close spacings to form a platoon. The papers ends with considerations about further improvements of the framework, involving simulation and study of the properties of the system.
Complete list of metadata

Cited literature [22 references]  Display  Hide  Download

https://hal.inria.fr/inria-00173876
Contributor : Alexis Scheuer Connect in order to contact the contributor
Submitted on : Wednesday, September 26, 2007 - 9:29:11 AM
Last modification on : Wednesday, February 2, 2022 - 3:53:48 PM
Long-term archiving on: : Friday, November 25, 2016 - 5:34:18 PM

Files

SimoninEtalRR07.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00173876, version 2

Collections

Citation

Olivier Simonin, Arnaud Lanoix, Samuel Colin, Alexis Scheuer, François Charpillet. Generic Expression in B of the Influence/Reaction Model: Specifying and Verifying Situated Multi-Agent Systems. [Research Report] RR-6304, INRIA. 2007, pp.18. ⟨inria-00173876v2⟩

Share

Metrics

Record views

182

Files downloads

262