Jansen, N;
Dehnert, C;
Kaminski, BL;
Katoen, J-P;
Westhofen, L;
(2016)
Bounded Model Checking for Probabilistic Programs.
In: Artho, C and Legay, A and Peled, D, (eds.)
Automated Technology for Verification and Analysis: 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings.
(pp. pp. 68-85).
Springer: Cham, Switzerland.
Preview |
Text
main.pdf - Accepted Version Download (501kB) | Preview |
Abstract
In this paper we investigate the applicability of standard model checking approaches to verifying properties in probabilistic programming. As the operational model for a standard probabilistic program is a potentially infinite parametric Markov decision process, no direct adaption of existing techniques is possible. Therefore, we propose an on–the–fly approach where the operational model is successively created and verified via a step–wise execution of the program. This approach enables to take key features of many probabilistic programs into account: nondeterminism and conditioning. We discuss the restrictions and demonstrate the scalability on several benchmarks.
| Type: | Proceedings paper |
|---|---|
| Title: | Bounded Model Checking for Probabilistic Programs |
| Event: | 14th International Symposium on Automated Technology for Verification and Analysis (ATVA) |
| Location: | Chiba, JAPAN |
| Dates: | 17 October 2016 - 20 October 2016 |
| ISBN-13: | 978-3-319-46519-7 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1007/978-3-319-46520-3_5 |
| Publisher version: | https://doi.org/10.1007/978-3-319-46520-3_5 |
| Language: | English |
| Additional information: | This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions. |
| Keywords: | Model Check, Markov Decision Process, Operational Semantic, Program Variable, Probabilistic Program |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10089696 |
Archive Staff Only
 |
View Item |
