zbMATH — the first resource for mathematics

Efficient reduction of nondeterministic automata with application to language inclusion testing. (English) Zbl 07029311
Summary: We present efficient algorithms to reduce the size of nondeterministic Büchi word automata (NBA) and nondeterministic finite word automata (NFA), while retaining their languages. Additionally, we describe methods to solve PSPACE-complete automata problems like language universality, equivalence, and inclusion for much larger instances than was previously possible (\(\geq 1000\) states instead of 10–100). This can be used to scale up applications of automata in formal verification tools and decision procedures for logical theories.
The algorithms are based on new techniques for removing transitions (pruning) and adding transitions (saturation), as well as extensions of classic quotienting of the state space. These techniques use criteria based on combinations of backward and forward trace inclusions and simulation relations. Since trace inclusion relations are themselves PSPACE-complete, we introduce lookahead simulations as good polynomial time computable approximations thereof.
Extensive experiments show that the average-case time complexity of our algorithms scales slightly above quadratically. (The space complexity is worst-case quadratic.) The size reduction of the automata depends very much on the class of instances, but our algorithm consistently reduces the size far more than all previous techniques. We tested our algorithms on NBA derived from LTL-formulae, NBA derived from mutual exclusion protocols and many classes of random NBA and NFA, and compared their performance to the well-known automata tool GOAL.
Reviewer: Reviewer (Berlin)
03B70 Logic in computer science
68 Computer science
Full Text: arXiv
[1] Spot: a platform for LTL and ω-automata manipulation. https://spot.lrde.epita.fr/. · Zbl 1004.03047
[2] P. A. 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 Universality and Inclusion Testing. In T. Touili, B. Cook, and P. Jackson, editors, Computer Aided Verification, volume 6174 of LNCS, pages 132–147, 2010.
[3] P. A. 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 J.-P. Katoen and B. K¨onig, editors, International Conference on Concurrency Theory, volume 6901 of LNCS, pages 187–202, Sept. 2011. · Zbl 1334.68084
[4] P. A. Abdulla, Y.-F. Chen, L. Hol´ık, R. Mayr, and T. Vojnar. When simulation meets antichains. In TACAS, volume 6015 of LNCS, pages 158–174, 2010. · Zbl 1284.68337
[5] P. A. Abdulla, Y.-F. Chen, L. Hol´ık, and T. Vojnar. Mediating for reduction (on minimizing alternating B¨uchi automata). In FSTTCS, volume 4 of LIPIcs, pages 1–12. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2009. · Zbl 1426.68283
[6] P. A. Abdulla, Y.-F. Chen, L. Hol´ık, and T. Vojnar. Mediating for reduction (on minimizing alternating B¨uchi automata). Theor. Comput. Sci., 552(0):26–43, 2014. · Zbl 1355.68105
[7] R. Almeida. Efficient algorithms for hard problems in nondeterministic tree automata. PhD thesis, School of Informatics. University of Edinburgh, UK, 2017. http://hdl.handle.net/1842/28794. · Zbl 1448.68456
[8] R. Almeida, L. Hol´ık, and R. Mayr. Reduction of nondeterministic tree automata. In Proc. of TACAS 2016, volume 9636 of LNCS, 2016. arXiv 1512.08823. · Zbl 1407.03072
[9] T. Babiak, M. Kˇret´ınsk´y, V. ˇReh´ak, and J. Strejˇcek. LTL to B¨uchi automata translation: Fast and more deterministic. In Proceedings of TACAS 2012, volume 7214 of LNCS, pages 95–109. Springer-Verlag, 2012. · Zbl 06944937
[10] F. Blahoudek, A. Duret-Lutz, M. Kˇret´ınsk´y, and J. Strejˇcek. Is there a best B¨uchi automaton for explicit model checking? In In Proc. of SPIN’14, SPIN 2014, pages 68–76, New York, NY, USA, 2014. ACM. · Zbl 1425.03027
[11] F. Bonchi and D. Pous. Checking NFA equivalence with bisimulations up to congruence. In Principles of Programming Languages (POPL), Rome, Italy. ACM, Jan. 2013. · Zbl 1285.68058
[12] N. Bousquet and C. L¨oding. Equivalence and inclusion problem for strongly unambiguous B¨uchi automata. In A.-H. Dediu, H. Fernau, and C. Mart´ın-Vide, editors, In Proc. of LATA’10, pages 118–129, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg. · Zbl 1284.68340
[13] J. Brzozowski and N. Santean. Predictable semiautomata. Theor. Comput. Sci., 410(35):3236–3249, 2009. · Zbl 1216.03064
[14] D. Bustan and O. Grumberg. Simulation-based minimization. ACM Trans. Comput. Logic, 4:181–206, April 2003. · Zbl 1284.68516
[15] Y.-F. Chen and R. Mayr. RABIT/Reduce: Tools for language inclusion testing and reduction of nondeterministic B¨uchi automata and NFA. http://www.languageinclusion.org/doku.php?id=tools. · Zbl 1428.68040
[16] L. Clemente. B¨uchi Automata Can Have Smaller Quotients. In L. Aceto, M. Henzinger, and J. Sgall, editors, ICALP, volume 6756 of LNCS, pages 258–270. Springer-Verlag, 2011. · Zbl 1306.68155
[17] L. Clemente. Generalized Simulation Relations with Applications in Automata Theory. PhD thesis, University of Edinburgh, 2012. · Zbl 1172.68538
[18] L. Clemente and R. Mayr. Multipebble Simulations for Alternating Automata - (Extended Abstract). In International Conference on Concurrency Theory, volume 6269 of LNCS, pages 297–312. Springer-Verlag, 2010. · Zbl 1287.68094
[19] L. Clemente and R. Mayr. Advanced automata minimization. In 40th Annual ACM SIGPLAN-SIGACT · Zbl 1395.03028
[20] L. Clemente and R. Mayr. Efficient reduction of nondeterministic automata with application to language inclusion testing. arXiv, 1711.09946, 2018. https://arxiv.org/abs/1711.09946. · Zbl 1257.03086
[21] J.-M. Couvreur. On-the-fly verification of linear temporal logic. In Proceedings of the Wold Congress on Formal Methods in the Development of Computing Systems-Volume I - Volume I, FM ’99, pages 253–271, London, UK, UK, 1999. Springer-Verlag. · Zbl 1089.03507
[22] D. L. Dill, A. J. Hu, and H. Wont-Toi. Checking for Language Inclusion Using Simulation Preorders. In Computer Aided Verification, volume 575 of LNCS. Springer-Verlag, 1991. · Zbl 1423.68406
[23] L. Doyen and J.-F. Raskin. Antichains Algorithms for Finite Automata. In Tools and Algorithms for the Construction and Analysis of Systems, volume 6015 of LNCS, pages 2–22. Springer-Verlag, 2010. · Zbl 1284.68348
[24] K. Etessami. A Hierarchy of Polynomial-Time Computable Simulations for Automata. In International Conference on Concurrency Theory, volume 2421 of LNCS, pages 131–144. Springer-Verlag, 2002. · Zbl 0625.90056
[25] K. Etessami and G. Holzmann. Optimizing B¨uchi Automata. In International Conference on Concurrency Theory, volume 1877 of LNCS, pages 153–168. Springer-Verlag, 2000. · Zbl 1327.68129
[26] K. Etessami, T. Wilke, and R. A. Schuller. Fair Simulation Relations, Parity Games, and State Space Reduction for B¨uchi Automata. SIAM J. Comput., 34(5):1159–1175, 2005. · Zbl 0938.68825
[27] S. Fogarty, O. Kupferman, M. Y. Vardi, and T. Wilke. Unifying B¨uchi Complementation Constructions. In M. Bezem, editor, Computer Science Logic, volume 12 of LIPIcs, pages 248–263. Schloss Dagstuhl– Leibniz-Zentrum fuer Informatik, 2011. · Zbl 1327.68211
[28] S. Fogarty and M. Vardi. B¨uchi Complementation and Size-Change Termination. In S. Kowalewski and A. Philippou, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 5505 of LNCS, pages 16–30. Springer-Verlag, 2009. · Zbl 1234.68256
[29] S. Fogarty and M. Y. Vardi. Efficient B¨uchi Universality Checking. In Tools and Algorithms for the Construction and Analysis of Systems, volume 6015 of LNCS, pages 205–220, 2010. · Zbl 1258.68076
[30] W. Fridman, C. L¨oding, and M. Zimmermann. Degrees of Lookahead in Context-free Infinite Games. In M. Bezem, editor, Proc. of CSL’11, volume 12 of LIPIcs, pages 264–276, Dagstuhl, Germany, 2011. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik. · Zbl 1206.03051
[31] C. Fritz and T. Wilke. Simulation Relations for Alternating B¨uchi Automata. Theor. Comput. Sci., 338(1-3):275–314, 2005. · Zbl 0408.03044
[32] C. Fritz and T. Wilke. Simulation relations for alternating parity automata and parity games. In O. Ibarra and Z. Dang, editors, In Proc. of DLT’06, volume 4036 of LNCS, pages 59–70. Springer Berlin / Heidelberg, 2006. · Zbl 0977.68538
[33] P. Gastin and D. Oddoux. Fast LTL to B¨uchi automata translation. In CAV, volume 2102 of LNCS, pages 53–65. Springer, 2001. · Zbl 1128.68366
[34] C¸ . E. Gerede, R. Hull, O. H. Ibarra, and J. Su. Automated composition of e-services: Lookaheads. In Proc. of ICSOC ’04, ICSOC ’04, pages 252–262, New York, NY, USA, 2004. ACM. · Zbl 1248.68242
[35] S. Gurumurthy, R. Bloem, and F. Somenzi. Fair simulation minimization. In Proc. of CAV’02, volume 2404 of LNCS, pages 610–624. Springer, 2002. · Zbl 1010.68086
[36] M. R. Henzinger, T. A. Henzinger, and P. W. Kopke. Computing simulations on finite and infinite graphs. In Foundations of Computer Science, FOCS ’95, Washington, DC, USA, 1995. IEEE Computer Society. · Zbl 0983.68080
[37] T. A. Henzinger, O. Kupferman, and S. K. Rajamani. Fair Simulation. Information and Computation, 173:64–81, 2002. · Zbl 06623526
[38] L. Hol´ık and J. ˇSim´aˇcek. Optimizing an LTS-simulation algorithm. Technical Report FIT-TR-2009-03, Brno University of Technology, 2009. http://www.fit.vutbr.cz/research/view_pub.php.en?id=9085. · Zbl 1409.68253
[39] M. Holtmann, L. Kaiser, and W. Thomas. Degrees of lookahead in regular infinite games. LMCS, 8(3:24):1–15, Sept. 2012. · Zbl 1406.68106
[40] G. Holzmann. The SPIN Model Checker. Addison-Wesley, 2004. · Zbl 1336.03065
[41] J. E. Hopcroft. An n log n algorithm for minimizing states in a finite automaton. Technical report, Stanford, CA, USA, 1971. · Zbl 0497.68021
[42] F. A. Hosch and L. H. Landweber. Finite delay solutions for sequential conditions. In Proc. of ICALP’72, pages 45–70, 1972.
[43] M. Hutagalung, M. Lange, and E. Lozes. Revealing vs. Concealing: More Simulation Games for B¨uchi Inclusion. In A.-H. Dediu, C. Mart´ın-Vide, and B. Truthe, editors, Proc. of LATA’13, volume 7810 of · Zbl 1390.68585
[44] M. Hutagalung, M. Lange, and E. Lozes. Buffered simulation games for B¨uchi Automata. In ´Esik, Zolt´an and F¨ul¨op, Zolt´an, editors, Proc. of AFL’14, volume 151 of EPTCS, pages 286–300. Open Publishing Association, 2014.
[45] T. Jiang and B. Ravikumar. Minimal NFA Problems are Hard. In J. Albert, B. Monien, and M. Artalejo, editors, ICALP, volume 510 of LNCS, pages 629–640. Springer-Verlag, 1991. · Zbl 0766.68063
[46] S. Juvekar and N. Piterman. Minimizing Generalized B¨uchi Automata. In Computer Aided Verification, volume 4414 of LNCS, pages 45–58. Springer-Verlag, 2006. · Zbl 0870.68077
[47] F. Klein and M. Zimmermann. How much lookahead is needed to win infinite games? In M. M. Halld´orsson, K. Iwama, N. Kobayashi, and B. Speckmann, editors, Proc. of ICALP’15, volume 9135 of LNCS, pages 452–463. Springer, 2015. · Zbl 0586.03010
[48] F. Klein and M. Zimmermann. What are Strategies in Delay Games? Borel Determinacy for Games with Lookahead. In S. Kreutzer, editor, Proc. of CSL’15, volume 41 of LIPIcs, pages 519–533, Dagstuhl, Germany, 2015. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik. · Zbl 1434.03123
[49] O. Kupferman and M. Vardi. Verification of Fair Transition Systems. In Computer Aided Verification, volume 1102 of LNCS, pages 372–382. Springer-Verlag, 1996.
[50] R. Kurshan. Complementing deterministic B¨uchi automata in polynomial time. Journal of Computer and System Sciences, 35(1):59–71, 1987. · Zbl 1309.68168
[51] C. S. Lee, N. D. Jones, and A. M. Ben-Amram. The size-change principle for program termination. In Proc. of POPL’01, pages 81–92. ACM, 2001. · Zbl 1323.68216
[52] O. Leng´al, J. ˇSim´aˇcek, and T. Vojnar. Libvata: highly optimised non-deterministic finite tree automata library. http://www.fit.vutbr.cz/research/groups/verifit/tools/libvata/, 2015.
[53] J. Leroux and G. Point. TaPAS: The Talence Presburger Arithmetic Suite. In Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 5505 of LNCS. Springer, 2009. · Zbl 1234.03002
[54] C. L¨oding. Efficient minimization of deterministic weak omega-automata. Inf. Process. Lett., 79(3):105– 109, July 2001. · Zbl 0891.03029
[55] C. L¨oding and S. Repke. Decidability Results on the Existence of Lookahead Delegators for NFA. In A. Seth and N. K. Vishnoi, editors, FSTTCS’13, volume 24 of LIPIcs, pages 327–338, Dagstuhl, Germany, 2013. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik. · Zbl 1359.68173
[56] A. R. Meyer and L. J. Stockmeyer. The equivalence problem for regular expressions with squaring requires exponential space. In Proceedings of the 13th Annual Symposium on Switching and Automata Theory, SWAT ’72, pages 125–129, Washington, DC, USA, 1972. IEEE Computer Society. · Zbl 06623527
[57] R. Milner. Communication and Concurrency. Prentice Hall, 1989. · Zbl 0683.68008
[58] I. Niven. Mathematics of Choice. The Mathematical Association of America, 1965.
[59] D. Park. Concurrency and automata on infinite sequences. In Proceedings of the 5th GI-Conference on Theoretical Computer Science, pages 167–183, London, UK, UK, 1981. Springer-Verlag. · Zbl 1186.68440
[60] N. Piterman. From nondeterministic B¨uchi and Streett automata to deterministic parity automata. In LICS, pages 255–264. IEEE, 2006. · Zbl 0953.68150
[61] J. Rathke, P. Soboci´nski, and O. Stephens. Compositional reachability in Petri Nets. In J. Ouaknine, I. Potapov, and J. Worrell, editors, Proc. of RP’14, volume 8762 of LNCS, pages 230–243. Springer, 2014. · Zbl 06623531
[62] B. Ravikumar and N. Santean. Deterministic simulation of a NFA with k–symbol lookahead. In J. van Leeuwen, G. Italiano, W. van der Hoek, C. Meinel, H. Sack, and F. Pl´aˇsil, editors, Proc. of SOFSEM’07, volume 4362 of LNCS, pages 488–497. Springer, 2007. · Zbl 1131.68471
[63] R. Sebastiani and S. Tonetta. More deterministic vs. smaller B¨uchi automata for efficient LTL model checking. In Correct Hardware Design and Verification Methods, volume 2860 of LNCS, 2003. · Zbl 0632.94030
[64] A. P. Sistla, M. Y. Vardi, and P. Wolper. The complementation problem for B¨uchi automata with applications to temporal logic. Theor. Comput. Sci., 49:217–237, Jan. 1987. · Zbl 0613.03015
[65] F. Somenzi and R. Bloem. Efficient B¨uchi Automata from LTL Formulae. In Computer Aided Verification, volume 1855 of LNCS, pages 248–263. Springer-Verlag, 2000. · Zbl 1214.94086
[66] D. Tabakov and M. Vardi. Model Checking B¨uchi Specifications. In LATA, volume Report 35/07. Research Group on Mathematical Linguistics, Universitat Rovira i Virgili, Tarragona, 2007. · Zbl 1133.03037
[67] W. Thomas. Automata on Infinite Objects, Handbook of theoretical computer science (vol. B), Chapter 4.
[68] 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 C. Ramakrishnan and J. Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 4963 of LNCS, pages 346–350. SpringerVerlag, 2008. · Zbl 1134.68420
[69] Y.-K. Tsay, M.-H. Tsai, J.-S. Chang, and Y.-W. Chang. B¨uchi store: An open repository of B¨uchi automata. In P. A. Abdulla and K. Leino, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 6605 of LNCS, pages 262–266. Springer-Verlag, 2011. 10.1007/978-3-642-19835-9 23 http://buchi.im.ntu.edu.tw/.
[70] Y.-K. Tsay, M.-H. Tsai, J.-S. Chang, Y.-W. Chang, and C.-S. Liu. B¨uchi Store: An open repository of ω-automata. International Journal on Software Tools for Technology Transfer, 15(2):109–123, 2013. http://buchi.im.ntu.edu.tw/.
[71] M. D. Wulf, L. Doyen, T. A. Henzinger, and J.-F. Raskin. Antichains: A new algorithm for checking universality of finite automata. In Proc. of CAV 2006, volume 4144 of LNCS, pages 17–30. Springer-Verlag, 2006. · Zbl 1188.68171
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.