Generating and Solving Symbolic Parity Games

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

7 Citations (Scopus)
50 Downloads (Pure)

Abstract

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)
PublisherEPTCS
Pages2-14
Number of pages13
DOIs
Publication statusPublished - Apr 2014

Publication series

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

Keywords

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

Cite this

Kant, G., & van de Pol, J. C. (2014). Generating and Solving Symbolic Parity Games. In Proceedings 3rd Workshop on GRAPH Inspection and Traversal Engineering (GRAPHITE 2014) (pp. 2-14). (Electronic Proceedings in Theoretical Computer Science; Vol. 159). EPTCS. https://doi.org/10.4204/EPTCS.159.2
Kant, Gijs ; van de Pol, Jan Cornelis. / Generating and Solving Symbolic Parity Games. Proceedings 3rd Workshop on GRAPH Inspection and Traversal Engineering (GRAPHITE 2014). EPTCS, 2014. pp. 2-14 (Electronic Proceedings in Theoretical Computer Science).
@inproceedings{728ff805ee8a46748277ce08ba35b143,
title = "Generating and Solving Symbolic Parity Games",
abstract = "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.",
keywords = "EWI-24949, FMT-MC: MODEL CHECKING, Multi-valued Decision Diagrams, Verification, METIS-305967, IR-91924, Modal mu-calculus, Model Checking, Parity Games",
author = "Gijs Kant and {van de Pol}, {Jan Cornelis}",
note = "10.4204/EPTCS.159.2",
year = "2014",
month = "4",
doi = "10.4204/EPTCS.159.2",
language = "Undefined",
series = "Electronic Proceedings in Theoretical Computer Science",
publisher = "EPTCS",
pages = "2--14",
booktitle = "Proceedings 3rd Workshop on GRAPH Inspection and Traversal Engineering (GRAPHITE 2014)",

}

Kant, G & van de Pol, JC 2014, Generating and Solving Symbolic Parity Games. in Proceedings 3rd Workshop on GRAPH Inspection and Traversal Engineering (GRAPHITE 2014). Electronic Proceedings in Theoretical Computer Science, vol. 159, EPTCS, pp. 2-14. https://doi.org/10.4204/EPTCS.159.2

Generating and Solving Symbolic Parity Games. / Kant, Gijs; van de Pol, Jan Cornelis.

Proceedings 3rd Workshop on GRAPH Inspection and Traversal Engineering (GRAPHITE 2014). EPTCS, 2014. p. 2-14 (Electronic Proceedings in Theoretical Computer Science; Vol. 159).

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

TY - GEN

T1 - Generating and Solving Symbolic Parity Games

AU - Kant, Gijs

AU - van de Pol, Jan Cornelis

N1 - 10.4204/EPTCS.159.2

PY - 2014/4

Y1 - 2014/4

N2 - 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.

AB - 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.

KW - EWI-24949

KW - FMT-MC: MODEL CHECKING

KW - Multi-valued Decision Diagrams

KW - Verification

KW - METIS-305967

KW - IR-91924

KW - Modal mu-calculus

KW - Model Checking

KW - Parity Games

U2 - 10.4204/EPTCS.159.2

DO - 10.4204/EPTCS.159.2

M3 - Conference contribution

T3 - Electronic Proceedings in Theoretical Computer Science

SP - 2

EP - 14

BT - Proceedings 3rd Workshop on GRAPH Inspection and Traversal Engineering (GRAPHITE 2014)

PB - EPTCS

ER -

Kant G, van de Pol JC. Generating and Solving Symbolic Parity Games. In Proceedings 3rd Workshop on GRAPH Inspection and Traversal Engineering (GRAPHITE 2014). EPTCS. 2014. p. 2-14. (Electronic Proceedings in Theoretical Computer Science). https://doi.org/10.4204/EPTCS.159.2