论文标题
在多代理系统上结合模型检查和运行时验证
Towards the Combination of Model Checking and Runtime Verification on Multi-Agent Systems
论文作者
论文摘要
众所周知，多机构系统（MAS）很复杂且难以验证。实际上，建模MAS并不是很微不足道的，即使建立模型，也不总是有可能以正式的方式验证它实际上是按照我们的期望。通常，知道代理是否能够实现自己的目标是很重要的。检查此问题的一种可能方法是通过模型检查。具体而言，通过验证交替的时间逻辑（ATL）属性，可以描述实现目标策略的概念。不幸的是，总体而言，由此产生的模型检查问题是无法决定的。在本文中，我们提出了一个基于组合模型检查和运行时验证的验证过程，其中属于可决定片段的MAS模型的子模型由模型检查器验证，并且使用运行时监测器来验证其余的。此外，我们实施我们的技术并显示实验结果。
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.
