A tableau for bundled strategies

Abstract

There is a bundled variant, BCTL*, of the branching time logic CTL* which allows reasoning about models with fairness constraints on the possible futures. However, the stronger branching logic ATL*, which is well suited to reasoning about multi-agent systems, has no bundled variant. Schedulers, humans and so on may also exhibit “fair” behaviour that only manifests in the limit, motivating a similar variant of ATL*. In this paper we (1) show how to define a non-trivial Bundled variant of ATL* (BATL*); (2) Present a 2EXPTIME tableau for BATL* (so showing BATL* is 2EXPTIME-complete); (3) prove the correctness of the tableau; and (4) provide an implementation that can decide simple formulas for BATL* and another “non-local” variant NL-BCTL* that is well suited to verifying rewrite rules for ATL*.