How Variables Graphs May Help to Correct Erroneous MAS Specifications - GREYC mad Access content directly
Conference Papers Year : 2023

How Variables Graphs May Help to Correct Erroneous MAS Specifications

Abstract

This paper is situated in the context of multi-agent systems validation using theorem proving techniques. This document presents a preliminary case study, which is a part of a broader investigation aiming to explore whether such techniques could aid developers in detecting and characterizing errors in MAS specifications. Indeed, regardless of the verification system used (model checking or theorem proving), understanding the reason of a failure in order to correct the specification is most of the time rather difficult. In this article, we propose a method that may help in this task. This method relies on the variables (and their dependencies) that appear in proof obligations generated by GDT4MAS, a specification and verification method dedicated to Multi-Agent Systems. Graphs generated thanks to dependencies between variables occurring in an unproved theorem may indeed help to identify certain types of mistakes, giving a way to correct the specification.
Fichier principal
Vignette du fichier
articleIntelliSys2023.pdf (489.09 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
licence : CC BY NC SA - Attribution - NonCommercial - ShareAlike

Dates and versions

hal-04199918 , version 1 (08-09-2023)

Licence

Attribution - NonCommercial - ShareAlike

Identifiers

  • HAL Id : hal-04199918 , version 1

Cite

Bruno Mermet, Gaële Simon. How Variables Graphs May Help to Correct Erroneous MAS Specifications. Intelligent Systems (Intellisys), Sep 2023, Amsterdam, France. ⟨hal-04199918⟩
20 View
5 Download

Share

Gmail Facebook X LinkedIn More