One possible direction for future work is to apply the extended translation algorithms to truly on-the-fly model checking, even if past operators are involved. The more recent work [40] that interweaves simplification operations with the on-the-fly states construction seems promising. It will be interesting to see if our techniques can be applied to extend this type of model checking algorithms to handle past operators.
As the experimental results in Chapter 5 showed, the nondeterministic construc-tions Rank and Slice produced many more dead states of complements. One reason is that there are many nondeterministic choices (rank functions in the rank-based approach and decorations in the slice-based approach) but only few of them are cor-rect. While Friedgut et al. proposed tight ranking in [27] to reduce the number of ranking functions for the rank-based approach, we proposed the heuristic of deter-ministic decoration to alleviate this problem for the slice-based approach. However, the improved constructions Rank+A and Slice+ADRM still produced many more dead states compared to SP+ASE in our experiments. There may be other opportunities
to improve the rank-based and the slice-based constructions further.
Consider incremental containment testing, althoug the Safra-Piterman approach already performs better than the Ramsey-based approach, we may expedite the testing procedure with a subsumption relation. This will be challenging because the structure of compact Safra trees is complicated and checking the subsumption relation between two compact Safra trees may consume more time than that it saves.
To further improve B¨uchi Store, we can extend the repository by featured collec-tions such as a collection of both all the two-state B¨uchi automata with two propo-sitions and their shortest equivalent formulae. The challenge of this improvement is that finding a shortest formula equivalent to an automaton is hard. The work in [51]
can construct a QPTL formula equivalent to a specified B¨uchi automaton but quan-tifications are not required for counter-free automata that are actually as expressive as PTL. We can also provide explanatory descriptions other than temporal formu-lae. Such descriptions would be helpful additions for searching and understanding.
A more systematic classification of temporal formulae into the various specification patterns, which cannot be fully automated though, should also be useful.
To improve GOAL, we can implement translation algorithms for IEEE Property Specification Language (PSL) such that GOAL can be more practical for the indus-try. The visualization and manipulation of tree automata would also be interesting.
Besides, there are still many algorithms for automata and temporal logics not avail-able in GOAL. During the implementation of these algorithms, we would get better understanding of the algorithm and may find improvements, whose performance can be verified easily by experiments with the help of GOAL and B¨uchi Store.
Bibliography
[1] P. Abdulla, Y.-F. Chen, L. Clemente, L. Hol´ık, C.-D. Hong, R. Mayr, and T. Vojnar. Simulation subsumption in Ramsey-based B¨uchi automata uni-versality and inclusion testing. In CAV 2010, LNCS 6174, pages 132–147.
Springer, 2010.
[2] P. Abdulla, Y.-F. Chen, L. Clemente, L. Hol´ık, C.-D. Hong, R. Mayr, and T. Vojnar. Advanced Ramsey-based B¨uchi automata inclusion testing. In CONCUR 2011, LNCS 6901, pages 187–202. Springer, 2011.
[3] P. Abdulla, Y.-F. Chen, L. Hol´ık, R. Mayr, and T. Vojnar. When simulation meets antichains. In TACAS 2010, LNCS 6015, pages 158–174. Springer, 2010.
[4] C. Althoff, W. Thomas, and N. Wallmeier. Observations on determinization of B¨uchi automata. TCS, 363(2):224–233, 2006.
[5] A. Ben-Amram and C. Lee. Program termination analysis in polynomial time.
TOPLAS, 29(1), 2007.
[6] U. Boker and O. Kupferman. Co-ing B¨uchi made tight and useful. In LICS 2009, pages 245–254. IEEE Computer Society, 2009.
[7] R. Bryant. Graph-based algorithms for boolean function manipulation. IEEE TC, 35(8):677–691, 1986.
[8] J. B¨uchi. On a decision method in restricted second order arithmetic. In ICLMPS 1960, pages 1–12. Stanford University Press, 1962.
[9] O. Carton and R. Maceiras. Computing the Rabin index of a parity automaton.
ITA, 33(6):495–506, 1999.
[10] I. Cern´a and R. Pel´anek. Relating hierarchy of temporal properties to model checking. In MFCS, LNCS 2747, pages 318–327. Springer, 2003.
[11] K. Chatterjee, T. Henzinger, B. Jobstmann, and A. Radhakrishna. GIST:
A solver for probabilistic games. In CAV 2010, LNCS 6174, pages 665–669.
Springer, 2010.
[12] K. Chatterjee, T. Henzinger, B. Jobstmann, and R. Singh. QUASY: Quanti-tative synthesis tool. In TACAS 2011, LNCS 6605, pages 267–271. Springer, 2011.
[13] J. Cicho´n, A. Czubak, and A. Jasi´nski. Minimal B¨uchi automata for certain classes of LTL formulas. In DepCoS-RELCOMEX, pages 17–24. IEEE, 2009.
[14] E. Clarke, O. Grumberg, and D. Peled. Model Checking. The MIT Press, 2000.
[15] CodeIgniter. http://codeigniter.com/.
[16] J.-M. Couvreur. On-the-fly verification of linear temporal logic. In FM, LNCS 1708, pages 253–271. Springer, 1999.
[17] M. Daniele, F. Giunchiglia, and M. Vardi. Improved automata generation for linear temporal logic. In CAV 1999, LNCS 1633, pages 249–260. Springer, 1999.
[18] M. De Wulf, L. Doyen, T. Henzinger, and J.-F. Raskin. Antichains: A new algorithm for checking universality of finite automata. In CAV, LNCS 4144, pages 17–30. Springer, 2006.
[19] V. Diekert and P. Gastin. First-order definable languages. In Logic and Au-tomata: History and Perspective, TLG 2, pages 261–306. Amsterdam Univer-sity Press, 2008.
[20] L. Doyen and J.-F. Raskin. Improved algorithms for the automata-based approach to model-checking. In TACAS 2007, LNCS 4424, pages 451–465.
Springer, 2007.
[21] L. Doyen and J.-F. Raskin. Antichains for the automata-based approach to model-checking. LMCS, 5(1:5):1–20, 2009.
[22] M. Dwyer, G. Avrunin, and J. Corbett. Patterns in property specifications for finite-state verification. In ICSE 1999, pages 411–420. ACM, 1999.
[23] K. Etessami and G. Holzmann. Optimizing B¨uchi automata. In CONCUR 2000, LNCS 1877, pages 153–167. Springer, 2000.
[24] K. Etessami, T. Wilke, and R. A. Schuller. Fair simulation relations, parity games, and state space reduction for B¨uchi automata. In ICALP 2011, LNCS 2076, pages 694–707. Springer, 2001.
[25] S. Fogarty and M. Vardi. B¨uchi complementation and size-change termination.
In TACAS 2009, LNCS 5505, pages 16–30. Springer, 2009.
[26] S. Fogarty and M. Vardi. Efficient B¨uchi universality checking. In TACAS 2010, LNCS 6015, pages 205–220. Springer, 2010.
[27] E. Friedgut, O. Kupferman, and M. Y. Vardi. B¨uchi complementation made tighter. IJFCS, 17(4):851–868, 2006.
[28] O. Friedmann and M. Lange. Solving parity games in practice. In ATVA 2009, LNCS 5799, pages 182–196. Springer, 2009.
[29] D. Gabbay. The declarative past and imperative future: Executable temporal logic for interactive systems. In TLS 1987, LNCS 398, pages 409–448. Springer, 1987.
[30] D. Gabbay, A. Pnueli, S. Shelah, and J. Stavi. On the temporal analysis of fairness. In POPL 1980, pages 163–173. ACM Press, 1980.
[31] P. Gastin and D. Oddoux. LTL2BA: fast translation from LTL formulae to B¨uchi automata. http:// www.lsv.ens-cachan.fr/~gastin/
[32] P. Gastin and D. Oddoux. Fast LTL to B¨uchi automata translation. In CAV 2001, LNCS 2102, pages 53–65. Springer, 2001.
[33] P. Gastin and D. Oddoux. LTL with past and two-way very-weak alternating automata. In MFCS 2003, LNCS 2747, pages 439–448. Springer, 2003.
[34] R. Gerth, D. Peled, M. Vardi, and P. Wolper. Simple on-the-fly automatic verification of linear temporal logic. In PSTV, pages 3–18. Chapman & Hall, 1995.
[35] D. Giannakopoulou and F. Lerda. From states to transitions: Improving translation of LTL formulae to B¨uchi automata. In FORTE 2002, LNCS 2529, pages 308–326. Springer, 2002.
[36] E. Gr¨adel, W. Thomas, and T. Wilke, editors. Automata, Logics, and Infi-nite Games: A Guide to Current Research [outcome of a Dagstuhl seminar, February 2001], LNCS 2500. Springer, 2002.
[37] O. Grumberg and D. Long. Model checking and modular verification.
TOPLAS, 16(3):843–871, 1994.
[38] S. Gurumurthy, R. Bloem, and F. Somenzi. Fair simulation minimization. In CAV 2002, LNCS 2404, pages 610–624. Springer, 2002.
[39] S. Gurumurthy, O. Kupferman, F. Somenzi, and M. Vardi. On complementing nondeterministic B¨uchi automata. In CHARME 2003, LNCS 2860, pages 96–
110. Springer, 2003.
[40] M. Hammer, A. Knapp, and S. Merz. Truly on-the-fly LTL model checking.
In TACAS 2005, LNCS 3440, pages 191–205, 2005.
[41] M. Henzinger, T. Henzinger, and P. Kopke. Computing simulations on finite and infinite graphs. In FOCS 1995, pages 453–462. IEEE Computer Society, 1995.
[42] G. Holzmann. The SPIN Model Checker: Primer and Reference Manual.
Addison-Wesley, 2003.
[43] Java Plugin Framework. http://jpf.sourceforge.net.
[44] D. Johnson. Finding all the elementary circuits of a directed graph. SICOMP, 4(1):77–84, 1975.
[45] M. Jurdzi´nski. Small progress measures for solving parity games. In STACS 2000, LNCS 1770, pages 290–301. Springer, 2000.
[46] M. Jurdzi´nski, M. Paterson, and U. Zwick. A deterministic subexponential algorithm for solving parity games. SICOMP, 38(4):1519–1532, 2008.
[47] D. K¨ahler and T. Wilke. Complementation, disambiguation, and determiniza-tion of B¨uchi automata unified. In ICALP 2008, LNCS 5125, pages 724–735.
Springer, 2008.
[48] H. Karmarkar and S. Chakraborty. On minimal odd rankings for B¨uchi com-plementation. In ATVA 2009, LNCS 5799, pages 228–243. Springer, 2009.
[49] Y. Kesten, Z. Manna, H. McGuire, and A. Pnueli. A decision algorithm for full propositional temporal logic. In CAV 1993, LNCS 697, pages 97–109.
Springer, 1993.
[50] Y. Kesten and A. Pnueli. Verification by augmented finitary abstraction.
Information and Computation, 163(1):203–243, 2000.
[51] Y. Kesten and A. Pnueli. Complete proof system for QPTL. IJLP, 12(5):701–
745, 2002.
[52] Y. Kesten, A. Pnueli, and L. Raviv. Algorithmic verification of linear temporal logic specifications. In ICALP 1998, LNCS 1443, pages 1–16. Springer, 1998.
[53] V. King, O. Kupferman, and M. Vardi. On the complexity of parity word automata. In FoSSaCS 2001, LNCS 2030, pages 276–286. Springer, 2001.
[54] N. Klarlund. Progress measures for complementation of ω-automata with applications to temporal logic. In FOCS 1991, pages 358–367. IEEE, 1991.
[55] J. Klein and C. Baier. Experiments with deterministic ω-automata for formu-las of linear temporal logic. TCS, 363(2):182–195, 2006.
[56] T. Klotz, N. Seßler, B. Straube, and E. Fordran. Compositional verification of material handling systems. In ETFA 2012, pages 1–8. IEEE, 2012.
[57] O. Kupferman and M. Vardi. Weak alternating automata are not that weak.
TOCL, 2(3):408–429, 2001.
[58] O. Kupferman and M. Vardi. Safraless decision procedures. In FOCS 2005, pages 531–540. IEEE Computer Society, 2005.
[59] R. Kurshan. Complementing deterministic B¨uchi automata in polynomial time. JCSS, 35(1):59–71, 1987.
[60] R. K¨usters. Memoryless determinacy of parity games. In Automata, Logics, and Infinite Games, LNCS 2500, pages 95–106. Springer, 2001.
[61] L. H. Landweber. Decision problems for ω-automata. MST, 3(4):376–384, 1969.
[62] F. Laroussinie, N. Markey, and P. Schnoebelen. Temporal logic with forget-table past. In LICS 2002, pages 383–392. IEEE, 2002.
[63] T. Latvala, A. Biere, K. Heljanko, and T. A. Junttila. Simple is better: Ef-ficient bounded model checking for past LTL. In VMCAI 2005, LNCS 3385, pages 380–395. Springer, 2005.
[64] O. Lichtenstein, A. Pnueli, and L. Zuck. The glory of the past. In Logic of Programs, LNCS 193, pages 196–218. Springer, 1985.
[65] Z. Manna and A. Pnueli. A hierarchy of temporal properties. In PODC 1990, pages 377–410. ACM, 1990.
[66] Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety.
Springer, 1995.
[67] R. Mazala. Infinite games. In Automata, Logics, and Infinite Games, LNCS 2500, pages 23–42. Springer, 2001.
[68] R. McNaughton. Infinite games played on finite graphs. APAL, 65(2):149–184, 1993.
[69] M. Michel. Complementation is more difficult with automata on infinite words.
In CNET, 1988.
[70] D. Muller and P. Schupp. Simulating alternating tree automata by nonde-terministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra. TCS, 141(1&2):69–107, 1995.
[71] K. Namjoshi and R. Trefler. On the completeness of compositional reasoning.
In CAV 2000, LNCS 1855, pages 139–153. Springer, 2000.
[72] H. Peng, Y. Mokhtari, and S. Tahar. Environment synthesis for compositional model checking. In ICCD 2002, pages 70–75. IEEE, 2002.
[73] PHP/Java Bridge. http://php-java-bridge. sourceforge.net/.
[74] N. Piterman. From nondeterministic B¨uchi and Streett automata to deter-ministic parity automata. LMCS, 3(3), 2007.
[75] M. Rabin and D. Scott. Finite automata and their decision problems. IBM JRD, 3:115–125, 1959.
[76] S. Rodger and T. Finley. JFLAP. http://www.jflap.org/.
[77] S. Safra. On the complexity of ω-automata. In FOCS 1988, pages 319–327.
IEEE, 1988.
[78] S. Schewe. Solving parity games in big steps. In FSTTCS 2007, LNCS 4855, pages 449–460. Springer, 2007.
[79] S. Schewe. B¨uchi complementation made tight. In STACS 2009, LIPIcs 3, pages 661–672. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2009.
[80] S. Schewe. Tighter bounds for the determinisation of B¨uchi automata. In FOSSACS 2009, LNCS 5504, pages 167–181. Springer, 2009.
[81] R. Sebastiani and S. Tonetta. “More deterministic” vs. “smaller” B¨uchi au-tomata for efficient LTL model checking. In CHARME 2003, LNCS 2860, pages 126–140. Springer, 2003.
[82] A. Sistla. Theoretical Issues in the Design and Verification of Distributed Systems. PhD thesis, Harvard, 1983.
[83] A. Sistla, M. Vardi, and P. Wolper. The complementation problem for b¨uchi automata with appplications to temporal logic. TCS, 49:217–237, 1987.
[84] S. Sohail and F. Somenzi. Safety first: A two-stage algorithm for LTL games.
In FMCAD 2009, pages 77–84. IEEE, 2009.
[85] S. Sohail, F. Somenzi, and K. Ravi. A hybrid algorithm for LTL games. In VMCAI 2008, LNCS 4905, pages 309–323. Springer, 2008.
[86] F. Somenzi and R. Bloem. Efficient B¨uchi automata from LTL formulae. In CAV 2000, LNCS 1855, pages 248–263. Springer, 2000.
[87] The Spec Patterns repository. http://patterns.projects.cis.ksu.edu/.
[88] H. Tauriainen and K. Heljanko. Testing LTL formula translation into B¨uchi automata. STTT, 4(1):57–70, 2002.
[89] W. Thomas. Complementation of B¨uchi automata revisited. In Jewels are Forever, pages 109–120. Springer, 1999.
[90] Tomcat. http://tomcat.apache.org/.
[91] M.-H. Tsai, S. Fogarty, M. Vardi, and Y.-K. Tsay. State of B¨uchi complemen-tation. In CIAA 2010, LNCS 6482, pages 261–271. Springer, 2010.
[92] M.-H. Tsai, Y.-K. Tsay, and Y.-S. Hwang. GOAL for games, omega-automata, and logics. In CAV 2013, LNCS 8044. Springer, 2013.
[93] Y.-K. Tsay. Compositional verification in linear-time temporal logic. In FoS-SaCS 2000, LNCS 1784, pages 344–358. Springer, 2000.
[94] Y.-K. Tsay, Y.-F. Chen, M.-H. Tsai, W.-C. Chan, and C.-J. Luo. GOAL extended: Towards a research tool for omega automata and temporal logic. In TACAS 2008, LNCS 4963, pages 346–350, 2008.
[95] Y.-K. Tsay, Y.-F. Chen, M.-H. Tsai, K.-N. Wu, and W.-C. Chan. GOAL: A graphical tool for manipulating B¨uchi automata and temporal formulae. In TACAS 2007, LNCS 4424, pages 466–471, 2007.
[96] Y.-K. Tsay, M.-H. Tsai, J.-S. Chang, and Y.-W. Chang. B¨uchi Store: An open repository of B¨uchi automata. In TACAS 2011, LNCS 6605, pages 262–266.
Springer, 2011.
[97] Y.-K. Tsay, M.-H. Tsai, J.-S. Chang, Y.-W. Chang, and C.-S. Liu. B¨uchi Store: An open repository of ω-automata. STTT, 15(2):109–123, 2013.
[98] M. Vardi. An automata-theoretic approach to linear temporal logic. In Logics for Concurrency: Structure versus Automata, LNCS 1043, pages 238–266.
Springer, 1996.
[99] M. Vardi. Automata-theoretic model checking revisited. In VMCAI 2007, LNCS 4349, pages 137–150. Springer, 2007.
[100] M. Vardi. The B¨uchi complementation saga. In STACS 2007, LNCS 4393, pages 12–22. Springer, 2007.
[101] M. Vardi and T. Wilke. Automata: from logics to algorithms. In Logic and Automata: History and Perspective, TLG 2, pages 629–736. Amsterdam Uni-versity Press, 2007.
[102] M. Vardi and P. Wolper. An automata-theoretic approach to automatic pro-gram verification. In LICS 1986, pages 322–331, Cambridge, 1986.
[103] Q. Yan. Lower bounds for complementation of omega-automata via the full automata technique. LMCS, 4(1), 2008.
[104] W. Zielonka. Infinite games on finitely coloured graphs with applications to automata on infinite trees. TCS, 200(1-2):135–183, 1998.