A cure for stuttering parity games

Research output: Book/ReportReportAcademic

8 Citations (Scopus)
87 Downloads (Pure)

Abstract

We de¿ne 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(n^2 m) 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 veri¿cation problems.
Original languageEnglish
Place of PublicationEindhoven
PublisherTechnische Universiteit Eindhoven
Number of pages25
Publication statusPublished - 2012

Publication series

NameComputer science reports
Volume1205
ISSN (Print)0926-4515

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

  • Cite this

    Cranen, S., Keiren, J. J. A., & Willemse, T. A. C. (2012). A cure for stuttering parity games. (Computer science reports; Vol. 1205). Eindhoven: Technische Universiteit Eindhoven.