An extension of ATL with strategy interaction

Abstract

We propose an extension to ATL (alternating-time temporal logic), called BSIL (basic strategy-interaction logic), for specifying collaboration among agents in a multiagent system. We show that BSIL is strictly more expressive than ATL + but incomparable with ATL∗, GL (game logic), and AMC (alternating μ-calculus) in expressiveness. We show that a memoryful strategy is necessary for fulfilling a specification in BSIL. We establish that the BSIL model-checking problem is PSPACE-complete. However, BSIL model checking can be performed in time quadratic in the model for fixed formulas. The BSIL (and hence ATL +) satisfiability is 2EXPTIME-complete. Finally, we report our experiment with a model checker for BSIL.