GOAL Extended: Towards a Research Tool for Omega Automata and Temporal Logic

  • Yih-Kuen Tsay
  • Yu-Fang Chen
  • Ming-Hsien Tsai
  • Wen-Chin Chan
  • Chi-Jian Luo
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4963)


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.


Temporal Logic Linear Temporal Logic Translation Algorithm Collect Statistic Data Goal Tool 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Daniele, M., Giunchiglia, F., Vardi, M.Y.: Improved automata generation for linear temporal logic. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 249–260. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  2. 2.
    Friedgut, E., Kupferman, O., Vardi, M.Y.: Büchi complementation made tighter. In: Wang, F. (ed.) ATVA 2004. LNCS, vol. 3299, pp. 64–78. Springer, Heidelberg (2004)Google Scholar
  3. 3.
    Gastin, P., Oddoux, D.: Fast LTL to Büchi automata translations. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53–65. Springer, Heidelberg (2001)Google Scholar
  4. 4.
    Gastin, P., Oddoux, D.: LTL with past and two-way very-weak alternating automata. In: Rovan, B., Vojtáš, P. (eds.) MFCS 2003. LNCS, vol. 2747, pp. 439–448. Springer, Heidelberg (2003)Google Scholar
  5. 5.
    Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: PSTV 1995, pp. 3–18. Chapman & Hall, Boca Raton (1995)Google Scholar
  6. 6.
    Giannakopoulou, D., Lerda, F.: From states to transitions: Improving translation of LTL formulae to Büchi automata. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol. 2529, pp. 308–326. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  7. 7.
    Hammer, M., Knapp, A., Merz, S.: Truly on-the-fly LTL model checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 191–205. Springer, Heidelberg (2005)Google Scholar
  8. 8.
    Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2003)Google Scholar
  9. 9.
    Kesten, Y., Manna, Z., McGuire, H., Pnueli, A.: A decision algorithm for full propositional temporal logic. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 97–109. Springer, Heidelberg (1993)Google Scholar
  10. 10.
    Kesten, Y., Pnueli, A.: Verification by augmented finitary abstraction. In: Information and Computation, vol. 163, pp. 203–243 (2000)Google Scholar
  11. 11.
    Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM Transactions on Computational Logic 2(3), 408–429 (2001)CrossRefMathSciNetGoogle Scholar
  12. 12.
    Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safty. Springer, Heidelberg (1995)Google Scholar
  13. 13.
    Piterman, N.: From nondeterministic Büchi and Streett automata to deterministic parity automata. In: LICS 2006, pp. 255–264. IEEE Computer Society, Los Alamitos (2006)Google Scholar
  14. 14.
    Sebastiani, R., Tonetta, S.: More deterministic vs. smaller Büchi automata for efficient LTL model checking. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 126–140. Springer, Heidelberg (2003)Google Scholar
  15. 15.
    Somenzi, F., Bloem, R.: Efficient Büchi automata from LTL formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 248–263. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  16. 16.
    The Spec Patterns repository,
  17. 17.
    Tauriainen, H.: Automata and Linear Temporal Logic: Translations with Transition-based Acceptance. PhD thesis, Helsinki University of Technology (2006)Google Scholar
  18. 18.
    Thomas, W.: Complementation of Büchi automata revisited. In: Jewels are Forever, Contributions on Theoretical Computer Science in Honor of Arto Salomaa (1998)Google Scholar
  19. 19.
    Tsai, M.-H., Chan, W.-C., Tsay, Y.-K., Luo, C.-J.: Full PTL to Büchi automata translation for on-the-fly model checking. Manuscript (2007)Google Scholar
  20. 20.
    Tsay, Y.-K., Chen, Y.-F., Tsai, M.-H., Wu, K.-N., Chan, W.-C.: GOAL: A graphical tool for manipulating Büchi automata and temporal formulae. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 466–471. Springer, Heidelberg (2007)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Yih-Kuen Tsay
    • 1
  • Yu-Fang Chen
    • 1
  • Ming-Hsien Tsai
    • 1
  • Wen-Chin Chan
    • 1
  • Chi-Jian Luo
    • 1
  1. 1.Department of Information ManagementNational Taiwan UniversityTaiwan

Personalised recommendations