An axiomatization of bisimulation quantifiers via the μ-calculus

This paper deals with bisimulation quantifiers logic BQL, that is, the extension of propositional dynamic logic PDL with the so-called “bisimulation quantifiers”. This logic is expressively equivalent to the μ-calculus (an extension of modal logic with extremal fixpoints), albeit its formulas are easier to understand. In this work we provide a complete axiomatization of BQL, based on certain normal form results for the μ-calculus obtained by Janin and Walukiewicz.