Verifying Multi-agent Systems via Unbounded Model Checking


M. Kacprzak, A. Lomuscio, T. Lasica, W. Penczek, M. Szreter

We present an approach to the problem of verification of epistemic properties in multi-agent systems by means of symbolic model checking. In particular, it is shown how to extend the technique of unbounded model checking from a purely temporal setting to a temporal-epistemic one. In order to achieve this, we base our discussion on interpreted systems semantics, a popular semantics used in multi-agent systems literature. We give details of the technique and show how it can be applied to the well known train, gate and controller problem.

(keywords) Model checking - unbounded model checking - multi-agent systems

Formal Approaches to Agent-Based Systems Third International Workshop, FAABS 2004, Greenbelt, MD, April 26-27, 2004, Revised Selected Papers, Lecture Notes in Computer Science 3228,  2005, Springer.

@article{unboundedVerification05,
Author = {Kacprzak, M. and Lomuscio, A. and Lasica, T. and Penczek, W. and Szreter, M.},
Journal = {Lecture Notes in Computer Science},
Title = {Verifying Multi-agent Systems via Unbounded Model Checking},
Volume = {3228},
Year = {2005},
Publisher = {Springer},
DOI = {10.1007/978-3-540-30960-4_13}
}
Tags:

Publication

— authors

M. Kacprzak, A. Lomuscio, T. Lasica, W. Penczek, M. Szreter

— status

published

— sort

paper in proceedings

Venue

— volume

Formal Approaches to Agent-Based Systems Third International Workshop, FAABS 2004, Greenbelt, MD, April 26-27, 2004, Revised Selected Papers

— series

Lecture Notes in Computer Science

— volume

3228

— publication date

2005

URLs

original page  |  original PDF

Identifiers

— DOI

10.1007/978-3-540-30960-4_13

BibTeX

— BibTeX ID
unboundedVerification05
— BibTeX category
article

Partita IVA: 01131710376 - Copyright © 2008-2021 APICe@DISI Research Group - PRIVACY