GASt

The experimental platform GASt (Games, Automata & Strategies) consists of three parts:

  • Determinisation of non-deterministic Büchi automata (formaly known as OmegaDet). Implemented algorithms are:
    • Safra
    • Muller-Schupp
    • improved Muller-Schupp
    • Breakpoint construction by Miyano/Hayashi
  • Synthesis of infinite two player games. Implemented games are:
    • Reachability games
    • Safety games
    • Weak parity games
    • Staiger-Wagner games
    • Request-Response games
    • Büchi games
    • Generalized Büchi games
    • Parity games
    • Muller games
    • Simple Streett games
    • Streett games
    • Mean payoff games
  • Synthesis of Live Sequence Charts (formaly known as REMoRDS)

Download

The current version of the program can be copied and used freely for any non-commercial purpose.

Examples of non-deterministic Büchi automata (from our CIAA paper)

Automaton Safra Muller-Schupp Optimized Muller-Schupp Breakpoint
a0.nba a0.saf a0.ms a0.ms+
a1.nba a1.saf a1.ms a1.ms+ a1.brk
m1.nba m1.saf m1.ms m1.ms+
m2.nba m2.saf m2.ms.tar.bz2 m2.ms+
m3.nba m3.saf Please compute yourself m3.ms+.tar.bz2
m4.nba m4.saf.tar.bz2 Please compute yourself
m5.nba Please compute yourself

Literature

C. Schulte Althoff, W. Thomas, and N. Wallmeier. Observations on determinization of Büchi automata. In Proceedings of the 10th International Conference on the Implementation and Application of Automata, CIAA 2005, volume 3845 of Lecture Notes in Computer Science, pages 262-272. Springer, 2005. (c) Springer.
[ pdf | ps | Abstract ]

C. Schulte Althoff, W. Thomas, and N. Wallmeier. Observations on determinization of Büchi automata. Theoretical Computer Science, 363(2):224-233, October 2006.
[ pdf | ps | Abstract ]

Y. Bontemps. Relating Inter-Agent and Intra-Agent Specifications (The Case of Live Sequence Charts). PhD Thesis, April 2005, University of Namur (Belgium).
[ pdf ]

Contact

Dipl.-Inform. Nico Wallmeier, RWTH Aachen, Lehrstuhl für Informatik 7, 52056 Aachen,
e-mail: wallmeier@informatik.rwth-aachen.de