compute the i-attractor of a set of states phi in paritry game pg

The teaching tool for omega-automata synthesis.

Automaton2MooreGame converts an automaton to a parity game that aims at the synthesis of a Moore machine, i.e., outputs are determined by the state only. The ranks are determined in that accepting states get rank 1 while other states of the automaton have rank 0, and the intermediate states will have the rank of their source state.

The teaching tool for boolean unification.

CopsAndRobber game: a cop and a robber are placed on an undirected graph and make alternating moves. Clearly, the cop aims at catching the robber and the robber wants to escape forever, so that we have a safety or liveness game. The game is also known as a video game called Pacman, and graphs that are cop-win graphs are well researched [AiFr84,GaTT18]. The function below is given the edge relation where only one direction between two vertices is sufficient, and the initial state (r,c,t) where r and c are the vertices where the robber and the cop are located at the beginning, and t is a boolean value that is true if the cop is making the next move. The function converts the graph to a game graph whose nodes are triples (r,c,t) like the initial state, and solves the game. The function returns a triple (pg,win,strat) where pg is the parity game and win[i] are the winning states of player i and finally strat[i] is the strategy of player i, where player 0 is the cop and player 1 is the robber.

This function is the teaching tool for the CopRobberGame; it reads the edge relation, and the initial state from a html form input, and uses function CopRobberGame to generate and solve the graph game. The tool then prints the solved graph game as svg graphics on the generated html page and prints also a transition relation for the graph game if viewed as a Kripke structure. The locations of the robber and cop are then binary encoded with boolean variables rN,...,r0 and cN,...,c0, resp.

DetF2LivenessGame converts a given DetF automaton to a LivenessGame where player 0 tries to reach accepting states, i.e., rank-1 states, and where player 1 tries to avoid these.

DetFG2ParityGame converts a given DetFG automaton to a ParityGame where player 0 tries to visit from a certain point of time onwards only accepting states of the given DetFG automaton, and player 1 tries to infinitely often escape from these.

DetG2SafetyGame converts a DetG automaton to a safety game where player 0 aims at exclusively using safe states (having rank 1), and where player 1 aims at reaching a rank-0 state.

DetGF2ParityGame converts a given DetGF automaton to a ParityGame where player0 tries to infinitely often visit accepting states of the DetGF automaton, and player 1 tries to visit them only finitely often.

example of DiRu10:

generic example from Frie11 where Frie11(n) recursively calls Frie11(n-1) and Frie11(n-2) to prove exponential runtime

writing a parity game as graphiz graph

The teaching tool for solving parity games.

parsing a parity game from a string; the syntax is explained by the following example: player0 3,4,5,6; player1 0,1,2,7; ranks 0:0; 1:1; 2:2; 3:3; 4:4; 5:5; 6:6; 7:8; transitions 0->1; 0->3; 1->4; 1->6; 2->0; 2->5; 3->2; 4->0; 4->1; 5->7; 6->1; 6->7; 7->2; 7->5;

Solve a liveness game which is encoded as a parity game with ranks 1 for the states that must be reached by player 0 (liveness) and must be avoided by player 1 (safety).

This function solves a given parity game by Zielonka's recursive algorithm. It returns a tuple (win,strat) where win[i] are the winning states of player i and strat[i] is the strategy of player i.

Solve a safety game which is encoded as a parity game with ranks 1 for the safe states that must be exclusively used by player 0 (safety) and where player 1 tries to escape from.

example of Wikipedia:

This function solves a given parity game by Zielonka's recursive algorithm. It returns a tuple (win,st,traceL,gA) where win[i] are the winning states of player i, st[i] is the strategy of player i, traceL is a list of the recursive calls with detailed information of intermediate steps, and gA is the latest game number used in that list. The initial call requires a number gameNum which is the first number of these games.