{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T07:05:34Z","timestamp":1725865534276},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319465197"},{"type":"electronic","value":"9783319465203"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-46520-3_28","type":"book-chapter","created":{"date-parts":[[2016,9,21]],"date-time":"2016-09-21T10:40:27Z","timestamp":1474454427000},"page":"444-460","source":"Crossref","is-referenced-by-count":2,"title":["Symbolic Model Checking for Factored Probabilistic Models"],"prefix":"10.1007","author":[{"given":"David","family":"Deininger","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rayna","family":"Dimitrova","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rupak","family":"Majumdar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,9,22]]},"reference":[{"key":"28_CR1","doi-asserted-by":"crossref","unstructured":"Bahar, R.I., Frohm, E.A., Gaona, C.M., Hachtel, G.D., Macii, E., Pardo, A., Somenzi, F.: Algebraic decision diagrams and their applications. In: Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design, ICCAD 1993, pp. 188\u2013191 (1993)","DOI":"10.1109\/ICCAD.1993.580054"},{"key":"28_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"430","DOI":"10.1007\/3-540-63165-8_199","volume-title":"Automata, Languages and Programming","author":"C Baier","year":"1997","unstructured":"Baier, C., Clarke, E.M., Hartonas-Garmhausen, V., Kwiatkowska, M., Ryan, M.: Symbolic model checking for probabilistic processes. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol. 1256, pp. 430\u2013440. Springer, Heidelberg (1997)"},{"key":"28_CR3","volume-title":"Principles of Model Checking (Representation and Mind Series)","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking (Representation and Mind Series). The MIT Press, Cambridge (2008)"},{"key":"28_CR4","unstructured":"Bruna, M., Grigore, R., Kiefer, S., Ouaknine, J., Worrell, J.: Proving the Herman-protocol conjecture (2015). CoRR, abs\/1504.01130"},{"issue":"8","key":"28_CR5","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C\u201335","author":"R Bryant","year":"1986","unstructured":"Bryant, R.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. C\u201335(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"key":"28_CR6","doi-asserted-by":"crossref","unstructured":"Burch, J.R., Clarke, E.M., Long, D.E.: Representing circuits more efficiently in symbolic model checking. In: Proceedings of the 28th ACM\/IEEE Design Automation Conference, DAC 1991, pp. 403\u2013407. ACM (1991)","DOI":"10.1145\/127601.127702"},{"issue":"2","key":"28_CR7","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"JR Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Inf. Comput. 98(2), 142\u2013170 (1992)","journal-title":"Inf. Comput."},{"key":"28_CR8","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., McMillan, K.L., Zhao, X., Fujita, M., Yang, J.: Spectral transforms for large Boolean functions with applications to technology mapping. In: DAC, pp. 54\u201360 (1993)","DOI":"10.1145\/157485.164569"},{"key":"28_CR9","doi-asserted-by":"crossref","unstructured":"Demaille, A., Peyronnet, S., Sigoure, B.: Modeling of sensor networks using XRM. In: Second International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2006, pp. 271\u2013276, November 2006","DOI":"10.1109\/ISoLA.2006.27"},{"issue":"2","key":"28_CR10","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1023\/A:1008647823331","volume":"10","author":"M Fujita","year":"1997","unstructured":"Fujita, M., McGeer, P.C., Yang, J.C.-Y.: Multi-terminal binary decision diagrams: an efficient data structure for matrix representation. Formal Methods Syst. Des. 10(2), 149\u2013169 (1997)","journal-title":"Formal Methods Syst. Des."},{"issue":"2","key":"28_CR11","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1016\/0020-0190(90)90107-9","volume":"35","author":"T Herman","year":"1990","unstructured":"Herman, T.: Probabilistic self-stabilization. Inf. Process. Lett. 35(2), 63\u201367 (1990)","journal-title":"Inf. Process. Lett."},{"key":"28_CR12","unstructured":"Hermanns, H., Meyer-Kayser, J., Siegle, M.: Multi terminal binary decision diagrams to represent and analyse continuous time Markov chains. In: 3rd International Workshop on the Numerical Solutions of Markov Chains, NSMC 1999, pp. 188\u2013207 (1999)"},{"key":"28_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011)"},{"key":"28_CR14","unstructured":"Langmead, C.J., Jha, S.K., Clarke, E.M.: Temporal-logics as query languages for dynamic Bayesian networks: application to D. melanogaster embryo development (2006)"},{"key":"28_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1007\/978-3-642-33386-6_2","volume-title":"Automated Technology for Verification and Analysis","author":"SK Palaniappan","year":"2012","unstructured":"Palaniappan, S.K., Thiagarajan, P.S.: Dynamic Bayesian networks: a factored model of probabilistic dynamics. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 17\u201325. Springer, Heidelberg (2012)"},{"key":"28_CR16","unstructured":"Parker, D.: Implementation of symbolic model checking for probabilistic systems. Ph.D. thesis, University of Birmingham (2002)"},{"key":"28_CR17","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1016\/j.cosrev.2015.03.001","volume":"15","author":"E Ruijters","year":"2015","unstructured":"Ruijters, E., Stoelinga, M.: Fault tree analysis: a survey of the state-of-the-art in modeling, analysis and tools. Comput. Sci. Rev. 15, 29\u201362 (2015)","journal-title":"Comput. Sci. Rev."},{"key":"28_CR18","unstructured":"Somenzi, F.: CUDD: BDD package, University of Colorado, Boulder. http:\/\/vlsi.colorado.edu\/~fabio\/CUDD\/"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-46520-3_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T23:19:52Z","timestamp":1498346392000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-46520-3_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319465197","9783319465203"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-46520-3_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}