Seminar Room, ground floor (Building IMAG)
15 January 2018 - 14h00
Pattern Matching with Time: Theory and Applications (Phd Defense)
by Dogan Ulus from Verimag / UGA
Abstract: Dynamical systems exhibit temporal behaviors that can be expressed in various (sequential) forms such as signals, waveforms, time series, and event sequences. Detecting patterns over such temporal behaviors is a fundamental task for understanding and assessing these systems. Since many system behaviors involve certain timing characteristics, the need to specify and detect patterns of behaviors that involves quantitative timing requirements, called timed patterns, is evident. However, this is a non-trivial task due to a number of reasons including the concurrency of subsystems and the density of time.
The key contribution of this thesis is in introducing and developing timed pattern matching, that is, the act of identifying segments of a given behavior that satisfy a timed pattern. We propose timed regular expressions (TREs) and metric compass logic (MCL) as timed pattern
specification languages. We first develop a novel framework that abstracts the computation of time-related aspects called the algebra of timed relations. Then we provide offline matching algorithms for TRE and MCL over discrete-valued dense-time behaviors using this framework and study some practical extensions.
It is necessary for some application areas such as runtime verification that pattern matching needs to be performed during the actual execution of the system. For that, we provide an online matching algorithm for tres based on the classical technique of derivatives of regular expressions. We believe the underlying technique which combines derivatives and timed relations constitutes another major conceptual contribution for timed systems research.
Furthermore, we present an open-source tool Montre that implements our ideas and algorithms. We explore diverse applications of timed pattern matching over several case studies using Montre. Finally we discuss future directions and several open questions that emerged as a result of this thesis.
Composition of the Jury:
- Oded Maler, Verimag (Thesis Supervisor)
- Rajeev Alur, University of Pennsylvania, USA (Reviewer)
- Kim G. Larsen, University of Aalborg, Denmark (Reviewer)
- Radu Grosu, Technical University of Vienna, Austria (Reviewer)
- Patricia Bouyer-Decitre, LSV Cachan (Examiner)
- Ahmed Bouajjani, Irif, Universite Paris 7 (Examiner)
- Saddek Bensalem, Verimag (Examiner)
- Eugene Asarin, Irif, Universite Paris 7 (Invited)
- Dejan Nickovic, AIT, Austria (Invited)
