Partial Order Reductions for Model Checking Temporal-epistemic Logics over Interleaved Multi-agent Systems

Issue title: Concurrency Specification and Programming (CS&P)

Article type: Research Article

Authors: Lomuscio, Alessio | Penczek, Wojciech | Qu, Hongyang

Affiliations: Department of Computing, Imperial College London, UK. A.Lomuscio@imperial.ac.uk | Institute of Computer Science, PAS and University of Podlasie, Poland. wpenczek@gmail.com | Oxford University Computing Laboratory, UK. Hongyang.Qu@comlab.ox.ac.uk

Note: [] Address for correspondence: Department of Computing, Imperial College London, 180 Queen’s Gate London SW7 2AZ, UK

Abstract: We investigate partial order reduction techniques for the verification of multi-agent systems. We investigate the case of 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.

DOI: 10.3233/FI-2010-276

Journal: Fundamenta Informaticae, vol. 101, no. 1-2, pp. 71-90, 2010