Bisimulations over Parity Formulas
Tianwei Zhang

Abstract:
This thesis is an investigation into how to define the notion of bisimulation over parity formulas. We provide and argue for a list of criteria against which we could judge how good such a definition is. In general, a notion of bisimulation should be sound, closed under union and composition, easily decidable and as close to being complete as possible. It should also guarantee the existence of a largest bisimulation, namely the bisimilarity relation. Particular to the situation with parity formulas, a good bisimulation should also have a ’relative flavor’ in its handling of the priority condition. We propose four definitions of bisimulations over parity formulas and evaluate each of them according to those criteria. We especially argue for one of the four definitions to be the best by far, since it satisfies all qualitative criteria and lies in a relatively good position on the ’spectrum of completeness’. We also provide an adequate bisimilarity game for this notion of bisimulation which makes it easier to work with the notion.