Abstract
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 language | English |
---|---|
Title of host publication | Runtime Verification - 20th International Conference, RV 2020, Proceedings |
Editors | Jyotirmoy Deshmukh, Dejan Nickovic |
Number of pages | 19 |
Publisher | Springer Science+Business Media |
Publication date | 2020 |
Pages | 517-535 |
ISBN (Print) | 978-3-030-60507-0 |
ISBN (Electronic) | 978-3-030-60508-7 |
DOIs | |
Publication status | Published - 2020 |
Event | RV 2020: International Conference on Runtime Verification - Los Angeles, United States Duration: 6 Oct 2020 → 9 Oct 2020 |
Conference
Conference | RV 2020: International Conference on Runtime Verification |
---|---|
Country/Territory | United States |
City | Los Angeles |
Period | 06/10/2020 → 09/10/2020 |
Series | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Volume | 12399 LNCS |
ISSN | 0302-9743 |
Bibliographical note
Publisher Copyright:© 2020, Springer Nature Switzerland AG.
Copyright:
Copyright 2020 Elsevier B.V., All rights reserved.
Keywords
- Bayesian networks
- Statistical model checking
- Timed automata