Strategic Abilities of Asynchronous Agents: Semantic Paradoxes and How to Tame Them

Recently, we proposed a framework for verification of agents' abilities in asynchronous multi-agent systems, together with an algorithm for automated reduction of models. The semantics was built on the modeling tradition of distributed systems. As we show here, this can sometimes lead to paradoxical interpretation of formulas when reasoning about the outcome of strategies. First, the semantics disregards finite paths, and thus yields counterintuitive evaluation of strategies with deadlocks. Secondly, the semantic representations do not allow to capture the asymmetry between active agents and the recipients of their choices. We propose how to avoid the problems by a suitable change of the semantics, and prove that the model reduction scheme still works in the modified framework.