Skip to main content
SpringerLink
Log in

Efficient Online Timed Pattern Matching by Automata-Based Skipping

  • Conference paper
  • First Online:
Formal Modeling and Analysis of Timed Systems (FORMATS 2017)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10419))

Abstract

The timed pattern matching problem is an actively studied topic because of its relevance in monitoring of real-time systems. There one is given a log w and a specification \(\mathcal {A}\) (given by a timed word and a timed automaton in this paper), and one wishes to return the set of intervals for which the log w, when restricted to the interval, satisfies the specification \(\mathcal {A}\). In our previous work we presented an efficient timed pattern matching algorithm: it adopts a skipping mechanism inspired by the classic Boyer–Moore (BM) string matching algorithm. In this work we tackle the problem of online timed pattern matching, towards embedded applications where it is vital to process a vast amount of incoming data in a timely manner. Specifically, we start with the Franek-Jennings-Smyth (FJS) string matching algorithm—a recent variant of the BM algorithm—and extend it to timed pattern matching. Our experiments indicate the efficiency of our FJS-type algorithm in online and offline timed pattern matching.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    The FJS-type algorithm we present here is a simplified version of the original FJS algorithm. Our simplification is equipped with all the features that we will exploit later for pattern matching and timed pattern matching; the original algorithm further omits some other trivially unnecessary matching trials. We note that, because of the difference (that is conceptually inessential), our simplified algorithm (for string matching) no longer enjoys linear worst-case complexity.

  2. 2.

    In our previous work [32] we used regions [1] in place of zones. Though equivalent in terms of finiteness, zones give more efficient abstraction than regions.

  3. 3.

    To be precise we can start without the last \(m-1\) characters, where m is the length of a shortest word accepted by \(\mathcal {A}\). Usually m is by magnitude smaller than |w|.

References

  1. Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  2. Alur, R., Henzinger, T.A.: Back to the future: towards a theory of timed regular languages. In: 33rd Annual Symposium on Foundations of Computer Science, Pittsburgh, Pennsylvania, USA, 24–27 October 1992, pp. 177–186. IEEE Computer Society (1992)

    Google Scholar 

  3. Asarin, E., Caspi, P., Maler, O.: Timed regular expressions. J. ACM 49(2), 172–206 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  4. Behrmann, G., Bouyer, P., Fleury, E., Larsen, K.G.: Static guard analysis in timed automata verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 254–270. Springer, Heidelberg (2003). doi:10.1007/3-540-36577-X_18

    Chapter  Google Scholar 

  5. Behrmann, G., Bouyer, P., Larsen, K.G., Pelánek, R.: Lower and upper bounds in zone-based abstractions of timed automata. STTT 8(3), 204–215 (2006)

    Article  MATH  Google Scholar 

  6. Bombara, G., Vasile, C.I., Penedo, F., Yasuoka, H., Belta, C.: A decision tree approach to data classification using signal temporal logic. In: Abate, A., Fainekos, G.E. (eds.) HSCC 2016, Vienna, Austria, April 12–14, 2016, pp. 1–10. ACM (2016)

    Google Scholar 

  7. Boyer, R.S., Moore, J.S.: A fast string searching algorithm. Commun. ACM 20(10), 762–772 (1977)

    Article  MATH  Google Scholar 

  8. Chen, S., Sokolsky, O., Weimer, J., Lee, I.: Data-driven adaptive safety monitoring using virtual subjects in medical cyber-physical systems: a glucose control case study. JCSE 10(3), 75–84 (2016)

    Google Scholar 

  9. Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 197–212. Springer, Heidelberg (1990). doi:10.1007/3-540-52148-8_17

    Chapter  Google Scholar 

  10. DSouza, D., Matteplackel, R.: A clock-optimal hierarchical monitoring automaton construction for mitl. Technical report (2013)

    Google Scholar 

  11. Faro, S., Lecroq, T.: The exact online string matching problem: a review of the most recent results. ACM Comput. Surv. 45(2), 13:1–13:42 (2013)

    Article  MATH  Google Scholar 

  12. Ferrère, T., Maler, O., Ničković, D., Ulus, D.: Measuring with timed patterns. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 322–337. Springer, Cham (2015). doi:10.1007/978-3-319-21668-3_19

    Chapter  Google Scholar 

  13. Franek, F., Jennings, C.G., Smyth, W.F.: A simple fast hybrid pattern-matching algorithm. J. Discrete Algorithms 5(4), 682–695 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  14. Herbreteau, F., Srivathsan, B., Walukiewicz, I.: Efficient emptiness check for timed büchi automata. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 148–161. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14295-6_15

    Chapter  Google Scholar 

  15. Ho, H.-M., Ouaknine, J., Worrell, J.: Online monitoring of metric temporal logic. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 178–192. Springer, Cham (2014). doi:10.1007/978-3-319-11164-3_15

    Google Scholar 

  16. Hoxha, B., Abbas, H., Fainekos, G.E.: Benchmarks for temporal logic requirements for automotive systems. In: Frehse, G., Althoff, M. (eds.) 1st and 2nd International Workshop on Applied veRification for Continuous and Hybrid Systems, ARCH@CPSWeek 2014, Berlin, Germany, April 14, 2014 / ARCH@CPSWeek 2015, EPiC Series in Computing,Seattle, WA, USA, April 13, 2015, vol. 34, pp. 25–30. EasyChair (2014)

    Google Scholar 

  17. Jin, X., Deshmukh, J.V., Kapinski, J., Ueda, K., Butts, K.R.: Powertrain control verification benchmark. In: Fränzle M., Lygeros, J. (eds.) HSCC 2014, Berlin, Germany, April 15–17, 2014, pp. 253–262. ACM (2014)

    Google Scholar 

  18. Kane A.: Runtime monitoring for safety-critical embedded systems. Ph.D. thesis, Carnegie Mellon University, USA (2015)

    Google Scholar 

  19. Kane, A., Chowdhury, O., Datta, A., Koopman, P.: A case study on runtime monitoring of an autonomous research vehicle (ARV) system. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 102–117. Springer, Cham (2015). doi:10.1007/978-3-319-23820-3_7

    Chapter  Google Scholar 

  20. Kini, D.R., Krishna, S.N., Pandya, P.K.: On construction of safety signal automata for \(MITL[\,\cal{U},\,\cal{S}]\) using temporal projections. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 225–239. Springer, Heidelberg (2011). doi:10.1007/978-3-642-24310-3_16

    Chapter  Google Scholar 

  21. Knuth, D.E., Morris Jr., J.H., Pratt, V.R.: Fast pattern matching in strings. SIAM J. Comput. 6(2), 323–350 (1977)

    Article  MathSciNet  MATH  Google Scholar 

  22. Maler, O., Nickovic, D., Pnueli, A.: From MITL to timed automata. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 274–289. Springer, Heidelberg (2006). doi:10.1007/11867340_20

    Chapter  Google Scholar 

  23. The MathWorks Inc, Natick, MA, USA. Simulink User’s Guide (2015)

    Google Scholar 

  24. Ničković, D., Piterman, N.: From Mtl to deterministic timed automata. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 152–167. Springer, Heidelberg (2010). doi:10.1007/978-3-642-15297-9_13

    Chapter  Google Scholar 

  25. Pure Programming Language. https://purelang.bitbucket.io

  26. Raimondi, F., Skene, J., Emmerich, W.: Efficient online monitoring of web-service slas. In: Harrold, M.J., Murphy, G.C. (eds.) Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2008, Atlanta, Georgia, USA, November 9–14, 2008, pp. 170–180. ACM (2008)

    Google Scholar 

  27. Reinbacher, T., Függer, M., Brauer, J.: Runtime verification of embedded real-time systems. Formal Meth. Syst. Des. 44(3), 203–239 (2014)

    Article  MATH  Google Scholar 

  28. Sunday, D.: A very fast substring search algorithm. Commun. ACM 33(8), 132–142 (1990)

    Article  Google Scholar 

  29. Ulus, D.: Montre: a tool for monitoring timed regular expressions. CoRR, abs/1605.05963 (2016)

    Google Scholar 

  30. Ulus, D., Ferrère, T., Asarin, E., Maler, O.: Timed pattern matching. In: Legay, A., Bozga, M. (eds.) FORMATS 2014. LNCS, vol. 8711, pp. 222–236. Springer, Cham (2014). doi:10.1007/978-3-319-10512-3_16

    Google Scholar 

  31. Ulus, D., Ferrère, T., Asarin, E., Maler, O.: Online timed pattern matching using derivatives. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 736–751. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49674-9_47

    Chapter  Google Scholar 

  32. Waga, M., Akazaki, T., Hasuo, I.: A boyer-moore type algorithm for timed pattern matching. In: Fränzle, M., Markey, N. (eds.) FORMATS 2016. LNCS, vol. 9884, pp. 121–139. Springer, Cham (2016). doi:10.1007/978-3-319-44878-7_8

    Chapter  Google Scholar 

  33. Waga, M., Hasuo I., Suenaga, K.: Code that Accompanies “Efficient Online Timed Pattern Matching by Automata-Based Skipping”. https://github.com/MasWag/timed-pattern-matching

  34. Waga, M., Hasuo, I., Suenaga K.: Efficient Online Timed Pattern Matching by Automata-Based Skipping. CoRR, abs/1706.09174 (2017)

    Google Scholar 

  35. Watson, B.W., Watson, R.E.: A boyer-moore-style algorithm for regular expression pattern matching. Sci. Comput. Program. 48(2–3), 99–117 (2003)

    Article  MATH  Google Scholar 

Download references

Acknowledgments

Thanks are due to Sean Sedwards, Eugenia Sironi and the anonymous referees for useful discussions and comments. The authors are supported by JSPS Grant-in-Aid 15KT0012. M.W. and I.H. are supported by JST ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), and JSPS Grant-in-Aid No. 15K11984. K.S. is supported by JST PRESTO (No. JPMJPR15E5) and JSPS Grant-in-Aid No. 70633692.

Author information

Authors and Affiliations

  1. University of Tokyo, Tokyo, Japan

    Masaki Waga

  2. National Institute of Informatics, Tokyo, Japan

    Ichiro Hasuo

  3. Kyoto University and JST PRESTO, Kyoto, Japan

    Kohei Suenaga

Authors
  1. Masaki Waga
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ichiro Hasuo
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Kohei Suenaga
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Masaki Waga .

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of Oxford, Oxford, United Kingdom

    Alessandro Abate

  2. Dept. d’Informatique, Université Libre de Bruxelles, Brussels, Belgium

    Gilles Geeraerts

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Waga, M., Hasuo, I., Suenaga, K. (2017). Efficient Online Timed Pattern Matching by Automata-Based Skipping. In: Abate, A., Geeraerts, G. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2017. Lecture Notes in Computer Science(), vol 10419. Springer, Cham. https://doi.org/10.1007/978-3-319-65765-3_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-65765-3_13

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-65764-6

  • Online ISBN: 978-3-319-65765-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation