A Solver for Modal Fixpoint Logics

AbstractWe present MLSolver, a tool for solving the satisfiability and validity problems for modal fixpoint logics. The underlying technique is based on characterisations of satisfiability through infinite (cyclic) tableaux in which branches have an inner thread structure mirroring the regeneration of least and greatest fixpoint constructs in the infinite. Well-foundedness for unfoldings of least fixpoints is checked using deterministic parity automata. This reduces the satisfiability and validity problems to the problem of solving a parity game. MLSolver then uses a parity game solver in order to decide satisfiability and derives example models from the winning strategies in the parity game. Currently supported logics are the modal and linear-time μ-calculi, CTL*, and PDL (and therefore also CTL and LTL). MLSolver is designed to allow easy extensions in the form of further modal fixpoint logics