Combining the temporal and epistemic dimensions for MTL monitoring
15th International Conference on Formal Modelling and Analysis of Timed Systems, FORMATS 2017, Berlin, Almanya, 5 - 07 Eylül 2017, cilt.10419 LNCS, ss.207-223, (Tam Metin Bildiri)
- Yayın Türü: Bildiri / Tam Metin Bildiri
- Cilt numarası: 10419 LNCS
- Doi Numarası: 10.1007/978-3-319-65765-3_12
- Basıldığı Şehir: Berlin
- Basıldığı Ülke: Almanya
- Sayfa Sayıları: ss.207-223
- Boğaziçi Üniversitesi Adresli: Hayır
Özet
We define a new notion of satisfaction of a temporal logic formula (formula presented) by a behavior w. This notion, denoted by (formula presented), is characterized by two time parameters: the position t from which satisfaction is considered, and the end of the (finite) behavior t' which indicates how much do we know about the behavior. We define this notion in dense time where (formula presented) is a formula in the future fragment of metric temporal logic (MTL) and w is a Boolean signal of bounded variability. We show that the set of all pairs (t,t') such that (formula presented) can be expressed as a finite union of two-dimensional zones and give an effective procedure to compute it.