Partial-order reduction for parity games with an application on parameterised Boolean Equation Systems (Technical Report)

Research output: Book/ReportReportAcademic

Abstract

Partial-order reduction (POR) is a well-established technique to combat the problem of state-space explosion. Most approaches in literature focus on Kripke structures or labelled transition systems and preserve a form of stutter/weak trace equivalence or weak bisimulation. Therefore, they are at best applicable when checking weak modal mucalculus. We propose to apply POR on parity games, which can encode the combination of a transition system and a temporal property. Our technique allows one to apply POR in the setting of mu-calculus model checking. We show with an example that the reduction achieved on parity games can be significantly larger. Furthermore, we identify and repair an issue where stubborn sets do not preserve stutter equivalence.
LanguageEnglish
Place of PublicationEindhoven
PublisherTechnische Universiteit Eindhoven
Number of pages28
StatePublished - 1 Sep 2019

Publication series

NameComputer science reports
Volume19/02
ISSN (Print)0926-4515

Fingerprint

Model checking
Explosions
Repair

Cite this

@book{986a8de03a1c44be840cbc3866d4ec13,
title = "Partial-order reduction for parity games with an application on parameterised Boolean Equation Systems (Technical Report)",
abstract = "Partial-order reduction (POR) is a well-established technique to combat the problem of state-space explosion. Most approaches in literature focus on Kripke structures or labelled transition systems and preserve a form of stutter/weak trace equivalence or weak bisimulation. Therefore, they are at best applicable when checking weak modal mucalculus. We propose to apply POR on parity games, which can encode the combination of a transition system and a temporal property. Our technique allows one to apply POR in the setting of mu-calculus model checking. We show with an example that the reduction achieved on parity games can be significantly larger. Furthermore, we identify and repair an issue where stubborn sets do not preserve stutter equivalence.",
author = "Thomas Neele and Tim Willemse and Wieger Wesselink",
year = "2019",
month = "9",
day = "1",
language = "English",
series = "Computer science reports",
publisher = "Technische Universiteit Eindhoven",

}

Partial-order reduction for parity games with an application on parameterised Boolean Equation Systems (Technical Report). / Neele, Thomas; Willemse, Tim; Wesselink, Wieger.

Eindhoven : Technische Universiteit Eindhoven, 2019. 28 p. (Computer science reports; Vol. 19/02).

Research output: Book/ReportReportAcademic

TY - BOOK

T1 - Partial-order reduction for parity games with an application on parameterised Boolean Equation Systems (Technical Report)

AU - Neele,Thomas

AU - Willemse,Tim

AU - Wesselink,Wieger

PY - 2019/9/1

Y1 - 2019/9/1

N2 - Partial-order reduction (POR) is a well-established technique to combat the problem of state-space explosion. Most approaches in literature focus on Kripke structures or labelled transition systems and preserve a form of stutter/weak trace equivalence or weak bisimulation. Therefore, they are at best applicable when checking weak modal mucalculus. We propose to apply POR on parity games, which can encode the combination of a transition system and a temporal property. Our technique allows one to apply POR in the setting of mu-calculus model checking. We show with an example that the reduction achieved on parity games can be significantly larger. Furthermore, we identify and repair an issue where stubborn sets do not preserve stutter equivalence.

AB - Partial-order reduction (POR) is a well-established technique to combat the problem of state-space explosion. Most approaches in literature focus on Kripke structures or labelled transition systems and preserve a form of stutter/weak trace equivalence or weak bisimulation. Therefore, they are at best applicable when checking weak modal mucalculus. We propose to apply POR on parity games, which can encode the combination of a transition system and a temporal property. Our technique allows one to apply POR in the setting of mu-calculus model checking. We show with an example that the reduction achieved on parity games can be significantly larger. Furthermore, we identify and repair an issue where stubborn sets do not preserve stutter equivalence.

M3 - Report

T3 - Computer science reports

BT - Partial-order reduction for parity games with an application on parameterised Boolean Equation Systems (Technical Report)

PB - Technische Universiteit Eindhoven

CY - Eindhoven

ER -