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

    Onderzoeksoutput: Boek/rapportRapportAcademic

    45 Downloads (Pure)

    Samenvatting

    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.
    Originele taal-2Engels
    Plaats van productieEindhoven
    UitgeverijTechnische Universiteit Eindhoven
    Aantal pagina's28
    StatusGepubliceerd - 1 sep. 2019

    Publicatie series

    NaamComputer science reports
    Volume19/02
    ISSN van geprinte versie0926-4515

    Vingerafdruk

    Duik in de onderzoeksthema's van 'Partial-order reduction for parity games with an application on parameterised Boolean Equation Systems (Technical Report)'. Samen vormen ze een unieke vingerafdruk.

    Citeer dit