From Statistical Model Checking to Run-Time Monitoring Using a Bayesian Network Approach

Manfred Jaeger, Kim G Larsen, Alessandro Tibo

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

48 Downloads (Pure)


We propose a framework for monitoring and updating, at run-time, the probabilities of temporal properties of stochastic timed automata. Our method is based on Bayesian networks and can be useful in various real-time applications, such as flight control systems and cardiac pacemakers. The framework has been implemented by exploiting the statistical model checking engine of. By run-time monitoring a set of interesting temporal properties of a given stochastic automaton we update their probabilities, modeled through a Bayesian Network. The main advantages of our method are the capacity to discover non-trivial dependencies between properties and to efficiently update probabilities of unobserved properties given real-time observations. We present empirical results on three application scenarios, showing that the query time can keep up with the speed of some realistic real-time applications. We also present experiments demonstrating that the Bayesian Network approach performance-wise enables run-time monitoring while maintaining or even increasing the accuracy of probability estimation compared to statistical model checking.

Original languageEnglish
Title of host publicationRuntime Verification - 20th International Conference, RV 2020, Proceedings
EditorsJyotirmoy Deshmukh, Dejan Nickovic
Number of pages19
PublisherSpringer Science+Business Media
Publication date2020
ISBN (Print)978-3-030-60507-0
ISBN (Electronic)978-3-030-60508-7
Publication statusPublished - 2020
EventRV 2020: International Conference on Runtime Verification - Los Angeles, United States
Duration: 6 Oct 20209 Oct 2020


ConferenceRV 2020: International Conference on Runtime Verification
Country/TerritoryUnited States
CityLos Angeles
SeriesLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12399 LNCS

Bibliographical note

Publisher Copyright:
© 2020, Springer Nature Switzerland AG.

Copyright 2020 Elsevier B.V., All rights reserved.


  • Bayesian networks
  • Statistical model checking
  • Timed automata


Dive into the research topics of 'From Statistical Model Checking to Run-Time Monitoring Using a Bayesian Network Approach'. Together they form a unique fingerprint.

Cite this