Advertisement

Succinct Determinisation of Counting Automata via Sphere Construction

  • Lukáš Holík
  • Ondřej Lengál
  • Olli Saarikivi
  • Lenka Turoňová
  • Margus VeanesEmail author
  • Tomáš Vojnar
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11893)

Abstract

We propose an efficient algorithm for determinising counting automata (CAs), i.e., finite automata extended with bounded counters. The algorithm avoids unfolding counters into control states, unlike the naïve approach, and thus produces much smaller deterministic automata. We also develop a simplified and faster version of the general algorithm for the sub-class of so-called monadic CAs (MCAs), i.e., CAs with counting loops on character classes, which are common in practice. Our main motivation is (besides applications in verification and decision procedures of logics) the application of deterministic (M)CAs in pattern matching regular expressions with counting, which are very common in e.g. network traffic processing and log analysis. We have evaluated our algorithm against practical benchmarks from these application domains and concluded that compared to the naïve approach, our algorithm is much less prone to explode, produces automata that can be several orders of magnitude smaller, and is overall faster.

References

  1. 1.
    Abdulla, P.A., Krcal, P., Yi, W.: R-automata. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 67–81. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-85361-9_9CrossRefGoogle Scholar
  2. 2.
    Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: FAST: acceleration from theory to practice. STTT 10(5) (2008)CrossRefGoogle Scholar
  3. 3.
    Börklund, E., Martens, W., Timm, T.: Efficient incremental evaluation of succinct regular expressions. In: Proceedings of CIKM 2015, ACM (2015)Google Scholar
  4. 4.
    Chen, H., Lu, P.: Checking determinism of regular expressions with counting. Inf. Comput. 241, 302–320 (2015)MathSciNetCrossRefGoogle Scholar
  5. 5.
    Cheng, K., Krishnakumar, A.S.: Automatic functional test generation using the extended finite state machine model. In: Proceedings of DAC 1993, ACM Press (1993)Google Scholar
  6. 6.
    D’Antoni, L., Veanes, M.: Minimization of symbolic automata. In: Proceedings of POPL 2014, ACM (2014)Google Scholar
  7. 7.
    Dill, D.L., Hu, A.J., Wong-Toi, H.: Checking for language inclusion using simulation preorders. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 255–265. Springer, Heidelberg (1992).  https://doi.org/10.1007/3-540-55179-4_25CrossRefGoogle Scholar
  8. 8.
    Gelade, W., Martens, W., Neven, F.: Optimizing schema languages for XML: numerical constraints and interleaving. In: Schwentick, T., Suciu, D. (eds.) ICDT 2007. LNCS, vol. 4353, pp. 269–283. Springer, Heidelberg (2006).  https://doi.org/10.1007/11965893_19CrossRefGoogle Scholar
  9. 9.
    Gelade, W., Gyssens, M., Martens, W.: Regular expressions with counting: weak versus strong determinism. In: Královič, R., Niwiński, D. (eds.) MFCS 2009. LNCS, vol. 5734, pp. 369–381. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-03816-7_32CrossRefGoogle Scholar
  10. 10.
    van Glabbeek, R., Ploeger, B.: Five Determinisation algorithms. In: Ibarra, O.H., Ravikumar, B. (eds.) CIAA 2008. LNCS, vol. 5148, pp. 161–170. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-70844-5_17CrossRefGoogle Scholar
  11. 11.
    Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 36–52. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-39799-8_2CrossRefGoogle Scholar
  12. 12.
    Henriksen, J.G., et al.: Mona: monadic second-order logic in practice. In: Brinksma, E., Cleaveland, W.R., Larsen, K.G., Margaria, T., Steffen, B. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 89–110. Springer, Heidelberg (1995).  https://doi.org/10.1007/3-540-60630-0_5CrossRefGoogle Scholar
  13. 13.
    Hovland, D.: Regular expressions with numerical constraints and automata with counters. In: Leucker, M., Morgan, C. (eds.) ICTAC 2009. LNCS, vol. 5684, pp. 231–245. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-03466-4_15CrossRefGoogle Scholar
  14. 14.
    Hovland, D.: The membership problem for regular expressions with unordered concatenation and numerical constraints. In: Dediu, A.-H., Martín-Vide, C. (eds.) LATA 2012. LNCS, vol. 7183, pp. 313–324. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-28332-1_27CrossRefzbMATHGoogle Scholar
  15. 15.
    Kilpeläinen, P., Tuhkanen, R.: One-unambiguity of regular expressions with numeric occurrence indicators. Inf. Comput. 205(6), 890–916 (2007)MathSciNetCrossRefGoogle Scholar
  16. 16.
    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).  https://doi.org/10.1007/978-3-642-28756-5_7CrossRefzbMATHGoogle Scholar
  17. 17.
    Roesch, M., et al.: Snort: A Network Intrusion Detection and Prevention System. http://www.snort.org
  18. 18.
    Microsoft Automata Library: Automata and Transducer Library for .NET. https://github.com/AutomataDotNet/Automata
  19. 19.
    OWASP Foundation and Checkmarx: Regular Expression Denial of Service: ReDoS (2017)Google Scholar
  20. 20.
    RegExLib.com: The Internet’s First Regular Expression Library. http://regexlib.com/
  21. 21.
    Sommer, R., et al.: The Bro Network Security Monitor. http://www.bro.org
  22. 22.
    Shiple, T.R., Kukula, J.H., Ranjan, R.K.: A comparison of Presburger engines for EFSM reachability. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 280–292. Springer, Heidelberg (1998).  https://doi.org/10.1007/BFb0028752CrossRefGoogle Scholar
  23. 23.
    Smith, R., Estan, C., Jha, S.: XFA: faster signature matching with extended automata. In: Proceedings of SSP 2008, IEEE (2008)Google Scholar
  24. 24.
    Smith, R., Estan, C., Jha, S., Siahaan, I.: Fast signature matching using extended finite automaton (XFA). In: Sekar, R., Pujari, A.K. (eds.) ICISS 2008. LNCS, vol. 5352, pp. 158–172. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-89862-7_15CrossRefGoogle Scholar
  25. 25.
    Sperberg-McQueen, M.: Notes on Finite State Automata with Counters. https://www.w3.org/XML/2004/05/msm-cfa.html. Accessed 08 Aug 2018
  26. 26.
    The Sagan Team: The Sagan Log Analysis Engine. https://quadrantsec.com/sagan_log_analysis_engine/
  27. 27.
    Thompson, K.: Programming techniques: regular expression search algorithm. Commun. ACM 11(6), 419–422 (1968)CrossRefGoogle Scholar
  28. 28.
    Češka, M., Havlena, V., Holík, L., Lengál, O., Vojnar, T.: Approximate reduction of finite automata for high-speed network intrusion detection. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 155–175. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-89963-3_9CrossRefGoogle Scholar
  29. 29.
    Yang, L., Karim, R., Ganapathy, V., Smith, R.: Improving NFA-based signature matching using ordered binary decision diagrams. In: Jha, S., Sommer, R., Kreibich, C. (eds.) RAID 2010. LNCS, vol. 6307, pp. 58–78. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-15512-3_4CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Lukáš Holík
    • 1
  • Ondřej Lengál
    • 1
  • Olli Saarikivi
    • 2
  • Lenka Turoňová
    • 1
  • Margus Veanes
    • 2
    Email author
  • Tomáš Vojnar
    • 1
  1. 1.FIT, IT4Innovations Centre of ExcellenceBrno University of TechnologyBrnoCzech Republic
  2. 2.Microsoft ResearchRedmondUSA

Personalised recommendations