Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
9655945 | Electronic Notes in Theoretical Computer Science | 2005 | 22 Pages |
Abstract
We propose a framework for the verification of multi-agent systems' specification by symbolic model checking. The language CTLKD (an extension of CTL) allows for the representation of the temporal evolution of epistemic states of the agents, as well as their correct and incorrect functioning behaviour. We ground our analysis on the semantics of deontic interpreted systems. The verification approach is based on an adaption of the technique of bounded model checking, a mainstream approach in verification of reactive systems. We test our results on a typical communication scenario: the bit transmission problem with faults.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Bożena Woźna, Alessio Lomuscio, Wojciech Penczek,