Gridworld Problem: Game on Graph

This example demonstrates how to construct a game on graph using a Gridworld transition system and an LTL specification for P1.

In general, there are three ways to define a game on graph, namely

• By explicitly adding vertices and edges to the graph and marking the accepting states,
• By providing a transition system and a formal specification,
• By providing a game field and player objects.

Presently, in IGLSynth v0.2.3, only first two are supported. See Gridworld Problem: Game on Graph for an example of constructing game on graph by explicitly adding vertices and edges.

Define Transition System

To define a game using transition system and P1’s specification, first define the transition system. In general, a transition system may be defined using TSys class. In this example, we use a predefined Gridworld transition system from iglsynth.game.gridworld module:

from iglsynth.game.gridworld import *

# Define transition system
tsys = Gridworld(kind=TURN_BASED, dim=(3, 3), p1_actions=CONN_4, p2_actions=CONN_4)
tsys.generate_graph()

Define LTL Specification

To define P1’s objective using an LTL specification, import the logic module:

from iglsynth.logic.ltl import *

An LTL formula is defined over an alphabet. Hence, we start by defining AP objects using which we will construct an alphabet.

In this demo example, we will represent P1’s objective to reach to a goal. Such a reachability specification can be written as \(\varphi = \Diamond a\) where \(a\) is an AP representing goal. So, define the AP as:

GOAL = (0, 0)
a = AP("a", lambda st, *args, **kwargs: st.coordinate[0:2] == GOAL)

and the specification as:

spec = LTL("Fa", alphabet=Alphabet([a]))

Define Game Object

Given a transition system and specification, we will now define a game. To define game, we require the game module:

from iglsynth.game.game import *

Now, instantiate and define a game as follows:

game = Game(kind=TURN_BASED)
game.define(tsys, spec)

Solve the Game

The final step is to invoke a solver to solve the game. We will use Zielonka’s algorithm to solve the above game. Note that Zielonka’s algorithm computes winning region for P1 in a deterministic two-player zero-sum game.

In IGLSynth, Zielonka’s algorithm is implemented in zielonka module:

from iglsynth.solver.zielonka import ZielonkaSolver

To run the solver, first instantiate it and call the solve method:

solver = ZielonkaSolver(game)
solver.solve()

The solver.solve() runs the solver on the Game object game that encodes the game on graph. The solution of solver can be accessed using the properties:

print(solver.p1_win)
print(solver.p2_win)

which returns the winning sets for P1 and P2.