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 language | English |
---|---|
Title of host publication | Theoretical Aspects of Computing – ICTAC 2012 (9th International Colloquium, Bangalore, India, September 24-27, 2012. Proceedings) |
Editors | A. Roychoudhury, M. D'Souza |
Place of Publication | Berlin |
Publisher | Springer |
Pages | 198-212 |
ISBN (Print) | 978-3-642-32942-5 |
DOIs | |
Publication status | Published - 2012 |
Event | 9th International Colloquium on Theoretical Aspects of Computing (ICTAC 2012) - Bangalore, India Duration: 24 Sept 2012 → 27 Sept 2012 Conference number: 9 |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Volume | 7521 |
ISSN (Print) | 0302-9743 |
Conference
Conference | 9th International Colloquium on Theoretical Aspects of Computing (ICTAC 2012) |
---|---|
Abbreviated title | ICTAC 2012 |
Country/Territory | India |
City | Bangalore |
Period | 24/09/12 → 27/09/12 |