The tool below can be used to solve parity games by Zielonka's algorithm. For the specified parity game, it computes the winning states of both players as well as their strategies, and shows how these were computed by Zielonka's algorithm.
The syntax for the state transition systems (the Kripke structures) should be obvious: states are integers 0,...,n as listed for both players. The ranks of the states are given as declarations in the rank section where state s is given rank r by writing s:r. Finally, transitions are given in the form i->j denoting a transition from state i to state j.
The tool below can be used to check whether there is a Mealy or Moore automaton that can determine the output variables listed below such that the LTL formula will be satisfied by every trace of input/output variables of that automaton. The given LTL formula must only use variables which are either input or output variables of that automaton.
The tool below can be used to synthesize a Moore automaton (if possible) that will select output values in each state such that a given safety/liveness/persistence/fairness property is achieved. Note that the given omega-automaton has to be deterministic in the sense that every state has for every pair (i,o) of an input and an output exactly one transition.
The syntax for the state transition systems (the Kripke structures) should be obvious: states are integers 0,...,n as listed for both players. The ranks of the states are determined by the acceptance conditions.
The tool below can be used to find a most general unifier for two boolean functions that is computed by boolean unification. This means, it computes, if possible, a substitution of the variables by boolean functions such that the two given boolean functions become the same.
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 game is played on an undirected graph, but you may just enter one pair (x,y) for connected nodes x and y. For the initial state, provide a triple (r,c,t) where r and c are the vertices where the robber and the cop are located at the beginning, and t is either cop or robber and denotes which of both will make the first move.
The tool reduces the given cop and robber game to an equivalent parity game which is actually a safety/liveness game. After solving the game, the game graph is printed with the strategies of both players.