Combined model checking for temporal, probabilistic, and real-time logics
Combined model checking for temporal, probabilistic, and real-time logics
复制标题
DOI：
10.1016/j.tcs.2013.07.012
复制
发表时间：
2013-09-09
影响因子：
1.1
通讯作者：
Schewe, Sven
中科院分区：
文献类型：
--
作者：
Konur, Savas;Fisher, Michael;Schewe, Sven
模型检测是一种成熟的并发和分布式系统的形式化验证技术。近年来，模型检测已经扩展并适用于多智能体系统，主要是为了使信仰-愿望-意图系统的形式化分析。虽然这是成功的，有必要更复杂的逻辑框架，以验证现实的多代理系统。特别是概率和实时方面，以及知识、信念、目标等，然而，为复杂的逻辑组合开发新的模型检测工具既困难又耗时。在这篇文章中，我们将展示如何组成的时间，概率和实时逻辑的模型检查器可以重用模块化的方式，当我们考虑组合逻辑涉及不同的维度。这避免了模型检查过程的重新实现。我们定义了一个模块化的方法，证明其正确性，建立其复杂性，并展示了它如何可以用来描述现有的组合方法和定义尚未实现的组合。我们还证明了我们的方法的可行性的案例研究。(c)2013作者Elsevier B. V.出版，保留所有权利。
Model checking is a well-established technique for the formal verification of concurrent and distributed systems. In recent years, model checking has been extended and adapted for multi-agent systems, primarily to enable the formal analysis of belief-desire-intention systems. While this has been successful, there is a need for more complex logical frameworks in order to verify realistic multi-agent systems. In particular, probabilistic and real-time aspects, as well as knowledge, belief, goals, etc., are required.However, the development of new model checking tools for complex combinations of logics is both difficult and time consuming. In this article, we show how model checkers for the constituent temporal, probabilistic, and real-time logics can be re-used in a modular way when we consider combined logics involving different dimensions. This avoids the re-implementation of model checking procedures. We define a modular approach, prove its correctness, establish its complexity, and show how it can be used to describe existing combined approaches and define yet-unimplemented combinations. We also demonstrate the feasibility of our approach on a case study. (c) 2013 The Authors. Published by Elsevier B.V. All rights reserved.