A logic with revocable and refinable strategies

In this article, we present Updatable Strategy Logic (USL), a multi-agent temporal logic which subsumes the main propositions in this area, such as ATL, ATL*, ATLscATLsc and SL. These logics allow to express the capabilities of agents to ensure the satisfaction of temporal properties. USL mainly differs from SL, in two ways. Semantically, USL relies on multi-strategies (that is, non-deterministic strategies), and the notion of strategy composition is extended to enable an agent to refine her strategy, that is to update it without revoking it. Syntactically, the logic features a binding operator enabling multi-strategy refinements as well as an “unbinding” operator that allows an agent to explicitly revoke a multi-strategy (whereas revocation is implicit with the binding operator in SL). We show that USL allows to express a notion of sustainable control for an agent, i.e., a capability to always decide the satisfaction of a property, that still holds even after the said capability has been employed. Furthermore, USL allows the definition of a notion of equality between multi-strategies that enables to consider quantification over deterministic strategies. This makes USL strictly more expressive than SL. Finally, we also show that the model-checking problem for USL is decidable but non-elementary (as for SL).