A cure for stuttering parity games

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

9 Citations (Scopus)
1 Downloads (Pure)

Abstract

We define governed stuttering bisimulation for parity games, weakening stuttering bisimulation by taking the ownership of vertices into account only when this might lead to observably different games. We show that governed stuttering bisimilarity is an equivalence for parity games and allows for a natural quotienting operation. Moreover, we prove that all pairs of vertices related by governed stuttering bisimilarity are won by the same player in the parity game. Thus, our equivalence can be used as a preprocessing step when solving parity games. Governed stuttering bisimilarity can be decided in O(n2m)(n2m) time for parity games with n vertices and m edges. Our experiments indicate that governed stuttering bisimilarity is mostly competitive with stuttering equivalence on parity games encoding typical verification problems.
Original languageEnglish
Title of host publicationTheoretical Aspects of Computing – ICTAC 2012 (9th International Colloquium, Bangalore, India, September 24-27, 2012. Proceedings)
EditorsA. Roychoudhury, M. D'Souza
Place of PublicationBerlin
PublisherSpringer
Pages198-212
ISBN (Print)978-3-642-32942-5
DOIs
Publication statusPublished - 2012
Event9th International Colloquium on Theoretical Aspects of Computing (ICTAC 2012) - Bangalore, India
Duration: 24 Sept 201227 Sept 2012
Conference number: 9

Publication series

NameLecture Notes in Computer Science
Volume7521
ISSN (Print)0302-9743

Conference

Conference9th International Colloquium on Theoretical Aspects of Computing (ICTAC 2012)
Abbreviated titleICTAC 2012
Country/TerritoryIndia
CityBangalore
Period24/09/1227/09/12

Fingerprint

Dive into the research topics of 'A cure for stuttering parity games'. Together they form a unique fingerprint.

Cite this