Is there anyway to express a Product Buchi game as a parity game? There is no stochasticity in my original turn-based game and a Deterministic Buchi Automaton is constructed for LTL specifications.


I will assume that by "Product Buchi game", you mean the (synchronous) product of a deterministic Buchi automaton and some kind of plant or deterministic finite automaton that represents the rules of the game (so to speak) apart from the specification.

You then translated this product between the Buchi automaton and a deterministic automaton to a game by assigning atomic propositions (of which the actions of the two players are composed) or characters to the two players. You have a Buchi game then. Because in your question you state that you want to represent a Product Buchi game as a parity game, I will assume that you have this product Buchi game already.

Translating a Buchi game to a parity game is now easy: Let $\mathcal{F}$ be the set of accepting states/vertices/positions in the Buchi game. Then, you can replace $\mathcal{F}$ by the following coloring function (for every vertex $v$):

$$ c(v) = \begin{cases} 1 & \text{ if } v \in \mathcal{F} \\ 0 & \text{ otherwise} \end{cases} $$

This will give you a parity game in which the player who was formerly the Buchi player can ensure that the highest color visited infinitely often is odd if and only if it is able to win the Buchi game from which the parity game was translated.

If your definition of parity game reasons about the lowest color visited infinitely often, swap the 0 and 1 in the formula above. Likewise, add 1 to every number if the player should make sure that the highest/lowest color should be even. There are multiple definitions of parity game winning in the literature, which are however all equivalent.

  • $\begingroup$ Thank you very much @DCTLib. It helps me a lot. Is there any source that I can be more familiar with such transformations between different game structures? $\endgroup$ Dec 8 '18 at 3:06
  • $\begingroup$ @arincbulgur Such constructions are scattered throughout the papers available on the topic. They are not interesting enough to make it into the main thread of a paper, so they are only introduced whenever needed. The LNCS 2500 book contains a few of the more tedious constructions, but only those that are in the scope of their main thread. Translating from Buchi to parity is quite simple, so preliminaries often only mention that Buchi is a special case of parity. A product construction between Buchi games should also be part of some papers. $\endgroup$
    – DCTLib
    Dec 9 '18 at 7:40
  • $\begingroup$ Hi again @DCTLib, it will be a late feedback. However, the above configuration didn't give me the right translation. I obtained the right translation, when I colored by 2 the states that I want to visit infinitely open, and by 1 the rest of them. I obtained it by trial and error. I think this is another definition of winning for parity game that you mentioned. But I still don't understand why your suggestion didn't work. $\endgroup$ Feb 22 '19 at 22:07

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.