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 <>
Submitted on : Wednesday, September 26, 2007 - 9:29:11 AM
Last modification on : Thursday, March 4, 2021 - 3:12:16 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

432

Files downloads

320