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