Towards Assume-Guarantee Verification of Strategic Ability

Łukasz Mikulski (Nicolaus Copernicus University & Institute of Computer Science, Polish Academy of Sciences), Wojciech Jamroga (Institute of Computer Science, Polish Academy of Sciences & University of Luxembourg), Damian Kurpiewski (Institute of Computer Science Polish Academy of Sciences & Nicolaus Copernicus University)

Abstract

Formal verification of strategic abilities is a hard problem. We propose to use the methodology of assume-guarantee reasoning in order to facilitate model checking of alternating-time temporal logic with imperfect information and imperfect recall.