Automatic verification of deontic interpreted systems by model checking via OBDD's
Franco Raimondi, Alessio R. Lomuscio · UCL Discovery (University College London) · 2004
We present an algorithm for the verification of multiagent systems specified by means of a modal logic that includes a temporal, an epistemic, and a deontic operator. Verification is performed by model checking on OBDD's. We present an implementation of the algorithm and report on experimental results for the bit transmission problem with faults.