Please use this identifier to cite or link to this item:
Title: Symbolic Model Checking for Factored Probabilistic Models
Authors: Deininger, David
Dimitrova, Rayna
Majumdar, Rupak
First Published: 22-Sep-2016
Presented at: 14th International Symposium on Automated Technology for Verification and Analysis (ATVA), Chiba, JAPAN
Start Date: 17-Oct-2016
End Date: 20-Oct-2016
Publisher: Springer International Publishing AG
Citation: International Symposium on Automated Technology for Verification and Analysis ATVA 2016: Automated Technology for Verification and Analysis, Lecture Notes in Computer Science, 2016, 9938.
Abstract: The long line of research in probabilistic model checking has resulted in efficient symbolic verification engines. Nevertheless, scalability is still a key concern. In this paper we ask two questions. First, can we lift, to the probabilistic world, successful hardware verification techniques that exploit local variable dependencies in the analyzed model? And second, will those techniques lead to significant performance improvement on models with such structure, such as dynamic Bayesian networks? To the first question we give a positive answer by proposing a probabilistic model checking approach based on factored symbolic representation of the transition probability matrix of the analyzed model. Our experimental evaluation on several benchmarks designed to favour this approach answers the second question negatively. Intuitively, the reason is that the effect of techniques for reducing the size of BDD-based symbolic representations do not carry over to quantitative symbolic data structures. More precisely, the size of MTBDDs depends not only on the number of variables but also on the number of different terminals they have (which influences sharing), and which is not reduced by these techniques.
Series/Report no.: Lecture Notes in Computer Science book series (LNCS);9938
DOI Link: 10.1007/978-3-319-46520-3_28
ISSN: 0302-9743
ISBN: 978-3-319-46519-7
Version: Post-print
Status: Peer-reviewed
Type: Conference Paper
Rights: Copyright © 2016, Springer International Publishing AG. Deposited with reference to the publisher’s open access archiving policy. (
Appears in Collections:Conference Papers & Presentations, Dept. of Computer Science

Files in This Item:
File Description SizeFormat 
atva16.pdfPost-review (final submitted author manuscript)404.75 kBAdobe PDFView/Open

Items in LRA are protected by copyright, with all rights reserved, unless otherwise indicated.