GOAL

GOAL is a graphical interactive tool for defining and manipulating Büchi automata and temporal logic formulae. It also partially supports other variants of omega-automata. The GOAL tool can be used for educational purposes, helping the user get a better understanding of how Büchi automata work and how they are related to linear temporal logics. It may also be used to construct correct and smaller specification automata, supplementing model checkers such as SPIN that adopt the automata-theoretic approach. Since the release dated 2007-06-01, most functions can be accessed by programs or scripts, making GOAL convenient for supporting research. The acronym GOAL was originally derived from “Graphical Tool for Omega-Automata and Logics”. It also stands for “Games, Omega-Automata, and Logics”, as we gradually add support for omega-regular games. Our long-term goal is for the tool to handle all the common variants of omega-automata and the logics that are expressively equivalent to these automata. Therefore, the GOAL tool will constantly be extended and improved; please come back once in a few months for a better version.