Advertisement

Learning Büchi Automata and Its Applications

  • Yong Li
  • Andrea TurriniEmail author
  • Yu-Fang Chen
  • Lijun Zhang
Chapter
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11430)

Abstract

In this work, we review an algorithm that learns a Büchi automaton from a teacher who knows an \(\omega \)-regular language; the algorithm is based on learning a formalism named family of DFAs (FDFAs) recently proposed by Angluin and Fisman. We introduce the learning algorithm by learning the simple \(\omega \)-regular language \((ab)^{\omega }\): besides giving the readers an overview of the algorithm, it guides them on how the algorithm works step by step. Further, we demonstrate how the learning algorithm can be exploited in classical automata operations such as complementation checking and in the context of termination analysis.

Notes

Acknowledgement

This work has been supported by the National Natural Science Foundation of China (Grant Nos. 61532019, 61761136011), and by the CAP project GZ1023.

References

  1. 1.
  2. 2.
    Aarts, F., Vaandrager, F.W.: Learning I/O automata. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 71–85. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-15375-4_6CrossRefGoogle Scholar
  3. 3.
    Abdulla, P.A., et al.: 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).  https://doi.org/10.1007/978-3-642-14295-6_14CrossRefGoogle Scholar
  4. 4.
    Abdulla, P.A., et al.: Advanced ramsey-based Büchi automata inclusion testing. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 187–202. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-23217-6_13CrossRefGoogle Scholar
  5. 5.
    Allred, J.D., Ultes-Nitsche, U.: A simple and optimal complementation algorithm for Büchi automata. In: LICS, pp. 46–55 (2018)Google Scholar
  6. 6.
    Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2(3), 117–126 (1987)CrossRefGoogle Scholar
  7. 7.
    Alur, R., Černỳ, P., Madhusudan, P., Nam, W.: Synthesis of interface specifications for Java classes. In: POPL, pp. 98–109 (2005)CrossRefGoogle Scholar
  8. 8.
    Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput. 75(2), 87–106 (1987)MathSciNetCrossRefGoogle Scholar
  9. 9.
    Angluin, D., Boker, U., Fisman, D.: Families of DFAs as acceptors of omega-regular languages. In: MFCS, pp. 11:1–11:14 (2016)Google Scholar
  10. 10.
    Angluin, D., Eisenstat, S., Fisman, D.: Learning regular languages via alternating automata. In: IJCAI, pp. 3308–3314 (2015)Google Scholar
  11. 11.
    Angluin, D., Fisman, D.: Learning regular omega languages. Theor. Comput. Sci. 650, 57–72 (2016)MathSciNetCrossRefGoogle Scholar
  12. 12.
    Arnold, A.: A syntactic congruence for rational \(\omega \)-languages. Theor. Comput. Sci. 39, 333–335 (1985)MathSciNetCrossRefGoogle Scholar
  13. 13.
    Babiak, T., et al.: The hanoi omega-automata format. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 479–486. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-21690-4_31CrossRefGoogle Scholar
  14. 14.
    Ben-Amram, A.M.: Size-change termination, monotonicity constraints and ranking functions. Log. Methods Comput. Sci. 6 (2010)Google Scholar
  15. 15.
    Ben-Amram, A.M., Genaim, S.: On the linear ranking problem for integer linear-constraint loops. In: POPL, pp. 51–62. ACM, New York (2013)Google Scholar
  16. 16.
    Ben-Amram, A.M., Genaim, S.: Complexity of bradley-manna-sipma lexicographic ranking functions. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 304–321. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-21668-3_18CrossRefGoogle Scholar
  17. 17.
    Ben-Amram, A.M., Genaim, S.: On multiphase-linear ranking functions. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 601–620. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-63390-9_32CrossRefGoogle Scholar
  18. 18.
    Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: TACAS, pp. 193–207 (1999)Google Scholar
  19. 19.
    Blahoudek, F., Heizmann, M., Schewe, S., Strejček, J., Tsai, M.-H.: Complementing semi-deterministic Büchi automata. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 770–787. Springer, Heidelberg (2016).  https://doi.org/10.1007/978-3-662-49674-9_49CrossRefGoogle Scholar
  20. 20.
    Bollig, B., Habermehl, P., Kern, C., Leucker, M.: Angluin-style learning of NFA. In: IJCAI, pp. 1004–1009 (2009)Google Scholar
  21. 21.
    Bollig, B., Katoen, J.-P., Kern, C., Leucker, M., Neider, D., Piegdon, D.R.: libalf: the automata learning framework. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 360–364. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-14295-6_32CrossRefGoogle Scholar
  22. 22.
    Borralleras, C., et al.: Proving termination through conditional termination. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 99–117. Springer, Heidelberg (2017).  https://doi.org/10.1007/978-3-662-54577-5_6CrossRefGoogle Scholar
  23. 23.
    Bradley, A.R., Manna, Z., Sipma, H.B.: Linear ranking with reachability. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 491–504. Springer, Heidelberg (2005).  https://doi.org/10.1007/11513988_48CrossRefGoogle Scholar
  24. 24.
    Breuers, S., Löding, C., Olschewski, J.: Improved ramsey-based Büchi complementation. In: Birkedal, L. (ed.) FoSSaCS 2012. LNCS, vol. 7213, pp. 150–164. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-28729-9_10CrossRefGoogle Scholar
  25. 25.
    Büchi, J.R.: On a decision method in restricted second order arithmetic. In: International Congress on Logic, Methodology and Philosophy of Science, pp. 1–11 (1962)Google Scholar
  26. 26.
    Calbrix, H., Nivat, M., Podelski, A.: Ultimately periodic words of rational \(\omega \)-languages. In: Brookes, S., Main, M., Melton, A., Mislove, M., Schmidt, D. (eds.) MFPS 1993. LNCS, vol. 802, pp. 554–566. Springer, Heidelberg (1994).  https://doi.org/10.1007/3-540-58027-1_27CrossRefzbMATHGoogle Scholar
  27. 27.
    Chapman, M., Chockler, H., Kesseli, P., Kroening, D., Strichman, O., Tautschnig, M.: Learning the language of error. In: ATVA, pp. 114–130 (2015)CrossRefGoogle Scholar
  28. 28.
    Chen, Y.F., et al.: Advanced automata-based algorithms for program termination checking. In: PLDI, pp. 135–150 (2018)Google Scholar
  29. 29.
    Chen, Y.F., et al.: PAC learning-based verification and model synthesis. In: ICSE, pp. 714–724 (2016)Google Scholar
  30. 30.
    Choueka, Y.: Theories of automata on \(\omega \)-tapes: a simplified approach. J. Comput. Syst. Sci. 8(2), 117–141 (1974)MathSciNetCrossRefGoogle Scholar
  31. 31.
    Clarke, E.M.: Model checking – my 27-year quest to overcome the state explosion problem. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 182–182. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-89439-1_13CrossRefGoogle Scholar
  32. 32.
    Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.): Handbook of Model Checking. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-10575-8CrossRefzbMATHGoogle Scholar
  33. 33.
    Clemente, L., Mayr, R.: Advanced automata minimization. In: Proceedings of POPL 2013, pp. 63–74. ACM (2013)Google Scholar
  34. 34.
    Cobleigh, J.M., Giannakopoulou, D., PĂsĂreanu, C.S.: Learning assumptions for compositional verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 331–346. Springer, Heidelberg (2003).  https://doi.org/10.1007/3-540-36577-X_24CrossRefzbMATHGoogle Scholar
  35. 35.
    Cook, B., Kroening, D., Rümmer, P., Wintersteiger, C.M.: Ranking function synthesis for bit-vector relations. Formal Methods Syst. Des. 43(1), 93–120 (2013)CrossRefGoogle Scholar
  36. 36.
    Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: PLDI, pp. 415–426. ACM, New York (2006)CrossRefGoogle Scholar
  37. 37.
    Cook, B., Podelski, A., Rybalchenko, A.: Proving program termination. Commun. ACM 54(5), 88–98 (2011)CrossRefGoogle Scholar
  38. 38.
    Cook, B., See, A., Zuleger, F.: Ramsey vs. lexicographic termination proving. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 47–61. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-36742-7_4CrossRefGoogle Scholar
  39. 39.
    Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, É., Xu, L.: Spot 2.0 — a framework for LTL and \(\omega \)-automata manipulation. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 122–129. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-46520-3_8CrossRefGoogle Scholar
  40. 40.
    Emerson, E.A., Lei, C.: Modalities for model checking: branching time strikes back. In: POPL, pp. 84–96 (1985)Google Scholar
  41. 41.
    Emerson, E.A., Lei, C.: Modalities for model checking: branching time logic strikes back. Sci. Comput. Program. 8(3), 275–306 (1987)MathSciNetCrossRefGoogle Scholar
  42. 42.
    Farzan, A., Chen, Y.-F., Clarke, E.M., Tsay, Y.-K., Wang, B.-Y.: Extending automated compositional verification to the full class of omega-regular languages. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 2–17. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-78800-3_2CrossRefzbMATHGoogle Scholar
  43. 43.
    Feng, L., Kwiatkowska, M., Parker, D.: Compositional verification of probabilistic systems using learning. In: QEST, pp. 133–142 (2010)Google Scholar
  44. 44.
    Fogarty, S., Kupferman, O., Vardi, M.Y., Wilke, T.: Profile trees for Büchi word automata, with application to determinization. Inf. Comput. 245, 136–151 (2015)CrossRefGoogle Scholar
  45. 45.
    Fogarty, S., Kupferman, O., Wilke, T., Vardi, M.Y.: Unifying Büchi complementation constructions. Log. Methods Comput. Sci. 9(1) (2013)Google Scholar
  46. 46.
    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).  https://doi.org/10.1007/978-3-540-30476-0_10CrossRefGoogle Scholar
  47. 47.
    Ganty, P., Genaim, S.: Proving termination starting from the end. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 397–412. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-39799-8_27CrossRefGoogle Scholar
  48. 48.
    Giesl, J., et al.: Analyzing program termination and complexity automatically with AProVe. J. Autom. Reason. 58, 3–31 (2017)MathSciNetCrossRefGoogle Scholar
  49. 49.
    Grädel, E., Thomas, W., Wilke, T. (eds.): Automata Logics, and Infinite Games. LNCS, vol. 2500. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-36387-4CrossRefzbMATHGoogle Scholar
  50. 50.
    Grinchtein, O., Jonsson, B., Leucker, M.: Learning of event-recording automata. Theor. Comput. Sci. 411(47), 4029–4054 (2010)MathSciNetCrossRefGoogle Scholar
  51. 51.
    Gurumurthy, S., Kupferman, O., Somenzi, F., Vardi, M.Y.: On complementing nondeterministic Büchi automata. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 96–110. Springer, Heidelberg (2003).  https://doi.org/10.1007/978-3-540-39724-3_10CrossRefGoogle Scholar
  52. 52.
    Harris, W.R., Lal, A., Nori, A.V., Rajamani, S.K.: Alternation for termination. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 304–319. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-15769-1_19CrossRefGoogle Scholar
  53. 53.
    van Heerdt, G., Sammartino, M., Silva, A.: CALF: categorical automata learning framework. In: CSL, pp. 29:1–29:24 (2017)Google Scholar
  54. 54.
    Heizmann, M., Hoenicke, J., Leike, J., Podelski, A.: Linear ranking for linear lasso programs. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 365–380. Springer, Cham (2013).  https://doi.org/10.1007/978-3-319-02444-8_26CrossRefzbMATHGoogle Scholar
  55. 55.
    Heizmann, M., Hoenicke, J., Podelski, A.: Termination analysis by learning terminating programs. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 797–813. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-08867-9_53CrossRefGoogle Scholar
  56. 56.
    Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley Longman Publishing Co., Inc., Boston (2006)Google Scholar
  57. 57.
    Howar, F., Steffen, B., Jonsson, B., Cassel, S.: Inferring canonical register automata. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 251–266. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-27940-9_17CrossRefGoogle Scholar
  58. 58.
    Isberner, M., Howar, F., Steffen, B.: Learning register automata: from languages to program structures. Mach. Learn. 96(1–2), 65–98 (2014)MathSciNetCrossRefGoogle Scholar
  59. 59.
    Isberner, M., Howar, F., Steffen, B.: The TTT algorithm: a redundancy-free approach to active automata learning. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 307–322. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-11164-3_26CrossRefGoogle Scholar
  60. 60.
    Isberner, M., Howar, F., Steffen, B.: The open-source LearnLib. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 487–495. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-21690-4_32CrossRefGoogle Scholar
  61. 61.
    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. LNCS, vol. 5125, pp. 724–735. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-70575-8_59CrossRefzbMATHGoogle Scholar
  62. 62.
    Kaminski, M.: A classification of \(\omega \)-regular languages. Theor. Comput. Sci. 36, 217–229 (1985)MathSciNetCrossRefGoogle Scholar
  63. 63.
    Kearns, M.J., Vazirani, U.V.: An Introduction to Computational Learning Theory. MIT Press, Cambridge (1994)CrossRefGoogle Scholar
  64. 64.
    Kroening, D., Sharygina, N., Tsitovich, A., Wintersteiger, C.M.: Termination analysis with compositional transition invariants. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 89–103. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-14295-6_9CrossRefGoogle Scholar
  65. 65.
    Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM Trans. Comput. Logic 2(3), 408–429 (2001)MathSciNetCrossRefGoogle Scholar
  66. 66.
    Kurshan, R.P.: Complementing deterministic Büchi automata in polynomial time. J. Comput. Syst. Sci. 35(1), 59–71 (1987)MathSciNetCrossRefGoogle Scholar
  67. 67.
    Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes: The Automata-theoretic Approach. Princeton University Press, Princeton (1994)zbMATHGoogle Scholar
  68. 68.
    Landweber, L.H.: Decision problems for \(\omega \)-automata. Math. Syst. Theory 3(4), 376–384 (1969)MathSciNetCrossRefGoogle Scholar
  69. 69.
    Le, T.C., Qin, S., Chin, W.: Termination and non-termination specification inference. In: PLDI, pp. 489–498. ACM, New York (2015)CrossRefGoogle Scholar
  70. 70.
    Lee, W., Wang, B.-Y., Yi, K.: Termination analysis with algorithmic learning. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 88–104. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-31424-7_12CrossRefGoogle Scholar
  71. 71.
    Leike, J., Heizmann, M.: Ranking templates for linear loops. Log. Methods Comput. Sci. 11(1) (2015)Google Scholar
  72. 72.
    Li, Y., Chen, Y., Zhang, L., Liu, D.: A novel learning algorithm for Büchi automata based on family of DFAs and classification trees. CoRR abs/1610.07380 (2016). http://arxiv.org/abs/1610.07380
  73. 73.
    Li, Y., Chen, Y.-F., Zhang, L., Liu, D.: A novel learning algorithm for Büchi automata based on family of DFAs and classification trees. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 208–226. Springer, Heidelberg (2017).  https://doi.org/10.1007/978-3-662-54577-5_12CrossRefGoogle Scholar
  74. 74.
    Li, Y., Turrini, A., Zhang, L., Schewe, S.: Learning to complement Büchi automata. In: VMCAI, vol. 10747, pp. 313–335 (2018)Google Scholar
  75. 75.
    Lin, S.W., André, E., Liu, Y., Sun, J., Dong, J.S.: Learning assumptions for compositional verification of timed systems. IEEE Trans. Softw. Eng. 40(2), 137–153 (2014)CrossRefGoogle Scholar
  76. 76.
    Maler, O., Pnueli, A.: On the learnability of infinitary regular sets. Inf. Comput. 118(2), 316–326 (1995)MathSciNetCrossRefGoogle Scholar
  77. 77.
    Maler, O., Staiger, L.: On syntactic congruences for omega-languages. In: STACS, pp. 586–594 (1993)Google Scholar
  78. 78.
    McMillan, K.L.: Symbolic Model Checking. Kluwer (1993)Google Scholar
  79. 79.
    Moerman, J., Sammartino, M., Silva, A., Klin, B., Szynwelski, M.: Learning nominal automata. In: POPL, pp. 613–625 (2017)Google Scholar
  80. 80.
    Padon, O., Hoenicke, J., Losa, G., Podelski, A., Sagiv, M., Shoham, S.: Reducing liveness to safety in first-order logic. ACM Program. Lang. 2(POPL), 26:1–26:33 (2018)Google Scholar
  81. 81.
    Peled, D., Vardi, M.Y., Yannakakis, M.: Black box checking. J. Automata Lang. Comb. 7(2), 225–246 (2002)MathSciNetzbMATHGoogle Scholar
  82. 82.
    Piterman, N.: From nondeterministic Büchi and streett automata to deterministic parity automata. In: LICS, pp. 255–264 (2006)Google Scholar
  83. 83.
    Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 239–251. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-24622-0_20CrossRefGoogle Scholar
  84. 84.
    Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS, pp. 32–41. IEEE Computer Society, Washington, DC (2004)Google Scholar
  85. 85.
    Podelski, A., Rybalchenko, A., Wies, T.: Heap assumptions on demand. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 314–327. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-70545-1_31CrossRefGoogle Scholar
  86. 86.
    Popeea, C., Rybalchenko, A.: Compositional termination proofs for multi-threaded programs. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 237–251. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-28756-5_17CrossRefzbMATHGoogle Scholar
  87. 87.
    Rivest, R.L., Schapire, R.E.: Inference of finite automata using homing sequences. In: STOC, pp. 411–420 (1989)Google Scholar
  88. 88.
    de Ruiter, J., Poll, E.: Protocol state fuzzing of TLS implementations. In: USENIX, pp. 193–206 (2015)Google Scholar
  89. 89.
    Safra, S.: On the complexity of omega-automata. In: FOCS, pp. 319–327 (1988)Google Scholar
  90. 90.
    Schewe, S.: Büchi complementation made tight. In: STACS. LIPIcs, vol. 3, pp. 661–672 (2009)Google Scholar
  91. 91.
    Schewe, S.: Tighter bounds for the determinisation of Büchi automata. In: de Alfaro, L. (ed.) FoSSaCS 2009. LNCS, vol. 5504, pp. 167–181. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-00596-1_13CrossRefzbMATHGoogle Scholar
  92. 92.
    Sickert, S., Esparza, J., Jaax, S., Křetínský, J.: Limit-deterministic Büchi automata for linear temporal logic. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 312–332. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-41540-6_17CrossRefGoogle Scholar
  93. 93.
    Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for Büchi automata with appplications to temporal logic. Theor. Comput. Sci. 49, 217–237 (1987)CrossRefGoogle Scholar
  94. 94.
    Staiger, L.: Research in the theory of omega-languages. Elektronische Informationsverarbeitung und Kybernetik 23(8/9), 415–439 (1987)MathSciNetzbMATHGoogle Scholar
  95. 95.
    Ströder, T., et al.: Automatically proving termination and memory safety for programs with pointer arithmetic. J. Autom. Reason. 58, 33–65 (2017)MathSciNetCrossRefGoogle Scholar
  96. 96.
    Thomas, W.: Automata on infinite objects. In: Handbook of Theoretical Computer Science, vol. B: Formal Models and Sematics, chap. 4, pp. 133–192 (1990)Google Scholar
  97. 97.
    Thomas, W.: Languages, automata, and logic. In: Rozenberg, G., Salomaa, A. (eds.) Handbook of Formal Languages, pp. 389–455. Springer, Heidelberg (1997).  https://doi.org/10.1007/978-3-642-59126-6_7CrossRefGoogle Scholar
  98. 98.
    Tsai, M., Fogarty, S., Vardi, M.Y., Tsay, Y.: State of Büchi complementation. Log. Methods Comput. Sci. 10(4) (2014)Google Scholar
  99. 99.
    Tsai, M.-H., Tsay, Y.-K., Hwang, Y.-S.: GOAL for games, omega-automata, and logics. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 883–889. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-39799-8_62CrossRefGoogle Scholar
  100. 100.
    Tsay, Y.-K., Tsai, M.-H., Chang, J.-S., Chang, Y.-W.: Büchi store: an open repository of Büchi automata. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 262–266. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-19835-9_23CrossRefGoogle Scholar
  101. 101.
    Urban, C., Gurfinkel, A., Kahsai, T.: Synthesizing ranking functions from bits and pieces. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 54–70. Springer, Heidelberg (2016).  https://doi.org/10.1007/978-3-662-49674-9_4CrossRefGoogle Scholar
  102. 102.
    Urban, C., Miné, A.: An abstract domain to infer ordinal-valued ranking functions. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 412–431. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-642-54833-8_22CrossRefGoogle Scholar
  103. 103.
    Vaandrager, F.: Model learning. Commun. ACM 60(2), 86–95 (2017)CrossRefGoogle Scholar
  104. 104.
    Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol. 1043, pp. 238–266. Springer, Heidelberg (1996).  https://doi.org/10.1007/3-540-60915-6_6CrossRefGoogle Scholar
  105. 105.
    Vardi, M.Y.: The Büchi complementation saga. In: Thomas, W., Weil, P. (eds.) STACS 2007. LNCS, vol. 4393, pp. 12–22. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-70918-3_2CrossRefGoogle Scholar
  106. 106.
    Vardi, M.Y., Wilke, T.: Automata: from logics to algorithms. In: Logic and Automata: History and Perspectives [in Honor of Wolfgang Thomas], pp. 629–736 (2008)Google Scholar
  107. 107.
    Wang, F., Wu, J.-H., Huang, C.-H., Chang, K.-H.: Evolving a test oracle in black-box testing. In: Giannakopoulou, D., Orejas, F. (eds.) FASE 2011. LNCS, vol. 6603, pp. 310–325. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-19811-3_22CrossRefGoogle Scholar
  108. 108.
    Yan, Q.: Lower bounds for complementation of \(\omega \)-automata via the full automata technique. Log. Methods Comput. Sci. 4(1:5) (2008)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.State Key Laboratory of Computer Science, Institute of SoftwareChinese Academy of SciencesBeijingChina
  2. 2.University of Chinese Academy of SciencesBeijingChina
  3. 3.Institute of Intelligent SoftwareGuangzhouChina
  4. 4.Institute of Information ScienceAcademia SinicaTaipeiTaiwan

Personalised recommendations