Timed Pattern Matching

  • Dogan Ulus
  • Thomas Ferrère
  • Eugene Asarin
  • Oded Maler
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8711)


Given a timed regular expression and a dense-time Boolean signal we compute the set of all matches of the expression in the signal, that is, the set of all segments of the signal that satisfy the regular expression. The set of matches is viewed as a set of points in a two-dimensional space with each point indicating the beginning and end of a matching segment on the real time axis. Our procedure, which works by induction on the structure of the expression, is based on the following result that we prove in this paper: the set of all matches of a timed regular expression by a signal of finite variability and duration can be written as a finite union of zones.


Temporal Logic Pattern Match Regular Expression Switching Point Satisfaction Relation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [ACM02]
    Asarin, E., Caspi, P., Maler, O.: Timed regular expressions. Journal of the ACM (JACM) 49(2), 172–206 (2002)CrossRefMathSciNetGoogle Scholar
  2. [AD94]
    Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)CrossRefzbMATHMathSciNetGoogle Scholar
  3. [AFH96]
    Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. Journal of the ACM (JACM) 43(1), 116–146 (1996)CrossRefzbMATHMathSciNetGoogle Scholar
  4. [AGM+90]
    Altschul, S., Gish, W., Miller, W., Myers, E., Lipman, D.: Basic local alignment search tool. Journal of Molecular Biology, 403–410 (1990)Google Scholar
  5. [BGM02]
    Bozga, M., Graf, S., Mounier, L.: IF-2.0: A validation environment for component-based real-time systems. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 343–348. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  6. [BM77]
    Boyer, R.S., Moore, J.S.: A fast string searching algorithm. Communications of the ACM (1977)Google Scholar
  7. [CR02]
    Crochemore, M., Rytter, W.: Jewels of Stringology. World Scientific (2002)Google Scholar
  8. [CVK04]
    Cohen, B., Venkataramanan, S., Kumari, A.: Using PSL/Sugar for formal and dynamic verification: Guide to Property Specification Language for Assertion-based Verification. VhdlCohen Publishing (2004)Google Scholar
  9. [DBS12]
    Dluhos, P., Brim, L., Safránek, D.: On expressing and monitoring oscillatory dynamics. In: HSB, pp. 73–87 (2012)Google Scholar
  10. [EF06]
    Eisner, C., Fisman, D.: A practical introduction to PSL. Springer (2006)Google Scholar
  11. [Fri06]
    Friedl, J.: Mastering regular expressions. O’Reilly Media, Inc. (2006)Google Scholar
  12. [FRM94]
    Faloutsos, C., Ranganathan, M., Manolopoulos, Y.: Fast subsequence matching in time-series databases. In: Proceedings of the ACM SIGMOD Conference on Management of Data (1994)Google Scholar
  13. [HL11]
    Havlicek, J., Little, S.: Realtime regular expressions for analog and mixed-signal assertions. In: FMCAD, pp. 155–162 (2011)Google Scholar
  14. [JS07]
    Jacox, E.H., Samet, H.: Spatial join techniques. ACM Transactions on Database Systems (TODS), 70 (2007)Google Scholar
  15. [Kle56]
    Kleene, S.C.: Representation of events in nerve nets and finite automata. Automata Studies (1956)Google Scholar
  16. [KMP77]
    Knuth, D.E., Morris Jr., J.H., Pratt, V.R.: Fast pattern matching in strings. SIAM Journal on Computing, 323–350 (1977)Google Scholar
  17. [Koy90]
    Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Systems 2(4), 255–299 (1990)CrossRefGoogle Scholar
  18. [Lau00]
    Laurikari, V.: NFAs with tagged transitions, their conversion to deterministic automata and application to regular expressions. In: Proceecedings of the Symposium on String Processing and Information Retrieval (SPIRE 2000), pp. 181–187 (2000)Google Scholar
  19. [MN04]
    Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS/FTRTFT 2004. LNCS, vol. 3253, pp. 152–166. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  20. [MNP05]
    Maler, O., Nickovic, D., Pnueli, A.: Real time temporal logic: Past, present, future. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 2–16. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  21. [MNP08]
    Maler, O., Ničković, D., Pnueli, A.: Checking temporal properties of discrete, timed and continuous behaviors. In: Pillars of Computer Science, pp. 475–505 (2008)Google Scholar
  22. [Pik87]
    Pike, R.: The text editor sam. Software: Practice and Experience 17(11), 813–845 (1987)Google Scholar
  23. [Spe06]
    Spear, C.: SystemVerilog for Verification. Springer (2006)Google Scholar
  24. [Ste94]
    Stephen, G.A.: String searching algorithms. World Scientific (1994)Google Scholar
  25. [Tho68]
    Thompson, K.: Programming techniques: Regular expression search algorithm. Communications of the ACM, 419–422 (1968)Google Scholar
  26. [VR06]
    Vijayaraghavan, S., Ramanathan, M.: A practical guide for SystemVerilog assertions. Springer (2006)Google Scholar
  27. [Wei73]
    Weiner, P.: Linear pattern matching algorithms. Switching and Automata Theory (1973)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Dogan Ulus
    • 1
  • Thomas Ferrère
    • 1
  • Eugene Asarin
    • 2
  • Oded Maler
    • 1
  1. 1.VERIMAGCNRS and the University of Grenoble-AlpesFrance
  2. 2.LIAFAUniversité Paris Diderot / CNRSParisFrance

Personalised recommendations