Oxford logo
[LPQ10] A. Lomuscio, W. Penczek and H. Qu. Partial order reductions for model checking temporal epistemic logics over interleaved multi-agent systems. In Proc. the 9th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS'10), pages 659-666, IFAAMAS. May 2010. [pdf] [bib]
Downloads:  pdf pdf (203 KB)  bib bib
Abstract. We investigate partial order reduction for model checking multi-agent systems by focusing on interleaved interpreted systems. These are a particular class of interpreted systems, a mainstream MAS formalism, in which only one action at the time is performed in the system. We present a notion of stuttering-equivalence, and prove the semantical equivalence of stuttering-equivalent traces with respect to linear and branching time temporal logics for knowledge without the next operator. We give algorithms to reduce the size of the models before the model checking step and show preservation properties. We evaluate the technique by discussing implementations and the experimental results obtained against well-known examples in the MAS literature.