Skip to main content
SpringerLink
Log in

Almost event-rate independent monitoring

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7

Similar content being viewed by others

References

  1. Antimirov V (1996) Partial derivatives of regular expressions and finite automaton constructions. Theor Comput Sci 155(2):291–319

    Article  MathSciNet  Google Scholar 

  2. Asarin E, Caspi P, Maler O (2002) Timed regular expressions. J ACM 49(2):172–206

    Article  MathSciNet  Google Scholar 

  3. 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

    Google Scholar 

  4. Basin DA, Klaedtke F, Zălinescu E (2017) Algorithms for monitoring real-time properties. Acta Inf 55:309–338

    Article  MathSciNet  Google Scholar 

  5. 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

    Google Scholar 

  6. 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

    Google Scholar 

  7. 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

    Google Scholar 

  8. 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

    Google Scholar 

  9. Basin DA, Klaedtke F, Müller S, Zălinescu E (2015) Monitoring metric first-order temporal properties. J ACM 62(2):15:1–15:45

    Article  MathSciNet  Google Scholar 

  10. 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

    Google Scholar 

  11. 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

    Google Scholar 

  12. Bouyer P, Chevalier F, Markey N (2010) On the expressiveness of TPTL and MTL. Inf Comput 208(2):97–116

    Article  MathSciNet  Google Scholar 

  13. Brzozowski JA (1964) Derivatives of regular expressions. J ACM 11(4):481–494

    Article  MathSciNet  Google Scholar 

  14. 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. Dax C, Klaedtke F, Lange M (2010) On regular temporal logics with past. Acta Inf 47(4):251–277

    Article  Google Scholar 

  16. 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. 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

    Google Scholar 

  18. 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

    Google Scholar 

  19. 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

    Google Scholar 

  20. Faymonville P, Zimmermann M (2014) Parametric linear dynamic logic. In: Peron A, Piazza C (eds) Proceedings 5th GandALF 2014, EPTCS, vol 161, pp 60–73

    Article  MathSciNet  Google Scholar 

  21. Faymonville P, Zimmermann M (2017) Parametric linear dynamic logic. Inf Comput 253:237–256

    Article  MathSciNet  Google Scholar 

  22. 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

    Google Scholar 

  23. Fischer MJ, Ladner RE (1979) Propositional dynamic logic of regular programs. J Comput Syst Sci 18(2):194–211

    Article  MathSciNet  Google Scholar 

  24. 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

    Google Scholar 

  25. 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

    Google Scholar 

  26. 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–311

    Chapter  Google Scholar 

  27. 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. 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

    Google Scholar 

  29. Henriksen JG, Thiagarajan P (1999) Dynamic linear time temporal logic. Ann Pure Appl Log 96(1):187–207

    Article  MathSciNet  Google Scholar 

  30. 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

    Google Scholar 

  31. 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

    Google Scholar 

  32. Koymans R (1990) Specifying real-time properties with metric temporal logic. Real-Time Syst 2(4):255–299

    Article  Google Scholar 

  33. 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

    Google Scholar 

  34. 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

    Google Scholar 

  35. 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

    Google Scholar 

  36. McAfee A, Brynjolfsson E (2012) Big data: the management revolution. Harv Bus Rev 90(10):61–67

    Google Scholar 

  37. 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

    Google Scholar 

  38. 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

    Google Scholar 

  39. Tange O (2011) GNU Parallel—the command-line power tool. login USENIX Mag 36(1):42–47. https://doi.org/10.5281/zenodo.16303. http://www.gnu.org/s/parallel

  40. Thati P, Roşu G (2005) Monitoring algorithms for metric temporal logic specifications. Electron Notes Theor Comput Sci 113:145–162

    Article  Google Scholar 

  41. Ulus D (2016) Montre: a tool for monitoring timed regular expressions. arXiv preprint arXiv:1605.05963

  42. 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

    Google Scholar 

  43. 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

    Google Scholar 

  44. 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–171

    Chapter  Google Scholar 

  45. Wolper P (1983) Temporal logic can be more expressive. Inf Control 56(1/2):72–99

    Article  MathSciNet  Google Scholar 

Download references

Acknowledgements

This research is supported by the Swiss National Science Foundation grant Big Data Monitoring (167162) and by the US Air Force grant Monitoring at Any Cost (FA9550-17-1-0306). The authors are listed alphabetically. Felix Klaedtke showed us an example property not expressible in MTL. Joshua Schneider participated in discussions about simplifying MDL’s syntax. Domenico Bianculli, Jasmin Blanchette, Joshua Schneider, and anonymous reviewers helped us to improve the presentation of this work.

Author information

Authors and Affiliations

  1. Institute of Information Security, Department of Computer Science, ETH Zürich, Zurich, Switzerland

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

Authors
  1. David Basin
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bhargav Nagaraja Bhatt
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Srđan Krstić
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Dmitriy Traytel
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Srđan Krstić or Dmitriy Traytel.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Basin, D., Bhatt, B.N., Krstić, S. et al. Almost event-rate independent monitoring. Form Methods Syst Des 54, 449–478 (2019). https://doi.org/10.1007/s10703-018-00328-3

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10703-018-00328-3

Keywords

Search

Navigation