Access Restriction

Author Raimondi, Franco ♦ Lomuscio, Alessio
Source CiteSeerX
Content type Text
File Format PDF
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Dining Cryptographer ♦ Interpreted System ♦ Multi-agent System ♦ Mechanical Verification ♦ Epistemic Property ♦ Smv Program ♦ Multi-agent System Specification ♦ Kripke Model Editor ♦ Smv Model Checker
Description We present a compiler that translates a multi-agent systems specification given in the formalism of Interpreted Systems into an SMV program. We show how an SMV model checker can be coupled with a Kripke model editor (Akka) to allow for the mechanical verification of epistemic properties of multi-agent systems. We apply this methodology to the verification of a communication protocol — the dining cryptographers. 1
Educational Role Student ♦ Teacher
Age Range above 22 year
Educational Use Research
Education Level UG and PG ♦ Career/Technical Study
Learning Resource Type Article
Journal Electronic Notes In Theoretical Computer Science