Simulation Algorithms for Symbolic Automata

  • Lukáš Holík
  • Ondřej LengálEmail author
  • Juraj Síč
  • Margus Veanes
  • Tomáš Vojnar
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11138)


We investigate means of efficient computation of the simulation relation over symbolic finite automata (SFAs), i.e., finite automata with transitions labeled by predicates over alphabet symbols. In one approach, we build on the algorithm by Ilie, Navaro, and Yu proposed originally for classical finite automata, modifying it using the so-called mintermisation of the transition predicates. This solution, however, generates all Boolean combinations of the predicates, which easily causes an exponential blowup in the number of transitions. Therefore, we propose two more advanced solutions. The first one still applies mintermisation but in a local way, mitigating the size of the exponential blowup. The other one focuses on a novel symbolic way of dealing with transitions, for which we need to sacrifice the counting technique of the original algorithm (counting is used to decrease the dependency of the running time on the number of transitions from quadratic to linear). We perform a thorough experimental evaluation of all the algorithms, together with several further alternatives, showing that all of them have their merits in practice, but with the clear indication that in most of the cases, efficient treatment of symbolic transitions is more beneficial than counting.



This paper was supported by the Czech Science Foundation projects 16-17538S and 16-24707Y, the IT4IXS: IT4Innovations Excellence in Science project (LQ1602), and the FIT BUT internal project FIT-S-17-4014.


  1. 1.
    Watson, B.W.: Implementing and Using Finite Automata Toolkits. Cambridge University Press, New York (1999)Google Scholar
  2. 2.
    Veanes, M., Bjørner, N.: Symbolic automata: the toolkit. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 472–477. Springer, Heidelberg (2012). Scholar
  3. 3.
    Veanes, M.: Applications of symbolic finite automata. In: Konstantinidis, S. (ed.) CIAA 2013. LNCS, vol. 7982, pp. 16–23. Springer, Heidelberg (2013). Scholar
  4. 4.
    D’Antoni, L., Veanes, M.: The power of symbolic automata and transducers. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 47–67. Springer, Cham (2017). Scholar
  5. 5.
    Abdulla, P.A., Chen, Y.-F., Holík, L., Mayr, R., Vojnar, T.: When simulation meets antichains. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 158–174. Springer, Heidelberg (2010). Scholar
  6. 6.
    Bonchi, F., Pous, D.: Checking NFA equivalence with bisimulations up to congruence. In: Proceeding of POPL’13, ACM (2013)Google Scholar
  7. 7.
    Ilie, L., Navarro, G., Yu, S.: On NFA reductions. In: Karhumäki, J., Maurer, H., Păun, G., Rozenberg, G. (eds.) Theory Is Forever. LNCS, vol. 3113, pp. 112–124. Springer, Heidelberg (2004). Scholar
  8. 8.
    Holík, L., Šimáček, J.: Optimizing an LTS-simulation algorithm. In: Masaryk, U. (ed.) Proceedings of MEMICS’09 (2009)Google Scholar
  9. 9.
    Lengál, O., Šimáček, J., Vojnar, T.: VATA: a library for efficient manipulation of non-deterministic tree automata. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 79–94. Springer, Heidelberg (2012). Scholar
  10. 10.
    Henzinger, M.R., Henzinger, T.A., Kopke, P.W.: Computing simulations on finite and infinite graphs. In: Proceedings of FOCS’95, IEEE (1995)Google Scholar
  11. 11.
    Cécé, G.: Foundation for a series of efficient simulation algorithms. In: Proceedings of LICS’17, IEEE (2017)Google Scholar
  12. 12.
    D’Antoni, L., Veanes, M.: Minimization of symbolic automata. In: Proceedings of POPL’14, ACM (2014)Google Scholar
  13. 13.
    D’Antoni, L., Veanes, M.: Forward bisimulations for nondeterministic symbolic finite automata. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 518–534. Springer, Heidelberg (2017). Scholar
  14. 14.
    Eberl, M.: Efficient and verified computation of simulation relations on NFAs. Bachelor’s thesis, TU Munich, 2012Google Scholar
  15. 15.
    Regular expression library.
  16. 16.
    Comon, H., et al.: Tree automata techniques and applications (2007)Google Scholar
  17. 17.
    Elgaard, J., Klarlund, N., Møller, A.: MONA 1.x: new techniques for WS1S and WS2S. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 516–520. Springer, Heidelberg (1998). Scholar
  18. 18.
    Fiedor, T., Holík, L., Lengál, O., Vojnar, T.: Nested antichains for WS1S. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 658–674. Springer, Heidelberg (2015). Scholar
  19. 19.
    Ranzato, F.: A more efficient simulation algorithm on Kripke structures. In: Chatterjee, K., Sgall, J. (eds.) MFCS 2013. LNCS, vol. 8087, pp. 753–764. Springer, Heidelberg (2013). Scholar
  20. 20.
    Bustan, D., Grumberg, O.: Simulation-based minimization. ACM Trans. Comput. Log. 4(2), 181–206 (2003)MathSciNetCrossRefGoogle Scholar
  21. 21.
    Holík, L., Lengál, O., Síč, J., Veanes, M., Vojnar, T.: Simulation algorithms for symbolic automata (Technical Report). CoRR, arXiv:abs/1807.08487 (2018)

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Lukáš Holík
    • 1
  • Ondřej Lengál
    • 1
    Email author
  • Juraj Síč
    • 1
    • 2
  • Margus Veanes
    • 3
  • Tomáš Vojnar
    • 1
  1. 1.FITBrno University of Technology, IT4Innovations Centre of ExcellenceBrnoCzech Republic
  2. 2.Faculty of InformaticsMasaryk UniversityBrnoCzech Republic
  3. 3.Microsoft ResearchRedmondUSA

Personalised recommendations