Using games to check a simulation

Python
C++

This example demonstrates how to use Spot's game interface to compute a simulation-relation between the states of an automaton. This algorithm is inspired from Fair Simulation Relations, Parity Games, and State Space Reduction for Büchi Automata (Kousha Etessami and Thomas Wilke, and Rebecca A. Schuller).

The code below is intended for demonstration of how to construct and use games. Spot contains some other (and faster) implementation to reduce an automaton using simulation-based reductions (see spot.simulation() and spot.reduce_direct_sim()).

Let us start with a definition of simulation for transition-based generalized-Büchi automata: A state \(s'\) simulates \(s\) iff for any transition \((s,c,a,d)\) leaving \(s\), there exists a transition \((s',c',a',d')\) leaving \(s'\) with a condition \(c'\) that covers \(c\), some colors \(a'\supseteq a\) that covers the colors of \(a\) other transition, and reaching a destination state \(d'\) that simulates \(d\).

In the following automaton, for instance, state 5 simulates state 1, and state 4 simulates state 0.

HOA: v1
States: 6
Start: 0
AP: 2 "a" "b"
Acceptance: 1 Inf(0)
--BODY--
State: 0
[1] 1
[1] 2
State: 1
[0&1] 1
State: 2
[0] 3
State: 3
[1] 3 {0}
State: 4
[1] 5
State: 5
[0] 5 {0}
--END--

Whether two states are in simulation can be decided as a game between two players. If the game is in state \((q,q')\), spoiler (player 0) first selects a transition from state \(q\), and duplicator (player 1) then has to choose a compatible transition from state \(q'\). Duplicator of course wins if it always manages to select compatibles transitions, otherwise spoiler wins.

The game arena can be encoded by associating each state to a pair of integers. States owned by player 0 (rounded rectangles) are pairs \((q,q')\) denoting the position of each player. States owned by player 1 (diamonds) are pairs \((e,q')\) where \(e\) is the number of the edges that player 0 just took (those numbers appears as #1, #2, etc. in the previous picture).

Here is how the game arena look like starting from \((q,q')=(4,0)\):

In this game, player 1, wins if it has a strategy to force the game to satisfy the acceptance condition. Here the acceptance condition is just true, so any infinite play will satisfy it.

Clearly, it is enough for player 1 to always go to \((5,1)\) when possible. If Spot is used to solve this game, the result can be presented as follows, where greens states represents states from which player 1 has a winning strategy, and red states are states from which player 0 has a winning strategy. The highlighted arrows show those strategies.

Since player 1 is winning from state \((4,0)\), we know that state 4 simulates state 0. Also since player 1 would also win from state \((5,1)\), we can tell that state 5 simulates state 1. We also learn that state 5 does not simulate states 2 and 3. We could build other games, or add more state to this game, to learn about other pairs of states.

Python

We now look at how to create such a game in Python.

Essentially, a game in Spot is just an automaton equiped with a named property "state-player" that hold a Boolean vector indicating the owner of each state. The game can be created using the usual automaton interface, and the owners are set by calling game.set_state_players() with a vector of Boolean at the very end.

import spot
from spot import buddy

def direct_sim_game(aut, s1, s2):
    if s1 >= aut.num_states() or s2 >= aut.num_states():
        raise ValueError('invalid state number')
    assert aut.acc().is_generalized_buchi()

    game = spot.make_twa_graph()
    # The names of the states are pairs of integers
    # (q,q') for states owned by player 0
    # (e,q') for states owned by player 1
    # These arrays are indiced by state numbers.
    names = []
    owners = []
    # The reverse assotiation (x,y) -> state number
    # must be kept for each player, since (x,y) can mean two different thing.
    s_orig_states = {}
    d_orig_states = {}
    # a list of player 0 states to process
    todo = []

    # Create the state (i, j) for a player if it does not exist yet and
    # return the state's number in the game.
    def get_game_state(player, i, j):
        orig_state = s_orig_states if player else d_orig_states
        if (i, j) in orig_state:
          return orig_state[(i, j)]
        s = game.new_state()
        names.append((i, j))
        owners.append(player)
        orig_state[(i, j)] = s
        # If it is a new state for Player 0 (spoiler)
        # we need to process it.
        if not player:
            todo.append(s)
        return s

    game.set_init_state(get_game_state(False, s1, s2))
    while todo:
        cur = todo.pop()
        # todo contains only player 0's states, named with pairs
        # of states.
        (s_src, d_src) = names[cur]

        # Player 0 is allowed to pick edge from s_src:
        for s_edge in aut.out(s_src):
            edge_idx = aut.edge_number(s_edge)
            st2 = get_game_state(True, edge_idx, d_src)
            # label the edge with true, because it's an automaton,
            # but we do not use this label for the game.
            game.new_edge(cur, st2, buddy.bddtrue)

            # Player 1 then try to find an edge with the
            # a compatible same condition and colors, from d_src.
            for d_edge in aut.out(d_src):
                if (buddy.bdd_implies(d_edge.cond, s_edge.cond) \
                    and d_edge.acc.subset(s_edge.acc)):
                    st3 = get_game_state(False, s_edge.dst, d_edge.dst)
                    game.new_edge(st2, st3, buddy.bddtrue)

    # Name each state with a string, just so we can read the pairs
    # when the automaton is displayed.
    game.set_state_names(list(map(str, names)))
    # This only line is actually what turns an automaton into a game!
    game.set_state_players(owners)
    return game

To solve a safety game g that has been created by the above method, it is enough to just call solve_safety_game(g). The function solve_game(g) used below is a more generic interface that looks at the acceptance condition of the game to dispatch to the more specific game solver. These functions return the player winning in the initial state. However, as a side effect they define additional automaton properties that indicate the winner of each state, and the associated strategy.

Therefore, to list all simulation pairs we learned from a game starting in state \((i,j)\), we could proceed as follows:

def list_simulations(aut, i, j):
    g = direct_sim_game(aut, i, j)
    spot.solve_game(g)

    winners = g.get_state_winners()
    owners = g.get_state_players()
    names = g.get_state_names()

    simulations = []
    for i in range(0, g.num_states()):
        if winners[i] and not owners[i]:
            simulations.append(tuple(map(int, names[i][1:-1].split(', '))))

    return simulations

On our running example, that gives:


print(list_simulations(aut, 4, 0))

[(4, 0), (5, 1)]

C++

Here is some almost equivalent code in C++.

Here instead of naming states with strings, we use the "product-states" property, which is usually used to display pair of integers that come from a product of automata.

#include <spot/twaalgos/game.hh>
#include <spot/twa/twagraph.hh>

spot::twa_graph_ptr direct_sim_game(spot::const_twa_graph_ptr aut,
                                    unsigned s1, unsigned s2)
{
  if (s1 >= aut->num_states() || s2 >= aut->num_states())
    throw std::runtime_error("direct_sim_game(): invalid state number");

  auto game = spot::make_twa_graph(spot::make_bdd_dict());

  auto names = new std::vector<std::pair<unsigned, unsigned>>();
  game->set_named_prop("product-states", names);

  auto owners = new std::vector<bool>();
  game->set_named_prop("state-player", owners);

  std::map<std::pair<unsigned, unsigned>, unsigned> s_orig_states;
  std::map<std::pair<unsigned, unsigned>, unsigned> d_orig_states;
  std::vector<unsigned> todo;

  auto new_state = [&](bool player, unsigned s1, unsigned s2)
  {
    auto& m = player ? s_orig_states : d_orig_states;
    if (auto it = m.find({s1, s2}); it != m.end())
      return it->second;
    unsigned s = game->new_state();
    names->emplace_back(s1, s2);
    owners->push_back(player);
    m.insert({{s1, s2}, s});
    if (!player)
      todo.push_back(s);
    return s;
  };

  game->set_init_state(new_state(false, s1, s2));
  while (!todo.empty())
    {
      unsigned cur = todo.back();
      todo.pop_back();
      auto [s_src, d_src] = (*names)[cur];

      for (const auto& s_edge : aut->out(s_src))
        {
          unsigned edge_idx = aut->edge_number(s_edge);
          unsigned st2 = new_state(true, edge_idx, d_src);
          game->new_edge(cur, st2, bddtrue);
          for (const auto& d_edge : aut->out(d_src))
            if (bdd_implies(d_edge.cond, s_edge.cond)
                && d_edge.acc.subset(s_edge.acc))
              {
                unsigned st3 = new_state(false, s_edge.dst, d_edge.dst);
                game->new_edge(st2, st3, bddtrue);
              }
        }
    }

  return game;
}

std::vector<std::pair<int,int>>
list_simulation(spot::const_twa_graph_ptr aut,
                unsigned i, unsigned j)
{
  auto g = direct_sim_game(aut, i, j);
  spot::solve_game(g);

  const std::vector<bool>& winners = spot::get_state_winners(g);
  const std::vector<bool>& owners = spot::get_state_players(g);

  typedef std::vector<std::pair<unsigned, unsigned>> names_t;
  auto names = *g->get_named_prop<names_t>("product-states");

  std::vector<std::pair<int,int>> res;

  unsigned n = g->num_states();
  for (unsigned i = 0; i < n; ++i)
    if (winners[i] && !owners[i])
      res.emplace_back(names[i]);
  return res;
}

Now to execute the above code on our example automaton, we just need to read the automaton from a file.

#include <iostream>
#include <spot/twa/twagraph.hh>
#include <spot/parseaut/public.hh>

int main()
{
  spot::parsed_aut_ptr pa = parse_aut("tut40.hoa", spot::make_bdd_dict());
  if (pa->format_errors(std::cerr))
    return 1;
  if (pa->aborted)
    {
      std::cerr << "--ABORT-- read\n";
      return 1;
    }
  for (auto [i,j]: list_simulation(pa->aut, 4, 0))
    std::cout << i << " simulates " << j << '\n';
  return 0;
}

4 simulates 0
5 simulates 1

Using games to check a simulation

Table of Contents

Python

C++