STV+AGR: Towards Practical Verification of Strategic Ability Using Assume-Guarantee Reasoning

Model checking of multi-agent systems (MAS) allows for formal (and, ideally, automated) verification of their relevant properties. Algorithms and tools for model checking of strategic abilities [1, 28, 9, 25] have been in development for over 20 years [2, 10, 6, 13, 7, 21, 8, 4, 3, 15, 20]. Unfortunately, the problem is hard, especially in the realistic case of agents with imperfect information [28, 5, 12]. In this paper, we propose a new extension of our experimental tool STV [19, 20] that facilitates compositional model checking of strategic properties in asynchronous MAS through assume-guarantee reasoning (AGR) [26, 11]. The extension is based on the preliminary results in [24], itself an adaptation of the AGR framework for liveness specifications from [22, 23].