A Solver for Modal Fixpoint Logics | Zendy

Oliver Friedmann | Zendy; Martin Lange | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

A Solver for Modal Fixpoint Logics

Author(s) -

Oliver Friedmann,

Martin Lange

Publication year - 2010

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2010.04.008

Subject(s) - modal μ calculus , satisfiability , fixed point , modal , solver , mathematics , discrete mathematics , boolean satisfiability problem , automaton , computer science , parity (physics) , theoretical computer science , algorithm , mathematical optimization , normal modal logic , description logic , multimodal logic , mathematical analysis , chemistry , physics , particle physics , polymer chemistry

We 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

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research