Main Functions

In this section, we describe the main functions of GOAL along with some highlights of their implementation.

Graphical Manipulation of Games and Automata

The user can easily point-and-click and drag-and-drop to create a game, an ω-automaton, an alternating ω-automaton, or a two-way alternating automaton; see

1

The tool is available at http://goal.im.ntu.edu.tw/.

Translation of QPTL Formulae

Tableau *, IncTableau * [49], Tester * [50], GPVW * [34],

GPVW+ * [34], LTL2AUT * [34], LTL2AUT+ *, LTL2BA * [32], PLTL2BA * [33], MoDeLLa [81], Couvreur [16], LTL2BUCHI [35], KP02 [51], CCJ09 [13]

Complementation of B¨uchi Automata

Safra* [77], WAPA* [89], WAA* [57], Safra-Piterman* [74], Kurshan’s [59], Ramsey-based [8, 83], Muller-Schupp [70, 4], Rank-based [57, 79], Slice-based [47]

Simplification of Automata

Direct and Reverse Simulation* [86], Pruning Fair Sets* [86], Delayed Simulation [24], Fair Simulation [38], Parity Simplification [9]

Parity Game Solving

Recursive [60], McNaughton-Zielonka [68, 104], Dominion Decomposition [46], Small Progress Measure [45], Big Steps [78], Global Optimization [28]

Table 7.1: Major algorithms in GOAL. The Modified Safra algorithm for comple-mentation is a slight variation of Safra’s construction.

Figure 7.1. After a game or an automaton is created, the user can lay it out au-tomatically by various layout algorithms implemented in GOAL. If the automatic layout is not satisfactory, the user can manually arrange the states of the automaton in a better shape with the help of snap to grid and display of gridlines provided by GOAL.

Translation of Logic Formulae

Fourteen algorithms have been implemented for QPTL formula to B¨uchi automa-ton translation; see Table 7.1. It is also possible to translate a formula into a generalized B¨uchi automaton, instead of going all the way to a B¨uchi automaton.

Five (Tableau, Incremental Tableau, Temporal Tester, KP02, and PLTL2BA) of them originally supported past operators. We have extended six more (GPVW, LTL2AUT, LTL2AUT+, MoDeLLa, Couvreur’s , and LTL2BUCHI) to allow past operators. Except KP02 that originally supports full QPTL formulae, all the other thirteen algorithms are further extended to support QPTL formulae convertible to prenex normal form. It has been shown that QPTL in prenex normal form is

Figure 7.1: An example of drawing a B¨uchi automaton with GOAL. The B¨uchi automaton is intended for32p. The inset window is the dialog window for updating the accepting states.

as expressive as QPTL [83]. The supported boolean and temporal operators and their input formats are shown in Table 7.2. To help learning, translations by six of the fourteen algorithms (Tableau, GPVW, GPVW+, LTL2AUT, LTL2AUT+, and MoDeLLa) can be viewed step-by-step. For instance, in the Tableau algorithm the user gets to see the closure computed for the given temporal formula, atoms created as states of the automaton, and transitions between states added one by one. Text is displayed to explain the intermediate step being carried out. The user can “play”

the translation, “pause” it, and then “resume” it. A snapshot of translating 23p with the Tableau algorithm is shown in Figure 7.3.

Besides QPTL, GOAL also supports the translation of an ACTL formula [72] to a maximal model (represented as an automaton) of the formula [37, 56]. Such model can be used in model checking or synthesis. The translation of ω-regular expressions is also available in GOAL.

Operator ∃ ∀ ¬ ∨ ∧ → ↔ Format 1 E A ~ \/ /\ --> <-->

Format 2 E A ! | & -> <->

Operator

2 3 U W R

2

3

S B T

Format 1 () [] <> U W R (-) (~) [-] <-> S B T

Format 2 X G F U W R Y Z H O S B T

Table 7.2: Boolean and temporal operators supported in GOAL and their input formats.

Conversion between Automata

GOAL supports many conversions between automata, especially the conversion from nondeterministic B¨uchi automata, if possible, to deterministic automata with B¨uchi [61, 6] or co-B¨uchi [6] acceptance conditions. Moreover, GOAL can automat-ically find and apply a sequence of chained conversions to convert an automaton to another type specified by the user. With the chained conversions performed by GOAL automatically, tests of B¨uchi automata and operations on B¨uchi automata can be applied to various types of automata convertible to equivalent B¨uchi au-tomata.

Tests of ω-Automata

Emptiness, (language) containment, (language) equivalence, simulation relations, input, and DBW-recognizable tests are supported. In the emptiness test, if the given ω-automaton is non-empty, GOAL highlights the path that corresponds to an accepted input. The equivalence test on two ω-automata is built on top of the con-tainment test which in turn relies on conversions to B¨uchi automata, the intersection and complementation operations, and the emptiness test. An equivalence test can also be performed between an ω-automaton and a temporal formula. In the input test, if a word provided by the user is accepted by an automaton, an accepting run

Figure 7.2: An example of testing a B¨uchi automaton on a word with GOAL. The B¨uchi automaton is intended for 23p. The word (p¬pp)^ω is represented in ASCII as {(p)(~p)(p)} where (.) is used to separate symbols, lala denotes the negation, and {.} denotes the infinite repetition of the enclosed word. The accepting run is highlighted in green.

of the automaton on the word will be highlighted; see Figure 7.2. The user may also run an input test interactively, or construct the run tree or run dag of an automaton on a word step-by-step.

Boolean Operations on ω-Automata

The three standard boolean operations—union, intersection, and complementation are supported. B¨uchi complementation is crucial in the implementation of language containment and equivalence tests, which are perhaps the most distinct functions of GOAL. Algorithms for B¨uchi complementation, because of their technical difficulty, are themselves a separate topic of learning (and also of research). Ten algorithms have been implemented in GOAL for B¨uchi complementation; see Table 7.1 for a listing. Nine of the ten algorithms can be performed step-by-step or stage-by-stage such that the results of intermediate steps or stage-by-stages can be shown, which will be convenient for learning. Cross-checking greatly increases our confidence in the

Figure 7.3: A screen shot of the step-by-step translation of a temporal formula into an equivalent generalized B¨uchi automaton using the Tableau algorithm. The given PTL formula is 23p. The lower window displays explanatory descriptions, while the steps are played out in the upper window.

correctness of the different complementation algorithms and hence the correctness of the language containment and equivalence tests.

Classification of ω-Regular Languages

We have implemented an algorithm for testing whether an ω-regular language or B¨uchi automaton is star-free [19]. If an ω-regular language is star-free, it can be specified by a formula in PTL, which is less expressive than QPTL. We have also implemented the classification of ω-regular languages into the temporal hierarchy of Manna and Pnueli [65]. Such classification can be used not only for educational purposes but also for helping model checking [10].

Tests on QPTL Formulae

Satisfiability and validity tests are supported. The equivalence test between two formulae is not supported directly, but can be easily realized by connecting the two

formulae with the mutual implication operator (↔) and testing the resulting formula for validity.

Simplifying B¨uchi Automata

The user can use the simplification (by direct simulation, delayed simulation, or fair simulation) operation to find states of a B¨uchi automaton that simulate each other and merge those states (if possible); there is also an operation for simplifying generalized B¨uchi Automata by pruning fair sets (acceptance sets). Four algorithms for finding direct simulation relations are implemented. One algorithm is an adap-tion of that proposed by Somenzi and Bloem [86] and the other three algorithms are adaptions of those proposed by Henzinger et al. [41]. Figure 7.4 shows an ex-ample of running the simplification algorithm on an automaton translated from the formula 2(p → p W q) (once p becomes true, it will remain true continuously until q becomes true, which may never occur). To understand the original machine-translated automaton is somewhat difficult. After the simplification, one gets a smaller automaton, as shown in Figure 7.4(b), which is easier to understand.

Game Solving and Conversion

We have implemented eight game solving algorithms of which one is for reachability games, one for B¨uchi games, and six for parity games. Winning regions and strate-gies in a solved game are highlighted and can be exported with the game to a file.

Four of the parity game solving algorithms as well as the B¨uchi game solving algo-rithm can be performed step-by-step. Several conversions between games, including the conversion from a Muller game to a parity game [67], are implemented. To help experiments with games, the generation of random games is provided as well. GOAL can also take the product of a game arena (that describes the allowed interactions

(a) The automaton before simplification

(b) The automaton after simplification

Figure 7.4: A demonstration of the automaton simplification.

between a module and its environment) and a specification automaton (resulting in a game), and hence may be used to experiment with the synthesis process in a game-based approach to the synthesis of reactive modules [84].

Exporting Games and Automata

Once a B¨uchi automaton has been defined and tested, the user can export it in the Promela (the system modeling language of SPIN) syntax on the screen or as a file.

This makes it possible to use GOAL as a graphical specification definition frontend to an automata-theoretic model checker like SPIN. The user may also export a game or an automaton in various image formats such as JPEG, PNG, and SVG, or to external tools such as JGraph², LBTT [88], and LaTeX.

The Automata Repository

GOAL comes with a local repository which contains a collection of frequently used temporal formulae and their corresponding equivalent B¨uchi automata. These au-tomata have been optimized by hand and checked by the GOAL tool itself. The user can also browse automata and temporal formulae in B¨uchi Store with GOAL. For beginners, this should be very convenient for learning the relation between B¨uchi automata and linear temporal logic.

The Command-Line Mode

This mode makes most of the GOAL functions accessible by programs or shell scripts and therefore provides an interface between GOAL and external tools. GOAL also provides an interpreter that can execute scripts in a customized language. Thus a batch of GOAL commands can be written as a script and executed by a single GOAL

2

JGraph is a tool for the visualization of layout of graphs. It is available in

http://www.jgraph.com.

process to achieve better performance. Sample scripts that compare translation algorithms and output the results as text files are provided. They can be easily adapted to handle other different tasks.

Utility Functions

Utility functions are available for collecting statistic data (numbers of states, transi-tions, and acceptance sets) and for generating random automata, random games, and random temporal formulae. Outputs from external automata tools MoDeLLa [81], LTL2BUCHI [35], and the translation tool in Spin may also be converted to the GOAL File Format (GFF, which is an XML file format designed to cover all ω-automata) for further processing by GOAL.