Document Open Access Logo

Monitoring Event Frequencies

Authors Thomas Ferrère , Thomas A. Henzinger , Bernhard Kragl

PDF
Thumbnail PDF

File

LIPIcs.CSL.2020.20.pdf
  • Filesize: 0.56 MB
  • 16 pages

Document Identifiers

Author Details

Thomas Ferrère
  • IST Austria, Klosterneuburg, Austria
Thomas A. Henzinger
  • IST Austria, Klosterneuburg, Austria
Bernhard Kragl
  • IST Austria, Klosterneuburg, Austria

Funding

This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award).

Acknowledgements

We thank Jan Maas for showing us a simple proof of convergence of the mode in the i.i.d. case, and Zbigniew S. Szewczak for pointing out to us the use of Karamata’s Tauberian theorem in connection with ergodic theory [Zbigniew S. Szewczak, 2008].

Cite As Get BibTex

Thomas Ferrère, Thomas A. Henzinger, and Bernhard Kragl. Monitoring Event Frequencies. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 20:1-20:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.CSL.2020.20

Abstract

The monitoring of event frequencies can be used to recognize behavioral anomalies, to identify trends, and to deduce or discard hypotheses about the underlying system. For example, the performance of a web server may be monitored based on the ratio of the total count of requests from the least and most active clients. Exact frequency monitoring, however, can be prohibitively expensive; in the above example it would require as many counters as there are clients. In this paper, we propose the efficient probabilistic monitoring of common frequency properties, including the mode (i.e., the most common event) and the median of an event sequence. We define a logic to express composite frequency properties as a combination of atomic frequency properties. Our main contribution is an algorithm that, under suitable probabilistic assumptions, can be used to monitor these important frequency properties with four counters, independent of the number of different events. Our algorithm samples longer and longer subwords of an infinite event sequence. We prove the almost-sure convergence of our algorithm by generalizing ergodic theory from increasing-length prefixes to increasing-length subwords of an infinite sequence. A similar algorithm could be used to learn a connected Markov chain of a given structure from observing its outputs, to arbitrary precision, for a given confidence.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Software organization and properties
  • Theory of computation → Randomness, geometry and discrete structures
Keywords
  • monitoring
  • frequency property
  • Markov chain

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Gul Agha and Karl Palmskog. A Survey of Statistical Model Checking. ACM Trans. Model. Comput. Simul., 28(1):6:1-6:39, 2018. URL: https://doi.org/10.1145/3158668.
  2. Rajeev Alur, Dana Fisman, and Mukund Raghothaman. Regular Programming for Quantitative Properties of Data Streams. In ESOP, volume 9632 of Lecture Notes in Computer Science, pages 15-40. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49498-1_2.
  3. Howard Barringer, Yliès Falcone, Klaus Havelund, Giles Reger, and David E. Rydeheard. Quantified Event Automata: Towards Expressive and Efficient Runtime Monitors. In FM, volume 7436 of Lecture Notes in Computer Science, pages 68-84. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-32759-9_9.
  4. Ezio Bartocci and Yliès Falcone, editors. Lectures on Runtime Verification - Introductory and Advanced Topics, volume 10457 of Lecture Notes in Computer Science. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-75632-5.
  5. Manuel Blum, Robert W. Floyd, Vaughan R. Pratt, Ronald L. Rivest, and Robert Endre Tarjan. Time Bounds for Selection. J. Comput. Syst. Sci., 7(4):448-461, 1973. URL: https://doi.org/10.1016/S0022-0000(73)80033-9.
  6. Taylor L. Booth. Statistical Properties of Random Digital Sequences. IEEE Trans. Computers, 17(5):452-461, 1968. URL: https://doi.org/10.1109/TC.1968.226909.
  7. Krishnendu Chatterjee, Thomas A. Henzinger, and Jan Otop. Quantitative Monitor Automata. In SAS, volume 9837 of Lecture Notes in Computer Science, pages 23-38. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-53413-7_2.
  8. Ben D'Angelo, Sriram Sankaranarayanan, César Sánchez, Will Robinson, Bernd Finkbeiner, Henny B. Sipma, Sandeep Mehrotra, and Zohar Manna. LOLA: runtime monitoring of synchronous systems. In TIME, pages 166-174. IEEE Computer Society, 2005. URL: https://doi.org/10.1109/TIME.2005.26.
  9. Peter Faymonville, Bernd Finkbeiner, Maximilian Schwenger, and Hazem Torfah. Real-time Stream-based Monitoring, 2019. URL: http://arxiv.org/abs/1711.03829v4.
  10. Thomas Ferrère, Thomas A. Henzinger, and N. Ege Saraç. A Theory of Register Monitors. In LICS, pages 394-403. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209194.
  11. Patrick C. Fischer, Albert R. Meyer, and Arnold L. Rosenberg. Counter Machines and Counter Languages. Mathematical Systems Theory, 2(3):265-283, 1968. URL: https://doi.org/10.1007/BF01694011.
  12. Thomas A. Henzinger. Quantitative reactive modeling and verification. Computer Science - R&D, 28(4):331-344, 2013. URL: https://doi.org/10.1007/s00450-013-0251-7.
  13. C. A. R. Hoare. Algorithm 65: find. Commun. ACM, 4(7):321-322, 1961. URL: https://doi.org/10.1145/366622.366647.
  14. Tien-Chung Hu, F Moricz, and R Taylor. Strong laws of large numbers for arrays of rowwise independent random variables. Acta Mathematica Hungarica, 54(1-2):153-162, 1989. URL: https://doi.org/10.1007/BF01950716.
  15. Marta Kwiatkowska. Quantitative verification: models techniques and tools. In ESEC/SIGSOFT FSE, pages 449-458. ACM, 2007. URL: https://doi.org/10.1145/1287624.1287688.
  16. Marta Kwiatkowska, Gethin Norman, and David Parker. Probabilistic Model Checking: Advances and Applications. In Rolf Drechsler, editor, Formal System Verification: State-of the-Art and Future Trends, pages 73-121. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-57685-5_3.
  17. David A. Levin, Yuval Peres, and Elizabeth L. Wilmer. Markov Chains and Mixing Times, second edition, 2017. URL: https://pages.uoregon.edu/dlevin/MARKOV/mcmt2e.pdf.
  18. Michael Mitzenmacher and Eli Upfal. Probability and Computing: Randomized Algorithms and Probabilistic Analysis. Cambridge University Press, 2005. URL: https://doi.org/10.1017/CBO9780511813603.
  19. James R. Norris. Markov Chains. Cambridge Series in Statistical and Probabilistic Mathematics. Cambridge University Press, 1998. Google Scholar
  20. Dana Ron. Automata Learning and its Applications. PhD thesis, Hebrew University, 1995. URL: http://www.cs.huji.ac.il/labs/learning/Theses/Dana_Ron_PhD.pdf.
  21. Steven Rudich. Inferring the Structure of a Markov Chain from its Output. In FOCS, pages 321-326. IEEE Computer Society, 1985. URL: https://doi.org/10.1109/SFCS.1985.34.
  22. Usa Sammapun, Insup Lee, and Oleg Sokolsky. RT-MaC: Runtime monitoring and checking of quantitative and probabilistic properties. In RTCSA, pages 147-153. IEEE Computer Society, 2005. URL: https://doi.org/10.1109/RTCSA.2005.84.
  23. Zbigniew S. Szewczak. On moments of recurrence times for positive recurrent renewal sequences. Statistics & Probability Letters, 78(17):3086-3090, 2008. URL: https://doi.org/10.1016/j.spl.2008.05.013.
  24. B. P. Welford. Note on a Method for Calculating Corrected Sums of Squares and Products. Technometrics, 4(3):419-420, 1962. URL: https://doi.org/10.1080/00401706.1962.10490022.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact