Loading...
Please wait, while we are loading the content...
Similar Documents
Generic Expression in B of the Influence/Reaction Model: Specifying and Verifying Situated Multi-Agent Systems
| Content Provider | Semantic Scholar |
|---|---|
| Author | Simonin, Olivier Lanoix, Arnaud Colin, Samuel Scheuer, Alexis Charpillet, François |
| Copyright Year | 2007 |
| 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. |
| Starting Page | 18 |
| Ending Page | 18 |
| Page Count | 1 |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://hal.inria.fr/docs/00/17/49/70/PDF/SimoninEtalRR07.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |