Towards model checking interpreted systems

We show how it is possible to pair the NuSMV model checker with Akka, a software platform used to check validity of propositional modal formulas, to verify properties of multi-agent systems formalised on interpreted systems semantics. We demonstrate this by analysing three variants of the bit-transmission problem.

• Type: Conference
• Year: 2003
• Where: ATAL
• Authors: Alessio Lomuscio, Franco Raimondi, Marek J. Sergot
• Keywords: ATAL 2003, Interpreted Systems Semantics, NuSMV Model Checker, Propositional Modal Formulas