Document Open Access Logo

Selective Monitoring

Authors Radu Grigore , Stefan Kiefer



PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2018.20.pdf
  • Filesize: 0.52 MB
  • 16 pages

Document Identifiers

Author Details

Radu Grigore
  • University of Kent, UK
Stefan Kiefer
  • University of Oxford, UK

Cite AsGet BibTex

Radu Grigore and Stefan Kiefer. Selective Monitoring. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 20:1-20:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.CONCUR.2018.20

Abstract

We study selective monitors for labelled Markov chains. Monitors observe the outputs that are generated by a Markov chain during its run, with the goal of identifying runs as correct or faulty. A monitor is selective if it skips observations in order to reduce monitoring overhead. We are interested in monitors that minimize the expected number of observations. We establish an undecidability result for selectively monitoring general Markov chains. On the other hand, we show for non-hidden Markov chains (where any output identifies the state the Markov chain is in) that simple optimal monitors exist and can be computed efficiently, based on DFA language equivalence. These monitors do not depend on the precise transition probabilities in the Markov chain. We report on experiments where we compute these monitors for several open-source Java projects.

Subject Classification

ACM Subject Classification
  • Theory of computation → Randomness, geometry and discrete structures
Keywords
  • runtime monitoring
  • probabilistic systems
  • Markov chains
  • automata
  • language equivalence

Metrics

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

References

  1. Matthew Arnold, Martin T. Vechev, and Eran Yahav. QVM: an efficient runtime for detecting defects in deployed systems. In OOPSLA, 2008. Google Scholar
  2. C. Baier and J.-P. Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  3. Ezio Bartocci, Radu Grosu, Atul Karmarkar, Scott A. Smolka, Scott D. Stoller, Erez Zadok, and Justin Seyster. Adaptive runtime verification. In RV, 2012. Google Scholar
  4. N. Bertrand, S. Haddad, and E. Lefaucheux. Foundation of diagnosis and predictability in probabilistic systems. In Proceedings of FSTTCS, volume 29 of LIPIcs, pages 417-429, 2014. Google Scholar
  5. N. Bertrand, S. Haddad, and E. Lefaucheux. Accurate approximate diagnosability of stochastic systems. In Proceedings of LATA, pages 549-561. Springer, 2016. Google Scholar
  6. Laura Bocchi, Tzu-Chun Chen, Romain Demangeon, Kohei Honda, and Nobuko Yoshida. Monitoring networks through multiparty session types. TCS, 2017. Google Scholar
  7. Mikołaj Bojánczyk, Bartek Klin, and Sławomir Lasota. Automata theory in nominal sets. LMCS, 2014. Google Scholar
  8. C. Calcagno, D. Distefano, J. Dubreil, D. Gabi, P. Hooimeijer, M. Luca, P. O'Hearn, I. Papakonstantinou, J. Purbrick, and D. Rodriguez. Moving fast with software verification. In NASA Formal Methods Symposium, 2015. Google Scholar
  9. C. Calcagno, D. Distefano, P.W. O'Hearn, and H. Yang. Compositional shape analysis by means of bi-abduction. JACM, 2011. Google Scholar
  10. Loris D'Antoni and Margus Veanes. The power of symbolic automata and transducers. In CAV, 2017. Google Scholar
  11. Stéphane Demri and Ranko Lazić. LTL with the freeze quantifier and register automata. TOCL, 2009. Google Scholar
  12. Gurobi Optimization, Inc. Gurobi optimizer reference manual. http://www.gurobi.com, 2017.
  13. Klaus Havelund, Martin Leucker, Giles Reger, and Volker Stolz. A Shared Challenge in Behavioural Specification (Dagstuhl Seminar 17462). Dagstuhl Reports, 2018. URL: http://dx.doi.org/10.4230/DagRep.7.11.59.
  14. S. Jiang, Z. Huang, V. Chandra, and R. Kumar. A polynomial algorithm for testing diagnosability of discrete-event systems. IEEE Transactions on Automatic Control, 46(8):1318-1321, 2001. Google Scholar
  15. K. Kalajdzic, E. Bartocci, S.A. Smolka, S.D. Stoller, and R. Grosu. Runtime verification with particle filtering. In RV, 2013. Google Scholar
  16. J.-Y. Kao, N. Rampersad, and J. Shallit. On NFAs where all states are final, initial, or both. Theoretical Computer Science, 410(47):5010-5021, 2009. Google Scholar
  17. Brian G. Leroux. Maximum-likelihood estimation for hidden markov models. Stochastic Processes and Their Applications, 1992. Google Scholar
  18. Grigore Rosu and Feng Chen. Semantics and algorithms for parametric monitoring. LMCS, 2012. Google Scholar
  19. M. Sampath, R. Sengupta, S. Lafortune, K. Sinnamohideen, and D. Teneketzis. Diagnosability of discrete-event systems. IEEE Transactions on Automatic Control, 40(9):1555-1575, 1995. Google Scholar
  20. A. Prasad Sistla, Miloš Žefran, and Yao Feng. Monitorability of stochastic dynamical systems. In Proceedings of CAV, pages 720-736. Springer, 2011. Google Scholar
  21. S.D. Stoller, E. Bartocci, J. Seyster, R. Grosu, K. Havelund, S.A. Smolka, and E. Zadok. Runtime verification with state estimation. In RV, 2011. Google Scholar
  22. D. Thorsley and D. Teneketzis. Diagnosability of stochastic discrete-event systems. IEEE Transactions on Automatic Control, 50(4):476-492, 2005. Google Scholar
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