Model Checking Multi-agent systems with Logic Based Petri Nets


Tristan M. Behrens, Jurgen Dix

We introduce a class of Petri nets, simple logic Petri nets (SLPN), that are based on logical expressions. We show how this type of nets can be efficiently mapped into logic programs with negation: the corresponding answer sets describe interleaved executions of the underlying nets (Theorem 1). The absence of an answer set indicates a deadlock situation. We also show how to correctly model and specify AgentSpeak agents and multi-agent systems with SLPN’s (Theorem 2). Both theorems allow us to solve the task of model checking AgentSpeak multi-agent systems by computing answer sets of the obtained logic program with any ASP system.

(keywords) Verification - Model checking - Petri nets - Agent oriented programming - Concurrency

Annals of Mathemathics and Artificial Intelligence 51(2-4), pages 81-121,  2007, Springer.
From the issue entitled "Special Issue in honor of Professor Jack Minker's 80th birthday”

@article{masmodelchecking-amai51,
Author = {Behrens, Tristan M. and Dix, Jurgen},
Doi = {10.1007/s10472-008-9092-7},
Issn = {1012-2443},
Journal = {Annals of Mathemathics and Artificial Intelligence},
Note = {From the issue entitled ``Special Issue in honor of Professor Jack Minker's 80th birthday''},
Number = {2-4},
Pages = {81--121},
Publisher = {Springer},
Title = {Model Checking Multi-agent systems with Logic Based {P}etri Nets},
Url = {http://www.springerlink.com/content/3q71261838q73u26/},
Volume = 51,
Year = 2007}
Tags:

Publication

— authors

Tristan M. Behrens, Jurgen Dix

— status

published

— sort

article in journal

Venue

— journal

Annals of Mathemathics and Artificial Intelligence

— volume

51

— issue

2-4

— pages

81-121

— publication date

2007

URLs

original page  |  original PDF

Identifiers

— DOI

10.1007/s10472-008-9092-7

— print ISSN

1012-2443

BibTeX

— BibTeX ID
masmodelchecking-amai51
— BibTeX category
article

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