Combined model checking for temporal, probabilistic, and real-time logics


Konur, Savas, Fisher, Michael and Schewe, Sven ORCID: 0000-0002-9093-9518 (2013) Combined model checking for temporal, probabilistic, and real-time logics. THEORETICAL COMPUTER SCIENCE, 503. pp. 61-88.

This is the latest version of this item.

[img] Text
1-s2.0-S030439751300515X-main.pdf__tid=501d3e2e-82f4-11e4-8ceb-00000aab0f27&acdnat=1418494835_0746cded9fcd8f161715e152469a1cda - Published version
Available under License Creative Commons Attribution.
Download (663kB)

Abstract

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. © 2013 The Authors.

Item Type: Article
Additional Information: Also: http://www.sciencedirect.com/science/article/pii/S030439751300515X ## TULIP Type: Articles/Papers (Journal) ##
Uncontrolled Keywords: Formal verification, Model checking, Combination of logics, Complexity, Multi-agent systems
Depositing User: Symplectic Admin
Date Deposited: 15 Dec 2014 10:04
Last Modified: 16 Dec 2022 03:00
DOI: 10.1016/j.tcs.2013.07.012
Related URLs:
URI: https://livrepository.liverpool.ac.uk/id/eprint/2003663

Available Versions of this Item

  • Combined model checking for temporal, probabilistic, and real-time logics. (deposited 15 Dec 2014 10:04) [Currently Displayed]
Dimensions
Altmetric
CORE (COnnecting REpositories)