• 2015/10/19: Add a plugin contributed by Daniel Weibel.
• 2015/10/18: The version 2015-10-18 is released.

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.

The 2010-12-18 version marks the final major release of the first generation of GOAL since 2006-08-23. Subsequent releases of this generation (dated as 2010-12-18pl1, 2010-12-18pl2, and so on) will be mainly for fixing bugs or anomalous behaviors. Contact us if you are interested in obtaining the source code of the first generation.

The next generation of GOAL (starting from 2011-02-14) is a redesign with a new architecture and user interface. Several algorithms are reimplemented and numerous new functions are added.

For Automata

• Drawing Büchi automata and other omega-automata, alternating automata, and also classic finite automata.
• Tests on Büchi automata:
  • Language equivalence between one Büchi automaton and another or a temporal formula
  • On-the-fly model checking of a system automaton against a property automaton
  • Others: input, emptiness, containment, syntactically deterministic, semantically deterministic, and simulation equivalence
• Operations on Büchi automata:
  • Union and Intersection
  • Complement (ten complementation algorithms; some may be run stage-by-stage)
  • Determinization
  • Simplify (by simulation and/or pruning fair sets)
  • Alphabet: expand or contract the alphabet and also rename the symbols
  • And many more
• Tests and operations on classic finite automata are also available.
• Laying out automata by various layout algorithms
• A local repository of pre-drawn and checked Büchi automata (over 100 entries and you may add more) and a viewer of the Büchi Store online repository.

For Formulae

• Translating a temporal (Quantified Propositional Temporal Logic, QPTL) formula into a Büchi automaton.
  • Many well-known translation algorithms are implemented; most of them support past operators.
  • Translation may be performed step-by-step.
• Tests on temporal formulae: Satisfiability and Validity.
• Simplification.

For Games

• Drawing two-player games.
• Several game solvers are implemented, including one for reachability games, one for Büchi games, and four for parity games.
• Some conversions between games are available.

Others

• Command-line mode: most GOAL functions are accessible by programs or scripts.
• Extensibility: several GOAL functions can be extended by plugins based on the Java Plugin Framework.
• File Exporting/Importing:
  • Exporting Büchi automata as Promela code, files in the Graphviz DOT format, JPEG files, PNG files, and LaTeX files.
  • Importing files created by MoDeLLa and LTL2Büchi, JFF files created by JFLAP, Promela never claim output by SPIN, and parity games generated by PGSolver.
• Utility functions: collect statistics, generate random automata and formulae, find maximal strongly connected components, find elementary cycles, and compute simulation relations.
• UI features: snap states to a grid, drag and drop to open a file, align selected states, drag and drop tabs, and many more.
• Multi-core support: some algorithms are divided into tasks run by different threads simultaneously.

Changes to GOAL can be found in the ChangeLog. Some FAQs are also provided.

The source code of the first generation is released per request under GPLv3. The binaries of GOAL are free to use, copy, and distribute for non-commercial purposes.

Latest version: 2015-10-18 (click on the version date to download)

Previous versions can be found here.

The GOAL tool is implemented in Java. You must have a Java runtime (6.0 or above is required) on your machine.

• For Windows
  1. Unzip the downloaded zip file for Windows/Linux.
  2. Execute goal.bat in the extracted folder.
• For Linux
  1. Unzip the downloaded zip file for Windows/Linux.
  2. Execute goal in the extracted folder.
• For Mac OSX
  1. Extract GOAL.dmg (or GOAL-yyyymmdd.dmg) from the downloaded zip file for Mac OSX.
  2. Mount GOAL.dmg (or GOAL-yyyymmdd.dmg) and drag the application bundle to the application folder.
  3. Double click on the GOAL application bundle to run it.

The first generation of GOAL (versions up to 2010-12-18) is packaged as a .jar file. To run the tool in Windows, simply double click the .jar file; in Linux, type “java -jar goal_yyyy_mm_dd.jar” (double click might also work if you know how to set the appropriate system option).

Below are a few use cases of the GOAL tool:

1. Preparing Büchi automaton diagrams for slides/papers/homework
2. Checking correctness of a hand-drawn Büchi automaton
3. “Hand-optimization” of a specification Büchi automaton
4. Combining GOAL with SPIN
5. Checking correctness of a Büchi complementation algorithm
6. Utilizing the Büchi Store

Click here for more details.

More screenshots.

GOAL can be extended by plugins based on the Java Plugin Framework. Plugin examples and users' contributions can be found here.

Current:

• Yih-Kuen Tsay
• Ming-Hsien Tsai
• Chi-Shiang Liu
• Yu-Shiang Hwang

Former:

• Yu-Fang Chen
• Kang-Nien (Conion) Wu
• Wen-Chin Chan
• Chi-Jian Luo
• Jinn-Shu Chang
• Yi-Wen Chang
• Yi-Hsiung Wang
• Jing-Jie Lin

The classic automata and the graph modules of the first generation of GOAL (versions up to 2010-12-18) were adapted and extended from those of JFLAP. We thank Susan H. Rodger, the creator of JFLAP, at Duke University for granting us the permission to use and modify the JFLAP source code.

• Ming-Hsien Tsai, Yih-Kuen Tsay, and Yu-Shiang Hwang. GOAL for Games, Omega-Automata, and Logics. In Proceedings of the 25th International Conference on Computer Aided Verification (CAV 2013), LNCS 8044, 883-889, July 2013. [Springer]
• Yih-Kuen Tsay, Ming-Hsien Tsai, Jinn-Shu Chang, Yi-Wen Chang, and Chi-Shiang Liu. Büchi Store: An Open Repository of ω-Automata. International Journal on Software Tools for Technology Transfer, 15(2):109-123, 2013. [Springer]
• Yih-Kuen Tsay, Ming-Hsien Tsai, Jinn-Shu Chang, and Yi-Wen Chang. Büchi Store: An Open Repository of Büchi Automata. In Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2011), LNCS 6605, 262-266, March/April, 2011. [Springer] [original submission]
• Ming-Hsien Tsai, Seth Fogarty, Moshe Y. Vardi, and Yih-Kuen Tsay. State of Büchi Complementation. In Proceedings of the 15th International Conference on Implementation and Application of Automata (CIAA 2010), LNCS 6482, 261–271, August, 2010. [Springer] [full version][test set][GOAL for experiments]
• Yih-Kuen Tsay, Yu-Fang Chen, Ming-Hsien Tsai, Kang-Nien Wu, Wen-Chin Chan, Chi-Jian Luo, and Jinn-Shu Chang. Tool Support for Learning Büchi Automata and Linear Temporal Logic. Formal Aspects of Computing, 21(3):259-275, 2009. [Springer] [preprint]
• Yih-Kuen Tsay, Yu-Fang Chen, Ming-Hsien Tsai, Wen-Chin Chan, and Chi-Jian Luo. GOAL Extended: Towards a Research Tool for Omega Automata and Temporal Logic. In Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008), LNCS 4963, 346–350, March/April, 2008. [Springer] [slides] [preprint]
• Yih-Kuen Tsay, Yu-Fang Chen, Ming-Hsien Tsai, Kang-Nien Wu and Wen-Chin Chan. GOAL: A Graphical Tool for Manipulating Büchi Automata and Temporal Formulae. In Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2007), LNCS 4424, 466–471, March/April, 2007. [Springer] [slides] [preprint]
• Yih-Kuen Tsay, Yu-Fang Chen, and Kang-Nien Wu. Tool Support for Learning Büchi Automata and Linear Temporal Logic. The 2006 Formal Methods in the Teaching Lab Workshop (A Workshop at the Formal Methods 2006 Symposium), August 26, 2006. [slides]

Please send all inquiries/comments to the following email address.

Thank you!