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的表述和改变执行语义来避免问题。我们还证明,示范削减计划仍然在修改后的框架中发挥作用。