Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
4663317 | Journal of Applied Logic | 2007 | 17 Pages |
Abstract
We present a methodology for the verification of multi-agent systems, whose properties are specified by means of a modal logic that includes a temporal, an epistemic, and a modal operator to reason about correct behaviour of agents. The verification technique relies on model checking via ordered binary decision diagrams. We present an implementation and report on experimental results for two scenarios: the bit transmission problem with faults and the protocol of the dining cryptographers.
Related Topics
Physical Sciences and Engineering
Mathematics
Logic
Authors
Franco Raimondi, Alessio Lomuscio,