This paper reports extensions to the GOAL tool that enable it to become a research tool for omega automata and temporal logic. The extensions include an expanded collection of translation, simplification, and complementation algorithms, a command-line mode which makes GOAL functions accessible by programs, and utility functions for such common tasks as file format conversion, random formulae generation, and statistics collection.
展开▼