Generating and Solving Symbolic Parity Games

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    12 Citations (Scopus)
    129 Downloads (Pure)


    We present a new tool for verification of modal mu-calculus formulae for process specifications, based on symbolic parity games. It enhances an existing method, that first encodes the problem to a Parameterised Boolean Equation System (PBES) and then instantiates the PBES to a parity game. We improved the translation from specification to PBES to preserve the structure of the specification in the PBES, we extended LTSmin to instantiate PBESs to symbolic parity games, and implemented the recursive parity game solving algorithm by Zielonka for symbolic parity games. We use Multi-valued Decision Diagrams (MDDs) to represent sets and relations, thus enabling the tools to deal with very large systems. The transition relation is partitioned based on the structure of the specification, which allows for efficient manipulation of the MDDs. We performed two case studies on modular specifications, that demonstrate that the new method has better time and memory performance than existing PBES based tools and can be faster (but slightly less memory efficient) than the symbolic model checker NuSMV.
    Original languageUndefined
    Title of host publicationProceedings 3rd Workshop on GRAPH Inspection and Traversal Engineering (GRAPHITE 2014)
    Number of pages13
    Publication statusPublished - Apr 2014
    Event3rd Workshop on GRAPH Inspection and Traversal Engineering, GRAPHITE 2014 - Grenoble, France
    Duration: 5 Apr 20145 Apr 2014

    Publication series

    NameElectronic Proceedings in Theoretical Computer Science
    ISSN (Print)2075-2180
    ISSN (Electronic)2075-2180


    Workshop3rd Workshop on GRAPH Inspection and Traversal Engineering, GRAPHITE 2014
    Other5 April 2014


    • EWI-24949
    • Multi-valued Decision Diagrams
    • Verification
    • METIS-305967
    • IR-91924
    • Modal mu-calculus
    • Model Checking
    • Parity Games

    Cite this