Specifying timed patterns using temporal logic
21st International Conference on Hybrid Systems: Computation and Control, HSCC 2018, Porto, Portekiz, 11 - 13 Nisan 2018, ss.167-176, (Tam Metin Bildiri)
- Yayın Türü: Bildiri / Tam Metin Bildiri
- Doi Numarası: 10.1145/3178126.3178129
- Basıldığı Şehir: Porto
- Basıldığı Ülke: Portekiz
- Sayfa Sayıları: ss.167-176
- Anahtar Kelimeler: Formal methods, Pattern matching, Realtime and embedded systems, Temporal logic
- Boğaziçi Üniversitesi Adresli: Hayır
Özet
Monitoring system behaviors using formal specifications appears to be an effective technique in analyzing cyber-physical systems. However, to achieve intended results in monitoring, specification languages need to be intuitive, elegant, and expressive at the first place. In this paper, we propose a metric extension of well-known Halpern-Shoham (HS) logic, called Metric Compass Logic (MCL), for monitoring purposes. Originally proposed for high-level temporal reasoning, the logic HS is very expressive and enables users to specify many temporal patterns in an intuitive and elegant way. As our main contribution, we present an offline monitoring technique for timed patterns specified in MCL. Our solution is built upon the framework developed for timed regular expressions (TRE) matching but explores a different (logical) direction. We finally study several practical features concerning atomic formulas and discuss a combined timed pattern specification language with TRE.