Main Index

Editors

Editors are used to define logic formulae, such as temporal formulae, and automata, such as finite automata, alternating ω-automata, or games. Once a logic formula or automaton/game has been defined, it can be manipulated by the functions included in the menu items that are accessible from the menu bar of an editor window. Currently, there are four editors:

1. Temporal Formula: Currently GOAL can handle a subset of the full QPTL (Quantified Propositional Temporal Logic, which which subsumes LTL) formulae, namely those with quantifiers that do not fall in the scope of temporal operators. This subset is as expressive as the full set of QPTL formulae.
2. Automaton: Currently Büchi automata (BA or NBW) and generalized Büchi automata (GBA or NGBW) are fully supported, while Muller automata (NMW), Rabin automata (NRW), Streett automata (NSW), parity automata (NPW), transition Büchi automata (TBA or NTBW), transition generalized Büchi automata (TGBA or NTGBW), transition Muller automata (NTMW), transition Rabin automata (NTRW), transition Streett automata (NTSW) and transition parity automata (NTPW) are partially supported. GOAL also supports classic finite automata (CLASSIC).
3. Alternating Automaton: Currently alternating automata, including alternating Büchi automata (ABW), universal Co-Büchi automata (UCBW), and alternating parity automata (APW), can only be edited, saved, printed, or translated into NBW.
4. Game: Currently games can only be edited, saved, or printed.

GOAL may also be used in a command-line mode.

Menu Items

The following are fully supported for Büchi automata and generalized Büchi automata, and partially supported for the others.

1. File: file handling options, including saving automata as Promela code.
2. Repository: a collection of common temporal formulae (or description) and their corresponding equivalent Büchi automata.
3. Test: several tests are available for temporal formulae and finite automata. Both temporal formulae and finite automata will remain unchanged after any test.


4. For formulae:
   1. Satisfiability: check whether the formula is satisfiable.
   2. Validity: check whether the formula is valid.
   3. Temporal Hierarchy: check which temporal hierarchy the formula belongs to. [Manna and Pnueli. A hierarchy of temporal properties. PODC '90]
5. For automata:
   1. Input
   2. Emptiness
   3. Containment
   • by Complementation and Intersection
   • by Rank-Based Approach [Kupferman and Vardi. Weak alternating automata are not that weak. ACM Transactions on Computational Logic, '01]
   4. Equivalence
      • with an Automaton
      • with a Formula
   5. On-the-Fly Model Checking
   6. Simulation Equivalence
   7. Semantically Deterministic check if a Büchi automaton is equivalent to some deterministic Büchi automaton.
6. Convert/Translate:
   For automata: from variants of GBA or BA to variants of GBA or BA (using standard algorithms).
   In particular, for transition GBA:
   • To BA [Gastin and Oddoux. Fast LTL to Büchi automata translation. CAV '01]
   • To BA (all permutations): Try all permutations of TGBA acceptance sets.
   For formulae: translate a temporal formula into an equivalent Büchi automaton.
   • Simplification: a subset of formula rewriting rules from [Somenzi and Bloem. Efficient Büchi automata from LTL formulae. CAV '00].
   • To GBA (label-on-state):
     1. Tableau (MP) [Manna and Pnueli. Temporal verification of reactive systems. Springer '95]
     2. Incremental Tableau (KMMP) [Kesten, Manna, McGuire, and Pnueli. A decision algorithm for full propositional temporal logic. CAV '93]
     3. Temporal Tester (KP) [Kesten and Pnueli. Verification by augmented finitary abstraction. IC '00]
     4. Extended On-the-Fly (GPVW) [Gerth, Peled, Vardi, and Wolper. Simple on-the-fly Automatic verification of linear temporal logic. PSTV '95]: this is an extension of the original on-the-fly algorithm, which applies for formulae containing quantifiers or past operators.
     5. Extended On-the-Fly (GPVW+): the same on-the-fly algorithm with enhancements suggested in the above paper. the algorithm has also been extended to handle formulae containing quantifiers or past operators.
     6. Extended LTL2AUT (DGV) [Daniele, Giunchiglia, and Vardi. Improved automata generation for linear temporal logic. CAV '99]: this is an extension of the original LTL2AUT algorithm, which applies for formulae containing quantifiers or past operators.
     7. Extended LTL2AUT+ (DGV): this is a slightly improved version of the original LTL2AUT algorithm.
   • To GBA:
     1. Tableau (MP)
     2. Incremental Tableau (KMMP)
     3. Temporal Tester (KP)
     4. Extended On-the-Fly (GPVW)
     5. Extended On-the-Fly (GPVW+)
     6. Extended LTL2AUT (DGV)
     7. Extended LTL2AUT+ (DGV)
     8. MoDeLLa (ST) [Sebastiani and Tonetta. "More deterministic" v.s. "Smaller" Büchi automata for efficient LTL model checking. CHARME '03]
   • To BA (label-on-state):
     1. Tableau (MP)
     2. Incremental Tableau (KMMP)
     3. Temporal Tester (KP)
     4. Extended On-the-Fly (GPVW)
     5. Extended On-the-Fly (GPVW+)
     6. Extended LTL2AUT (DGV)
     7. Extended LTL2AUT+ (DGV)
   • To BA:
     1. Tableau (MP)
     2. Incremental Tableau (KMMP)
     3. Temporal Tester (KP)
     4. Extended On-the-Fly (GPVW)
     5. Extended On-the-Fly (GPVW+)
     6. Extended LTL2AUT (DGV)
     7. Extended LTL2AUT+ (DGV)
     8. MoDeLLa (ST)
     9. LTL2BA (GO) [Gastin and Oddoux. Fast LTL to Büchi automata translation. CAV '01]
     10. PLTL2BA (GO) [Gastin and Oddoux. LTL with past and two-way very-weak alternating automata. MFCS '03]
     11. Couvreur’s Algorithm [Couvreur. On-the-fly verification of linear temporal logic. FM '99]
     12. LTL2BUCHI (GL) [Giannakopoulou and Lerda. From states to transitions: Improving translation of LTL formulae to Büchi automata. FORTE '02]
     13. LTL2BUCHI+ (GL): the conversion from LTL formula to TGBA is the same as in LTL2BUCHI, but the conversion from TGBA to BA follows instead the same algorithm as used in LTL2BA, which appears to perform better.
   • To GBA (label-on-state, step-by-step): translate a temporal formula into an equivalent label-on-state GBA step by step.
     1. Tableau (MP)
     2. Extended On-the-Fly (GPVW), explained in the terminology of LTL2AUT
     3. Extended On-the-Fly (GPVW+), explained in the terminology of LTL2AUT
     4. Extended LTL2AUT (DGV)
     5. Extended LTL2AUT+ (DGV)
   • To Transition GBA:
     1. Couvreur’s Algorithm
     2. LTL2BUCHI(GL)
   • To Alternating Automaton:
     1. LTL2VWAA (GO), this algorithm is an intermediate step of LTL2BA algorithm.
7. Operation: functions for manipulating Büchi and other types of automata.
   1. Duplicate: create a duplicate automaton.
   2. Duplicate without ACC: create a duplicate automaton without acceptance condition.
   3. Union: generate the union of the current and another chosen automaton.
   4. Intersection: generate the intersection of the current and another chosen automaton.
   5. Complement: generate the complement of the current automaton.
      In particular, for Büchi Automata:
      1. Ramsey-Based Construction [Büchi. On a decision method in restricted second order arithmetic. Congress on Logic, Method, and Philosophy of Science '60] [Sistla, Vardi, and Wolper. The complementation problem for Büchi automata with applications to temporal logic. TCS '87]
      2. Kurshan's Construction (for DBW) [Kurshan. Complementing deterministic Büchi automata in polynomial time. JCSS '87]
      3. Safra's Construction [Safra. On the complexity of omega-automata. FOCS '88]
      4. Modified Safra's Construction: this is the same as Safra's construction, except that we exchange the steps of computing successors and creating sons when constructing Safra trees.
      5. Muller-Schupp Construction [Muller and Schupp. Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra. TCS '95] [Althoff, Thomas, and Wallmeier. Observations on determinization of Büchi automata. Theoretical Computer Science, '06]
      6. Via Weak Alternating Parity Automaton [Thomas. Complementation of Büchi automata revisited. '99]
      7. Via Weak Alternating Automaton [Kupferman and Vardi. Weak alternating automata are not that weak. ACM Transactions on Computational Logic, '01] (The rank is 2*(n-F), where n is the size of state and F is the size of Büchi acceptance condition)
      8. Safra-Piterman Construction [Piterman. From nondeterministic Büchi and Streett automata to deterministic parity automata. LICS '06]
      9. Rank-Based Construction: the basic rank-based complementation algorithm is based on [Kupferman and Vardi. Weak alternating automata are not that weak. ACM Transactions on Computational Logic, 2001], and other optimizations are based on [Schewe. Büchi complementation made tight. STACS '09].
      10. Slice-Based Construction: besides of the basic slice-based complementation algorithm [Kähler and Wilke. Complementation, disambiguation, and determinization of Büchi automata unified. ICALP '08.], several optimizations proposed by Seth Fogarty and Ming-Hsien Tsai are also implemented.
   6. Complement (Stage-by-Stage): generate the complement of the current automaton stage by stage.
      In particular, for Büchi Automata:
      1. Safra's Construction : NBW → DRW → (complement) DSW → NBW
      2. Modified Safra's Construction: NBW → DRW → (complement) DSW → NBW
      3. Muller-Schupp Construction: NBW → DRW → (complement) DSW → NBW
      4. Via Weak Alternating Parity Automaton: NBW → APW → (complement) NBW
      5. (Temporarily disabled) Via Weak Alternating Automaton: NBW → (complement) UCBW (viewed as one; no actual conversion) → VWAA (very weak alternating automaton; a special case of ABW) → NBW
      6. Safra-Piterman Construction: NBW → DPW → (complement) DPW → NBW
      7. Rank-Based Construction: Rank-based completementation performed step-by-step
      8. Slice-Based Construction: Slice-based completementation performed step-by-step
   7. Determinization: generate the determinization of the current automaton.
      In particular, for Büchi Automata:
      1. Safra's Construction: NBW → DRW
      2. Modefied Safra's Construction: NBW → DRW
      3. Muller-Schupp Construction: NBW → DRW
      4. Safra-Piterman Construction: NBW → DPW
   8. Minimization: generate the minimized determinization of the current automaton. This applies only to classic finite automaton.
   9. Simplify (by Simulation) [Somenzi and Bloem. Efficient Büchi automata from LTL formulae. Section 5, CAV '00]: remove redundant states, including unreachable states, dead states, and states that are simulation-equivalent to another state.
   10. Simplify (by Pruning Fair Sets) [Somenzi and Bloem. Efficient Büchi automata from LTL formulae. Section 6, CAV '00]: remove redundant automaton information (states or fair sets) by analyzing the fair sets. This applies only to GBA.
   11. Simplify (by the Wring approach) [Somenzi and Bloem. Efficient Büchi automata from LTL formulae. CAV '00]: repeatedly apply the above two simplification methods until a fix-point is reached.
   12. Maximize Acceptance Set: maximize the acceptance set of a Büchi automaton without changing its language.
   13. Closure: take the safety closure of the given automaton.
   14. Reduce: remove unreachable and dead states.
   15. Alphabet: operations on the alphabet, including add/remove an atomic proposition, rename an atomic proposition, and show current atomic propositions.
   16. Statistics: get the number of states and the number of transitions.
   17. Get intermediate GBA: get the intermediate generalized Büchi automaton, if the Büchi automaton is translated from a temporal formula. This function does not apply for LTL2BA or PLTL2BA, which uses intermediate GBA with acceptance conditions on transitions.
8. Preference: adjust the user preferences.
9. Help: go to various help pages such as this one.