Faster model checking for the modal mu-calculus

Abstract

In this paper, we develop an algorithm for model checking that handles the full modal mu-calculus including alternating fixpoints. Our algorithm has a better worst-case complexity than the best known algorithm for this logic while performing just as well on certain sublogics as other specialised algorithms. Important for the efficiency is an alternative characterisation of formulas in terms of equational systems, which enables the sharing and reuse of intermediate results.