Recently, we have 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 counterintuitive interpretation of formulas when reasoning about the outcome of strategies. First, the semantics disregards finite paths, and thus 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.

翻译：近期，我们提出了一个用于验证异步多智能体系统中智能体能力的框架，并附带了一种模型自动约简算法。该语义基于分布式系统的建模传统构建。本文的研究表明，这种传统在推理策略结果时可能导致公式的悖论性解释。首先，该语义忽略了有限路径，因此对存在死锁的策略产生了非自然的评价。其次，语义表征无法捕捉主动智能体与其行为接收者之间的非对称性。我们提出通过适当扩展表征形式并改变异步MAS执行语义来规避这些问题。同时证明模型约简方案在改进后的框架中仍然有效。