Online timed pattern matching using derivatives
22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2016 and held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, Hollanda, 2 - 08 Nisan 2016, cilt.9636, ss.736-751, (Tam Metin Bildiri)
- Yayın Türü: Bildiri / Tam Metin Bildiri
- Cilt numarası: 9636
- Doi Numarası: 10.1007/978-3-662-49674-9_47
- Basıldığı Şehir: Eindhoven
- Basıldığı Ülke: Hollanda
- Sayfa Sayıları: ss.736-751
- Boğaziçi Üniversitesi Adresli: Hayır
Özet
Timed pattern matching consists in finding all segments of a dense-time Boolean signal that match a pattern defined by a timed regular expression. This problem has been formulated and solved in [17] via an offline algorithm that takes the signal and expression as inputs and produces the set of all matches, represented as a finite union of two-dimensional zones. In this work we develop an online version of this approach where the input signal is presented incrementally and the matching is computed incrementally as well. Naturally, the concept of derivatives of regular expressions due to Brzozowski [6] can play a role in defining what remains to match after having read a prefix of the signal. However the adaptation of this concept is not a straightforward for two reasons: the dense infinite-state nature of timed behaviors and the fact that we are interested in matching, not only in prefix acceptance. To resolve these issues we develop an alternative theory of signals and expressions based on absolute time and show how derivatives are defined and computed in this setting. We then implement an online timed pattern matching algorithm based on these results.