Skip to main content
Top
Published in: Formal Methods in System Design 3/2019

06-02-2019

Almost event-rate independent monitoring

Authors: David Basin, Bhargav Nagaraja Bhatt, Srđan Krstić, Dmitriy Traytel

Published in: Formal Methods in System Design | Issue 3/2019

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

A monitoring algorithm is trace-length independent if its space consumption does not depend on the number of events processed. The analysis of many monitoring algorithms has aimed at establishing their trace-length independence. But a monitor’s space consumption can depend on characteristics of the trace other than its size. We put forward the stronger notion of event-rate independence, where a monitor’s space usage does not depend on the event rate, i.e., the number of events in a fixed time unit. This property is critical for monitoring voluminous streams of events with a high arrival rate. We propose a new algorithm for metric temporal logic (MTL) that is almost event-rate independent, where “almost” denotes a logarithmic dependence on the event rate: the algorithm must store the event rate as a number. Afterwards, we investigate more expressive logics. In particular, we extend linear dynamic logic with past operators and metric features. The resulting metric dynamic logic (MDL) offers the quantitative temporal conveniences of MTL while increasing its expressiveness. We show how to modify our MTL algorithm in a modular way, yielding an almost event-rate independent monitor for MDL. Finally, we compare our algorithms with traditional monitoring approaches, providing empirical evidence that almost event-rate independence matters in practice.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Literature
1.
go back to reference Antimirov V (1996) Partial derivatives of regular expressions and finite automaton constructions. Theor Comput Sci 155(2):291–319MathSciNetCrossRef Antimirov V (1996) Partial derivatives of regular expressions and finite automaton constructions. Theor Comput Sci 155(2):291–319MathSciNetCrossRef
3.
go back to reference Basin DA, Bhatt B, Traytel D (2017) Almost event-rate indepedent monitoring of metric temporal logic. In: Legay A, Margaria T (eds) TACAS 2017, LNCS, vol 10206. Springer, New York, pp 94–112 Basin DA, Bhatt B, Traytel D (2017) Almost event-rate indepedent monitoring of metric temporal logic. In: Legay A, Margaria T (eds) TACAS 2017, LNCS, vol 10206. Springer, New York, pp 94–112
4.
5.
go back to reference Basin DA, Klaedtke F, Zălinescu E (2017) The MonPoly monitoring tool. In: Reger G, Havelund K (eds) RV-CuBES 2017, Kalpa Publications in computing, vol 3. EasyChair, Seattle, pp 19–28 Basin DA, Klaedtke F, Zălinescu E (2017) The MonPoly monitoring tool. In: Reger G, Havelund K (eds) RV-CuBES 2017, Kalpa Publications in computing, vol 3. EasyChair, Seattle, pp 19–28
6.
go back to reference Basin DA, Krstić S, Traytel D (2017) AERIAL: almost event-rate independent algorithms for monitoring metric regular properties. In: Reger G, Havelund K (eds) RV-CuBES 2017, Kalpa Publications in computing, vol 3. EasyChair, Seattle, pp 29–36 Basin DA, Krstić S, Traytel D (2017) AERIAL: almost event-rate independent algorithms for monitoring metric regular properties. In: Reger G, Havelund K (eds) RV-CuBES 2017, Kalpa Publications in computing, vol 3. EasyChair, Seattle, pp 29–36
7.
go back to reference Basin DA, Krstić S, Traytel D (2017) Almost event-rate indepedent monitoring of metric dynamic logic. In: Lahiri S, Reger G (eds) RV 2017, LNCS, vol 10548. Springer, New York, pp 85–102 Basin DA, Krstić S, Traytel D (2017) Almost event-rate indepedent monitoring of metric dynamic logic. In: Lahiri S, Reger G (eds) RV 2017, LNCS, vol 10548. Springer, New York, pp 85–102
8.
go back to reference Basin DA, Klaedtke F, Müller S, Pfitzmann B (2008) Runtime monitoring of metric first-order temporal properties. In: Hariharan R, Mukund M, Vinay V (eds) FSTTCS 2008, LIPIcs, vol 2. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Wadern, pp 49–60 Basin DA, Klaedtke F, Müller S, Pfitzmann B (2008) Runtime monitoring of metric first-order temporal properties. In: Hariharan R, Mukund M, Vinay V (eds) FSTTCS 2008, LIPIcs, vol 2. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Wadern, pp 49–60
9.
go back to reference Basin DA, Klaedtke F, Müller S, Zălinescu E (2015) Monitoring metric first-order temporal properties. J ACM 62(2):15:1–15:45MathSciNetCrossRef Basin DA, Klaedtke F, Müller S, Zălinescu E (2015) Monitoring metric first-order temporal properties. J ACM 62(2):15:1–15:45MathSciNetCrossRef
10.
go back to reference Basin DA, Klaedtke F, Zălinescu E (2012) Algorithms for monitoring real-time properties. In: Khurshid S, Sen K (eds) RV 2011, LNCS, vol 7186. Springer, New York, pp 260–275 Basin DA, Klaedtke F, Zălinescu E (2012) Algorithms for monitoring real-time properties. In: Khurshid S, Sen K (eds) RV 2011, LNCS, vol 7186. Springer, New York, pp 260–275
11.
go back to reference Bauer A, Küster J, Vegliach G (2013) From propositional to first-order monitoring. In: Legay A, Bensalem S (eds) RV 2013, LNCS, vol 8174. Springer, New York, pp 59–75 Bauer A, Küster J, Vegliach G (2013) From propositional to first-order monitoring. In: Legay A, Bensalem S (eds) RV 2013, LNCS, vol 8174. Springer, New York, pp 59–75
12.
14.
go back to reference D’Angelo B, Sankaranarayanan S, Sánchez C, Robinson W, Finkbeiner B, Sipma HB, Mehrotra S, Manna Z (2005) LOLA: runtime monitoring of synchronous systems. In: TIME 2005. IEEE Computer Society, pp 166–174 D’Angelo B, Sankaranarayanan S, Sánchez C, Robinson W, Finkbeiner B, Sipma HB, Mehrotra S, Manna Z (2005) LOLA: runtime monitoring of synchronous systems. In: TIME 2005. IEEE Computer Society, pp 166–174
15.
go back to reference Dax C, Klaedtke F, Lange M (2010) On regular temporal logics with past. Acta Inf 47(4):251–277CrossRef Dax C, Klaedtke F, Lange M (2010) On regular temporal logics with past. Acta Inf 47(4):251–277CrossRef
16.
go back to reference De Giacomo G, De Masellis R, Grasso M, Maggi FM, Montali M (2014) LTLf and LDLf monitoring: a technical report. CoRR arXiv:1405.0054 De Giacomo G, De Masellis R, Grasso M, Maggi FM, Montali M (2014) LTLf and LDLf monitoring: a technical report. CoRR arXiv:​1405.​0054
17.
go back to reference De Giacomo G, De Masellis R, Grasso M, Maggi FM, Montali M (2014) Monitoring business metaconstraints based on LTL and LDL for finite traces. In: Sadiq SW, Soffer P, Völzer H (eds) BPM 2014, LNCS, vol 8659. Springer, New York, pp 1–17 De Giacomo G, De Masellis R, Grasso M, Maggi FM, Montali M (2014) Monitoring business metaconstraints based on LTL and LDL for finite traces. In: Sadiq SW, Soffer P, Völzer H (eds) BPM 2014, LNCS, vol 8659. Springer, New York, pp 1–17
18.
go back to reference De Giacomo G, Vardi MY (2013) Linear temporal logic and linear dynamic logic on finite traces. In: Rossi F (ed) IJCAI-13. AAAI Press, New Orleans, pp 854–860 De Giacomo G, Vardi MY (2013) Linear temporal logic and linear dynamic logic on finite traces. In: Rossi F (ed) IJCAI-13. AAAI Press, New Orleans, pp 854–860
19.
go back to reference Du X, Liu Y, Tiu A (2015) Trace-length independent runtime monitoring of quantitative policies in LTL. In: Bjørner N, de Boer F (eds) FM 2015, LNCS, vol 9109. Springer, New York, pp 231–247 Du X, Liu Y, Tiu A (2015) Trace-length independent runtime monitoring of quantitative policies in LTL. In: Bjørner N, de Boer F (eds) FM 2015, LNCS, vol 9109. Springer, New York, pp 231–247
20.
go back to reference Faymonville P, Zimmermann M (2014) Parametric linear dynamic logic. In: Peron A, Piazza C (eds) Proceedings 5th GandALF 2014, EPTCS, vol 161, pp 60–73MathSciNetCrossRef Faymonville P, Zimmermann M (2014) Parametric linear dynamic logic. In: Peron A, Piazza C (eds) Proceedings 5th GandALF 2014, EPTCS, vol 161, pp 60–73MathSciNetCrossRef
22.
go back to reference Filliâtre J, Conchon S (2006) Type-safe modular hash-consing. In: Kennedy A, Pottier F (eds) ACM workshop on ML. ACM, New York, pp 12–19 Filliâtre J, Conchon S (2006) Type-safe modular hash-consing. In: Kennedy A, Pottier F (eds) ACM workshop on ML. ACM, New York, pp 12–19
23.
24.
go back to reference Furia CA, Spoletini P (2014) Bounded variability of metric temporal logic. In: Cesta A, Combi C, Laroussinie F (eds) TIME 2014. IEEE Computer Society, Washington, pp 155–163 Furia CA, Spoletini P (2014) Bounded variability of metric temporal logic. In: Cesta A, Combi C, Laroussinie F (eds) TIME 2014. IEEE Computer Society, Washington, pp 155–163
25.
go back to reference Gorostiaga F, Sánchez C (2018) Striver: stream runtime verification for real-time event-streams. In: Colombo C, Leucker M (eds) RV 2018, LNCS, vol 11237. Springer, New York, pp 282–298 Gorostiaga F, Sánchez C (2018) Striver: stream runtime verification for real-time event-streams. In: Colombo C, Leucker M (eds) RV 2018, LNCS, vol 11237. Springer, New York, pp 282–298
26.
go back to reference Gunadi H, Tiu A (2014) Efficient runtime monitoring with metric temporal logic: a case study in the Android operating system. In: Jones CB, Pihlajasaari P, Sun J (eds) FM 2014, LNCS, vol 8442. Springer, New York, pp 296–311CrossRef Gunadi H, Tiu A (2014) Efficient runtime monitoring with metric temporal logic: a case study in the Android operating system. In: Jones CB, Pihlajasaari P, Sun J (eds) FM 2014, LNCS, vol 8442. Springer, New York, pp 296–311CrossRef
27.
go back to reference Havelund K, Peled D, Ulus D (2018) DejaVu: a monitoring tool for first-order temporal logic. In: 3rd workshop on monitoring and testing of cyber-physical systems, MT@CPSWeek 2018, Porto, Portugal, April 10, 2018, pp 12–13 Havelund K, Peled D, Ulus D (2018) DejaVu: a monitoring tool for first-order temporal logic. In: 3rd workshop on monitoring and testing of cyber-physical systems, MT@CPSWeek 2018, Porto, Portugal, April 10, 2018, pp 12–13
28.
go back to reference Havelund K, Roşu G (2002) Synthesizing monitors for safety properties. In: Katoen J, Stevens P (eds) TACAS 2002, LNCS, vol 2280. Springer, New York, pp 342–356 Havelund K, Roşu G (2002) Synthesizing monitors for safety properties. In: Katoen J, Stevens P (eds) TACAS 2002, LNCS, vol 2280. Springer, New York, pp 342–356
29.
30.
go back to reference Ho H, Ouaknine J, Worrell J (2014) Online monitoring of metric temporal logic. In: Bonakdarpour B, Smolka SA (eds) RV 2014, LNCS, vol 8734. Springer, New York, pp 178–192 Ho H, Ouaknine J, Worrell J (2014) Online monitoring of metric temporal logic. In: Bonakdarpour B, Smolka SA (eds) RV 2014, LNCS, vol 8734. Springer, New York, pp 178–192
31.
go back to reference Kapoutsis CA (2005) Removing bidirectionality from nondeterministic finite automata. In: Jedrzejowicz J, Szepietowski A (eds) MFCS 2005, LNCS, vol 3618. Springer, New York, pp 544–555 Kapoutsis CA (2005) Removing bidirectionality from nondeterministic finite automata. In: Jedrzejowicz J, Szepietowski A (eds) MFCS 2005, LNCS, vol 3618. Springer, New York, pp 544–555
32.
go back to reference Koymans R (1990) Specifying real-time properties with metric temporal logic. Real-Time Syst 2(4):255–299CrossRef Koymans R (1990) Specifying real-time properties with metric temporal logic. Real-Time Syst 2(4):255–299CrossRef
33.
go back to reference Leucker M, Sánchez C (2007) Regular linear temporal logic. In: Jones CB, Liu Z, Woodcock J (eds) ICTAC 2007, LNCS, vol 4711. Springer, New York, pp 291–305 Leucker M, Sánchez C (2007) Regular linear temporal logic. In: Jones CB, Liu Z, Woodcock J (eds) ICTAC 2007, LNCS, vol 4711. Springer, New York, pp 291–305
34.
go back to reference Leucker M, Sánchez C, Scheffel T, Schmitz M, Schramm A (2018) Tessla: runtime verification of non-synchronized real-time streams. In: Haddad HM, Wainwright RL, Chbeir R (eds) SAC 2018. ACM, New York, pp 1925–1933 Leucker M, Sánchez C, Scheffel T, Schmitz M, Schramm A (2018) Tessla: runtime verification of non-synchronized real-time streams. In: Haddad HM, Wainwright RL, Chbeir R (eds) SAC 2018. ACM, New York, pp 1925–1933
35.
go back to reference Maler O, Nickovic D, Pnueli A (2005) Real time temporal logic: past, present, future. In: Pettersson P, Yi W (eds) FORMATS 2005, LNCS, vol 3829. Springer, New York, pp 2–16 Maler O, Nickovic D, Pnueli A (2005) Real time temporal logic: past, present, future. In: Pettersson P, Yi W (eds) FORMATS 2005, LNCS, vol 3829. Springer, New York, pp 2–16
36.
go back to reference McAfee A, Brynjolfsson E (2012) Big data: the management revolution. Harv Bus Rev 90(10):61–67 McAfee A, Brynjolfsson E (2012) Big data: the management revolution. Harv Bus Rev 90(10):61–67
37.
go back to reference Pous D (2015) Symbolic algorithms for language equivalence and Kleene algebra with tests. In: Walker D (ed) POPL 2015. ACM, New York, pp 357–368 Pous D (2015) Symbolic algorithms for language equivalence and Kleene algebra with tests. In: Walker D (ed) POPL 2015. ACM, New York, pp 357–368
38.
go back to reference Sánchez C, Leucker M (2010) Regular linear temporal logic with past. In: Barthe G, Hermenegildo MV (eds) VMCAI 2010, LNCS, vol 5944. Springer, New York, pp 295–311 Sánchez C, Leucker M (2010) Regular linear temporal logic with past. In: Barthe G, Hermenegildo MV (eds) VMCAI 2010, LNCS, vol 5944. Springer, New York, pp 295–311
40.
go back to reference Thati P, Roşu G (2005) Monitoring algorithms for metric temporal logic specifications. Electron Notes Theor Comput Sci 113:145–162CrossRef Thati P, Roşu G (2005) Monitoring algorithms for metric temporal logic specifications. Electron Notes Theor Comput Sci 113:145–162CrossRef
42.
go back to reference Ulus D, Ferrère T, Asarin E, Maler O (2014) Timed pattern matching. In: Legay A, Bozga M (eds) FORMATS 2014, LNCS, vol 8711. Springer, New York, pp 222–236 Ulus D, Ferrère T, Asarin E, Maler O (2014) Timed pattern matching. In: Legay A, Bozga M (eds) FORMATS 2014, LNCS, vol 8711. Springer, New York, pp 222–236
43.
go back to reference Ulus D, Ferrère T, Asarin E, Maler O (2016) Online timed pattern matching using derivatives. In: Chechik M, Raskin JF (eds) TACAS 2016, LNCS, vol 9636. Springer, New York, pp 736–751 Ulus D, Ferrère T, Asarin E, Maler O (2016) Online timed pattern matching using derivatives. In: Chechik M, Raskin JF (eds) TACAS 2016, LNCS, vol 9636. Springer, New York, pp 736–751
44.
go back to reference Vardi MY (2008) From church and prior to PSL. In: Grumberg O, Veith H (eds) 25 Years of model checking—history, achievements, perspectives, LNCS, vol 5000. Springer, New York, pp 150–171CrossRef Vardi MY (2008) From church and prior to PSL. In: Grumberg O, Veith H (eds) 25 Years of model checking—history, achievements, perspectives, LNCS, vol 5000. Springer, New York, pp 150–171CrossRef
Metadata
Title
Almost event-rate independent monitoring
Authors
David Basin
Bhargav Nagaraja Bhatt
Srđan Krstić
Dmitriy Traytel
Publication date
06-02-2019
Publisher
Springer US
Published in
Formal Methods in System Design / Issue 3/2019
Print ISSN: 0925-9856
Electronic ISSN: 1572-8102
DOI
https://doi.org/10.1007/s10703-018-00328-3

Other articles of this Issue 3/2019

Formal Methods in System Design 3/2019 Go to the issue

Premium Partner