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.
- Platform independent part: GASt.jar
- Linux: linux.tgz
- Windows: windows.zip
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