Optimizing Epistemic Model Checking Using Conditional Independence (Extended Abstract)

TL;DR

This paper introduces a method to optimize epistemic model checking by applying conditional independence reasoning, significantly improving performance as demonstrated in the MCK model checker with experimental results.

Contribution

It presents a novel application of conditional independence reasoning to enhance the efficiency of epistemic model checking, implemented in MCK.

Findings

Performance improvements of up to several orders of magnitude

Effective optimization for multi-agent knowledge verification

Validated approach through experimental results

Abstract

This paper shows that conditional independence reasoning can be applied to optimize epistemic model checking, in which one verifies that a model for a number of agents operating with imperfect information satisfies a formula expressed in a modal multi-agent logic of knowledge. The optimization has been implemented in the epistemic model checker MCK. The paper reports experimental results demonstrating that it can yield multiple orders of magnitude performance improvements.