Towards Assume-Guarantee Verification of Strategic Ability
arXiv:2310.15727 · doi:10.5555/3535850.3536082
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.