Efficient model checking of causal-knowledge protocols

Abstract

A model checking algorithm for proving correctness of causal knowledge protocols for multi-agent systems is given. Protocols are specified in an extension of the temporal logic of causal knowledge [18]. The temporal language is interpreted over labelled prime event structures. The epistemic operators correspond to knowledge and goals, whereas the temporal modalities correspond to the immediate causality and causality. The model checking algorithm is translated to the model checking problem for LTL or ACTL. This enables a further translation to the SAT-problem, using the technique of the bounded model checking.