Multi-Agent Systems (MAS) are notoriously complex and hard to verify. In fact, it is not trivial to model a MAS, and even when a model is built, it is not always possible to verify, in a formal way, that it is actually behaving as we expect. Usually, it is relevant to know whether an agent is capable of fulfilling its own goals. One possible way to check this is through Model Checking. Specifically, by verifying Alternating-time Temporal Logic (ATL) properties, where the notion of strategies for achieving goals can be described. Unfortunately, the resulting model checking problem is not decidable in general. In this paper, we present a verification procedure based on combining Model Checking and Runtime Verification, where sub-models of the MAS model belonging to decidable fragments are verified by a model checker, and runtime monitors are used to verify the rest. Furthermore, we implement our technique and show experimental results.
翻译:多机构系统(MAS)非常复杂,难以核实。事实上,建模一个MAS并非无关紧要,即使模型已经建成,也并不总是能够正式核实它实际上是否如我们所期望的那样行事。通常,需要了解一个代理机构是否有能力实现自己的目标。一个可能的检查方法就是通过模型检查。具体地说,通过核查不同时间的时空逻辑(ATL)属性,可以描述实现目标的战略概念。不幸的是,由此形成的模型检查问题一般无法分辨。在本文件中,我们提出了一个核查程序,其基础是将模式检查和运行时间核查结合起来,由模型检查者核查属于可破碎碎片的MAS模型的子模型,并使用运行时间监测器来核查其余碎片。此外,我们实施了我们的技术并展示实验结果。