Vérification formelle de propriétés de vivacité pour des systèmes multi-agents probabilistes à l’aide d’arbre à décomposition de buts
Revue Ouverte d'Intelligence Artificielle, Post-actes des Journées Francophones sur les Systèmes Multi-Agents (JFSMA 2023), Volume 5 (2024) no. 4, pp. 117-144.

Cet article traite de la preuve formelle de systèmes multi-agents dont les comportements peuvent être caractérisés de manière probabiliste. Nous nous fondons sur le modèle GDT4MAS qui aborde la vérification formelle de la spécification jusqu’à la génération d’obligations de preuve en s’appuyant sur la logique du premier ordre, ce qui lui confère une expressivité importante. Le modèle GDT4MAS ne traite cependant pas des comportements stochastiques et ne permet pas de prouver des propriétés de vivacité. Nous étendons le modèle GDT4MAS en permettant de modéliser des agents pouvant réaliser des actions aux effets stochastiques et redéfinissons les opérateurs dans ce cadre. Afin de prouver des propriétés de vivacité, nous nous appuyons sur des méthodes de variant adaptées à notre cadre et montrons comment prouver par exemple la terminaison presque sûre d’un SMA ou la récurrence d’une propriété particulière.

This article deals with the formal proof of multi-agent systems whose behaviors can be characterized probabilistically. We consider the GDT4MAS model which addresses formal verification from specification to proof obligation generation by relying on first-order logic, which gives it an important expressiveness. However, the GDT4MAS model does not deal with stochastic behavior and does not allow the proof of liveness properties. We then extend GDT4MAS to model agents that can perform actions with stochastic effects and redefine the operators in this framework. To prove liveness properties, we rely on variant methods adapted to our framework and show how to prove the MAS almost sure termination, or the recurrence of a property.

Publié le :
DOI : 10.5802/roia.89
Mots-clés : Vérification formelle, systèmes multi-agents, comportements stochastiques
Keywords: Formal verification, multi-agent systems, stochastic behaviours

Mathias Déhais 1 ; Bruno Mermet 2 ; Grégory Bonnet 1

1 Normandie Univ, UNICAEN, ENSICAEN, CNRS, GREYC
2 Normandie Univ, UNIHAVRE, ENSICAEN, CNRS, GREYC
Licence : CC-BY 4.0
Droits d'auteur : Les auteurs conservent leurs droits
@article{ROIA_2024__5_4_117_0,
     author = {Mathias D\'ehais and Bruno Mermet and Gr\'egory Bonnet},
     title = {V\'erification formelle de propri\'et\'es de vivacit\'e pour des syst\`emes multi-agents probabilistes \`a l{\textquoteright}aide d{\textquoteright}arbre \`a d\'ecomposition de buts},
     journal = {Revue Ouverte d'Intelligence Artificielle},
     pages = {117--144},
     publisher = {Association pour la diffusion de la recherche francophone en intelligence artificielle},
     volume = {5},
     number = {4},
     year = {2024},
     doi = {10.5802/roia.89},
     language = {fr},
     url = {https://roia.centre-mersenne.org/articles/10.5802/roia.89/}
}
TY  - JOUR
AU  - Mathias Déhais
AU  - Bruno Mermet
AU  - Grégory Bonnet
TI  - Vérification formelle de propriétés de vivacité pour des systèmes multi-agents probabilistes à l’aide d’arbre à décomposition de buts
JO  - Revue Ouverte d'Intelligence Artificielle
PY  - 2024
SP  - 117
EP  - 144
VL  - 5
IS  - 4
PB  - Association pour la diffusion de la recherche francophone en intelligence artificielle
UR  - https://roia.centre-mersenne.org/articles/10.5802/roia.89/
DO  - 10.5802/roia.89
LA  - fr
ID  - ROIA_2024__5_4_117_0
ER  - 
%0 Journal Article
%A Mathias Déhais
%A Bruno Mermet
%A Grégory Bonnet
%T Vérification formelle de propriétés de vivacité pour des systèmes multi-agents probabilistes à l’aide d’arbre à décomposition de buts
%J Revue Ouverte d'Intelligence Artificielle
%D 2024
%P 117-144
%V 5
%N 4
%I Association pour la diffusion de la recherche francophone en intelligence artificielle
%U https://roia.centre-mersenne.org/articles/10.5802/roia.89/
%R 10.5802/roia.89
%G fr
%F ROIA_2024__5_4_117_0
Mathias Déhais; Bruno Mermet; Grégory Bonnet. Vérification formelle de propriétés de vivacité pour des systèmes multi-agents probabilistes à l’aide d’arbre à décomposition de buts. Revue Ouverte d'Intelligence Artificielle, Post-actes des Journées Francophones sur les Systèmes Multi-Agents (JFSMA 2023), Volume 5 (2024) no. 4, pp. 117-144. doi : 10.5802/roia.89. https://roia.centre-mersenne.org/articles/10.5802/roia.89/

[1] J.-R. Abrial; A. Hoare; P. Chapron The B-Book, Cambridge University Press, 1996 | DOI | MR | Zbl

[2] M. Aouadhi A fully probabilistic extension of Event-B (2016) (Technical report)

[3] M. Aouadhi Introduction de raisonnement probabiliste dans la méthode B événementiel, Ph. D. Thesis, Université de Nantes (2017)

[4] C. Baier; M. Kwiatkowska Automatic verification of liveness properties of randomized systems, Proceedings of the Sixteenth Annual ACM Symposium on Principles of Distributed Computing, Santa Barbara, California, USA, August 21-24, 1997 (James E. Burns; Hagit Attiya, eds.), ACM, 1997 | DOI

[5] Christel Baier; Marta Kwiatkowska Model checking for a probabilistic branching time logic with fairness, Distributed Computing, Volume 11 (2004), pp. 125-155 | DOI | Zbl

[6] Marc Esteva; David de la Cruz; Carles Sierra ISLANDER : An electronic institutions editor, Proceedings of the First International Joint Conference on Autonomous Agents and Multiagent Systems : Part 3 (AAMAS ’02), ACM, 2002, pp. 1045-1052 | DOI

[7] Vojtěch Forejt; Marta Kwiatkowska; Gethin Norman; David Parker Automated Verification Techniques for Probabilistic Systems, Formal Methods for Eternal Networked Software Systems : 11th International School on Formal Methods for the Design of Computer, Communication and Software Systems, SFM 2011, Bertinoro, Italy, June 13-18, 2011. Advanced Lectures (Marco Bernardo; Valérie Issarny, eds.), Springer Berlin Heidelberg, Berlin, Heidelberg, 2011, pp. 53-113 | DOI

[8] Zeineb Graja; Frédéric Migeon; Christine Maurel; Marie-Pierre Gleizes; Ahmed Hadj Kacem Vers une modélisation formelle basée sur le raffinement des systèmes multi-agents auto-organisateurs, Principe de Parcimonie – JFSMA 14 – Vingt-deuxièmes Journées Francophones sur les Systèmes Multi-Agents, Loriol-sur-Drôme, France, Octobre 8-10, 2014 (Rémy Courdier; Jean-Paul Jamont, eds.), Cepadues Editions, 2014, pp. 139-148

[9] Zeineb Graja; Frédéric Migeon; Christine Maurel; Marie-Pierre Gleizes; Ahmed Hadj Kacem Vers une modélisation formelle basée sur le raffinement des systèmes multi-agents auto-organisateurs, RIA, Volume 30 (2016) no. 1-2, pp. 159-183 | DOI

[10] T. S. Hoang The development of a probabilistic B-method and a supporting toolkit, Ph. D. Thesis, University of New South Wales (2006)

[11] Thai Son Hoang; Jean-Raymond Abrial Reasoning about Liveness Properties in Event-B, Formal Methods and Software Engineering (Shengchao Qin; Zongyan Qiu, eds.), Springer Berlin Heidelberg, Berlin, Heidelberg, 2011, pp. 456-471 | DOI

[12] Simon Hudon; Thai Son Hoang; Jonathan S. Ostroff The Unit-B method : Refinement guided by progress concerns, SoSyM, Volume 15 (2016), pp. 1091-1116 | DOI

[13] John G. Kemeny; J. Laurie Snell; Anthony W. Knapp Denumerable Markov chains, Grad. Texts Math., 40, Springer, Cham, 1976 | DOI | MR | Zbl

[14] Marta Kwiatkowska; Gethin Norman; David Parker PRISM 4.0 : Verification of Probabilistic Real-Time Systems, Computer Aided Verification (Ganesh Gopalakrishnan; Shaz Qadeer, eds.), Springer Berlin Heidelberg, Berlin, Heidelberg, 2011, pp. 585-591 | DOI

[15] Marta Kwiatkowska; Gethin Norman; David Parker; Gabriel Santos Equilibria-Based Probabilistic Model Checking for Concurrent Stochastic Games, Formal methods – the next 30 years. Third world congress/23rd symposium, FM 2019, Porto, Portugal, October 7–11, 2019. Proceedings (Maurice H. ter Beek; Annabelle McIver; José N. Oliveira, eds.) (Lect. Notes Comput. Sci.), Volume 11800, Springer International Publishing, Cham, 2019, pp. 298-315 | DOI | MR | Zbl

[16] Marta Kwiatkowska; Gethin Norman; David Parker; Gabriel Santos Automatic verification of concurrent stochastic systems, Form. Methods Syst. Des., Volume 58 (2021) no. 1-2, pp. 188-250 | DOI | Zbl

[17] Alessio Lomuscio; Edoardo Pirovano Parameterised Verification of Strategic Properties in Probabilistic Multi-Agent Systems (AAMAS ’20), International Foundation for Autonomous Agents and Multiagent Systems, Richland, SC, 2020, pp. 762-770 | DOI

[18] Alessio Lomuscio; H. Qu; Franco Raimondi MCMAS : An opensource model checker for the verification of multi-agent systems, Int J Softw Tools Technol Transfer, Volume 19 (2017), pp. 9-30 | DOI

[19] Alessio Lomuscio; Franco Raimondi MCMAS : a model checker for multi-agent systems, Tools and algorithms for the construction and analysis of systems. 12th international conference, TACAS 2006, held as part of the joint European conferences on theory and practice of software, ETAPS 2006, Vienna, Austria, March 25 – April 2, 2006., Springer, Berlin, 2006, pp. 450-454 | DOI | Zbl

[20] Annabelle McIver; Carroll Morgan Abstraction, refinement and proof for probabilistic systems, Springer, New York, NY, 2005 | DOI | MR | Zbl

[21] Bruno Mermet; Gaële Simon GDT4MAS : an extension of the GDT model to specify and to verify MultiAgent systems, Proceedings of The 8th International Conference on Autonomous Agents and Multiagent Systems – Volume 1 (AAMAS ’09), International Foundation for Autonomous Agents and Multiagent Systems, Richland, SC, 2009, pp. 505-512 | DOI

[22] Bruno Mermet; Gaele Simon A New Proof System to Verify GDT Agents, Intelligent Distributed Computing VII (Filip Zavoral; Jason J. Jung; Costin Badica, eds.), Springer International Publishing, Cham, 2014, pp. 181-187 | DOI

[23] S. Owre; J. M. Rushby; N. Shankar PVS : A prototype verification system, Automated Deduction—CADE-11 (Deepak Kapur, ed.), Springer Berlin Heidelberg, Berlin, Heidelberg, 1992, pp. 748-752 | DOI

[24] E. Pirovano Parameterised model-checking of probabilistic multi-agent systems, Ph. D. Thesis, Imperial College London (2021)

[25] Ph. Schnoebelen The complexity of temporal logic model checking, Advances in modal logic. Vol. 4. Selected papers from the 4th conference (AiML 2002), Toulouse, France, October 2002, King’s College Publications, London, 2003, pp. 393-436 | MR | Zbl

[26] Kostas Stathis; Antonis C. Kakas; Wenjin Lu; Neophytos D emetriou; Ulle Endriss; Andrea Bracciali PROSOCS : a platform for programming software agents in computational logic, Proceedings of the Fourth International Symposium “From Agent Th eory to Agent Implementation” (AT2AI-4 – EMCSR’2004 Session M) (J. Müller; P. Petta, eds.), 2004, pp. 523-528

[27] Moshe Y. Vardi Automatic verification of probabilistic concurrent finite state programs, 26th Annual Symposium on Foundations of Computer Science (sfcs 1985), 1985, pp. 327-338 | DOI

[28] Moshe Y. Vardi Branching vs. linear time : Final showdown, Tools and algorithms for the construction and analysis of systems. 7th international conference, TACAS 2001, held as part of the joint European conferences on theory and practice of software, ETAPS 2001, Genova, Italy, April 2–6, 2001. Proceedings, Springer, Berlin, 2001, pp. 1-22 | Zbl

Cité par Sources :