Abstract
This paper introduces the second generation of GOAL, which is a graphical interactive tool for games, ω-automata, and logics. It is a complete redesign with an extensible architecture, many enhancements to existing functions, and new features. The extensible architecture allows easy integration of third-party plugins. The enhancements provide more automata conversion, complementation, simplification, and testing algorithms, translation of full QPTL formulae, and better automata navigation with more layout algorithms and utility functions. The new features include game solving, manipulation of two-way alternating automata, translation of ACTL formulae and ω-regular expressions, test of language star-freeness, classification of ω-regular languages into the temporal hierarchy of Manna and Pnueli, and a script interpreter.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Abdulla, P.A., Chen, Y.-F., Clemente, L., Holík, L., Hong, C.-D., Mayr, R., Vojnar, T.: Simulation subsumption in Ramsey-based Büchi automata universality and inclusion testing. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 132–147. Springer, Heidelberg (2010)
Althoff, C.S., Thomas, W., Wallmeier, N.: Observations on determinization of Büchi automata. TCS 363(2), 224–233 (2006)
Alur, R., Weiss, G.: RTComposer: a framework for real-time components with scheduling interfaces. In: EMSOFT, pp. 159–168. ACM (2008)
Boker, U., Kupferman, O.: Co-ing Büchi made tight and useful. In: LICS, pp. 245–254. IEEE Computer Society (2009)
Büchi, J.R.: On a decision method in restricted second order arithmetic. In: CLMPS, pp. 1–12. Stanford University Press (1962)
Carton, O., Maceiras, R.: Computing the Rabin index of a parity automaton. Informatique Théorique et Applications 33(6), 495–506 (1999)
Černá, I., Pelánek, R.: Relating hierarchy of temporal properties to model checking. In: Rovan, B., Vojtáš, P. (eds.) MFCS 2003. LNCS, vol. 2747, pp. 318–327. Springer, Heidelberg (2003)
Chatterjee, K., Henzinger, T.A., Jobstmann, B., Singh, R.: QUASY: Quantitative synthesis tool. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 267–271. Springer, Heidelberg (2011)
Cichoń, J., Czubak, A., Jasiński, A.: Minimal Büchi automata for certain classes of LTL formulas. In: DepCos-RELCOMEX, pp. 17–24. IEEE (2009)
Couvreur, J.-M.: On-the-fly verification of linear temporal logic. In: Wing, J.M., Woodcock, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 253–271. Springer, Heidelberg (1999)
Diekert, V., Gastin, P.: First-order definable languages. In: Logic and Automata. Texts in Logic and Games, vol. 2, pp. 261–306. Amsterdam Univ. Press (2008)
Etessami, K., Wilke, T., Schuller, R.A.: Fair simulation relations, parity games, and state space reduction for Büchi automata. SICOMP 34(5), 1159–1175 (2005)
Friedmann, O., Lange, M.: Solving parity games in practice. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 182–196. Springer, Heidelberg (2009)
Gastin, P., Oddoux, D.: Fast LTL to Büchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53–65. Springer, Heidelberg (2001)
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)
Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: PSTV, pp. 3–18. Chapman & Hall (1995)
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)
Grumberg, O., Long, D.E.: Model checking and modular verification. TOPLAS 16(3), 843–871 (1994)
Gurumurthy, S., Bloem, R., Somenzi, F.: Fair simulation minimization. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 610–624. Springer, Heidelberg (2002)
Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley (September 2003)
IEEE standard for property specification language (PSL). IEEE Std 1850-2010 (Revision of IEEE Std 1850-2005), 1–182 (2010)
Java Plugin Framework, http://jpf.sourceforge.net
Jurdziński, M.: Small progress measures for solving parity games. In: Reichel, H., Tison, S. (eds.) STACS 2000. LNCS, vol. 1770, pp. 290–301. Springer, Heidelberg (2000)
Jurdziński, M., Paterson, M., Zwick, U.: A deterministic subexponential algorithm for solving parity games. SICOMP 38(4), 1519–1532 (2008)
Kähler, D., Wilke, T.: Complementation, disambiguation, and determinization of Büchi automata unified. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part I. LNCS, vol. 5125, pp. 724–735. Springer, Heidelberg (2008)
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)
Kesten, Y., Pnueli, A.: Verification by augmented finitary abstraction. Information and Computation 163(1), 203–243 (2000)
Kesten, Y., Pnueli, A.: Complete proof system for QPTL. Journal of Logic and Computation 12(5), 701–745 (2002)
Klotz, T., Seßler, N., Straube, B., Fordran, E.: Compositional verification of material handling systems. In: ETFA, pp. 1–8. IEEE (2012)
Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. TOCL 2(3), 408–429 (2001)
Kurshan, R.P.: Complementing deterministic Büchi automata in polynomial time. JCSS 35(1), 59–71 (1987)
Küsters, R.: Memoryless determinacy of parity games. In: Grädel, E., Thomas, W., Wilke, T. (eds.) Automata, Logics, and Infinite Games. LNCS, vol. 2500, pp. 95–106. Springer, Heidelberg (2002)
Landweber, L.H.: Decision problems for omega-automata. Mathematical Systems Theory 3(4), 376–384 (1969)
Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In: PODC, pp. 377–410 (1990)
Mazala, R.: Infinite games. In: Grädel, E., Thomas, W., Wilke, T. (eds.) Automata, Logics, and Infinite Games. LNCS, vol. 2500, pp. 23–38. Springer, Heidelberg (2002)
McNaughton, R.: Infinite games played on finite graphs. Annals of Pure and Applied Logic 65(2), 149–184 (1993)
Muller, D.E., Schupp, P.E.: Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra. TCS 141(1&2), 69–107 (1995)
Peng, H., Mokhtari, Y., Tahar, S.: Environment synthesis for compositional model checking. In: ICCD, pp. 70–75. IEEE Computer Society (2002)
Piterman, N.: From nondeterministic Büchi and Streett automata to deterministic parity automata. LMCS 3(3), paper 5 (2007)
Rodger, S., Finley, T.: JFLAP, http://www.jflap.org/
Safra, S.: On the complexity of ω-automata. In: FOCS, pp. 319–327. IEEE (1988)
Schewe, S.: Solving parity games in big steps. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol. 4855, pp. 449–460. Springer, Heidelberg (2007)
Schewe, S.: Büchi complementation made tight. In: STACS. LIPIcs, vol. 3, pp. 661–672 (2009)
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)
Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for Büchi automata with appplications to temporal logic. TCS 49, 217–237 (1987)
Sohail, S., Somenzi, F.: Safety first: A two-stage algorithm for LTL games. In: FMCAD, pp. 77–84. IEEE (2009)
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)
Thomas, W.: Complementation of Büchi automata revisited. In: Jewels are Forever, pp. 109–120. Springer (1999)
Tsai, M.-H., Chan, W.-C., Tsay, Y.-K., Luo, C.-J.: Incremental translation of full PTL formulae to Büchi automata (manuscript 2013)
Tsai, M.-H., Fogarty, S., Vardi, M.Y., Tsay, Y.-K.: State of Büchi complementation. In: Domaratzki, M., Salomaa, K. (eds.) CIAA 2010. LNCS, vol. 6482, pp. 261–271. Springer, Heidelberg (2011)
Tsay, Y.-K., Chen, Y.-F., Tsai, M.-H., Chan, W.-C., Luo, C.-J.: GOAL extended: Towards a research tool for omega automata and temporal logic. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 346–350. Springer, Heidelberg (2008)
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)
Tsay, Y.-K., Tsai, M.-H., Chang, J.-S., Chang, Y.-W., Liu, C.-S.: Büchi Store: An open repository of ω-automata. STTT 15(2), 109–123 (2013)
Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. TCS 200(1-2), 135–183 (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tsai, MH., Tsay, YK., Hwang, YS. (2013). GOAL for Games, Omega-Automata, and Logics. In: Sharygina, N., Veith, H. (eds) Computer Aided Verification. CAV 2013. Lecture Notes in Computer Science, vol 8044. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39799-8_62
Download citation
DOI: https://doi.org/10.1007/978-3-642-39799-8_62
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39798-1
Online ISBN: 978-3-642-39799-8
eBook Packages: Computer ScienceComputer Science (R0)