Using Proof Failures to Help Debugging MAS

For several years, we have worked on the usage of theorem proving techniques to validate Multi-Agent Systems. In this article, we present a preliminary case study, that is part of larger work whose long-term goal is to determine how proof tools can be used to help to develop error-free Multi-Agent Systems. This article describes how an error caused by a synchronisation problem between several agents can be identified by a proof failure. We also show that analysing proof failures can help to find bugs that may occur only in a very particular context, which makes it difficult to analyse by standard debugging techniques.