{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:30:40Z","timestamp":1761597040327,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540672821"},{"type":"electronic","value":"9783540464198"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-46419-0_27","type":"book-chapter","created":{"date-parts":[[2007,8,8]],"date-time":"2007-08-08T23:17:25Z","timestamp":1186615045000},"page":"395-410","source":"Crossref","is-referenced-by-count":56,"title":["Symbolic Model Checking of Probabilistic Processes Using MTBDDs and the Kronecker Representation"],"prefix":"10.1007","author":[{"given":"Luca","family":"de Alfaro","sequence":"first","affiliation":[]},{"given":"Marta","family":"Kwiatkowska","sequence":"additional","affiliation":[]},{"given":"Gethin","family":"Norman","sequence":"additional","affiliation":[]},{"given":"David","family":"Parker","sequence":"additional","affiliation":[]},{"given":"Roberto","family":"Segala","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,6,1]]},"reference":[{"issue":"2\/3","key":"27_CR1","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1023\/A:1008699807402","volume":"10","author":"I. Bahar","year":"1997","unstructured":"I. Bahar, E. Frohm, C. Gaona, G. Hachtel, E. Macii, A. Pardo, and F. Somenzi. Algebraic Decision Diagrams and their Applications. Journal of Formal Methods in Systems Design, 10(2\/3):171\u2013206, 1997. 396, 397, 401, 405","journal-title":"Journal of Formal Methods in Systems Design"},{"key":"27_CR2","unstructured":"C. Baier. On algorithmic verification methods for probabilistic systems. Habilitation thesis, 1998. 396, 397, 399, 400, 401"},{"key":"27_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"430","DOI":"10.1007\/3-540-63165-8_199","volume-title":"Proceedings, 24th ICALP","author":"C. Baier","year":"1997","unstructured":"C. Baier, E. Clarke, V. Hartonas-Garmhausen, M. Kwiatkowska, and M. Ryan. Symbolic model checking for probabilistic processes. In Proceedings, 24th ICALP, volume 1256 of LNCS, pages 430\u2013440. Springer-Verlag, 1997. 396, 397, 401"},{"key":"27_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1007\/3-540-48320-9_12","volume-title":"CONCUR\u201999","author":"C. Baier","year":"1999","unstructured":"C. Baier, J.-P. Katoen, and H. Hermanns. Approximate symbolic model checking of continuous-time Markov chains. In CONCUR\u201999, volume 1664 of LNCS, pages 146\u2013161. Springer-Verlag, 1999. 396, 407"},{"key":"27_CR5","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/s004460050046","volume":"11","author":"C. Baier","year":"1998","unstructured":"C. Baier and M. Kwiatkowska. Model checking for a probabilistic branching time logic with fairness. Distributed Computing, 11:125\u2013155, 1998. 396, 397, 398, 399, 400","journal-title":"Distributed Computing"},{"key":"27_CR6","unstructured":"J. Bengtsson, K. G. Larsen, F. Larsson, P. Pettersson, W. Yi, and C. Weise. New generation of uppaal. In Proceedings of the International Workshop on Software Tools for Technology Transfer, Aalborg, Denmark, July 1998. 396"},{"key":"27_CR7","unstructured":"D. Bertsekas. Dynamic Programming and Optimal Control. Athena Scientific, 1995. 396"},{"key":"27_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1007\/3-540-60692-0_70","volume-title":"Proceedings, FST&TCS","author":"A. Bianco","year":"1995","unstructured":"A. Bianco and L. de Alfaro. Model checking of probabilistic and nondeterministic systems. In Proceedings, FST&TCS, volume 1026 of LNCS, pages 499\u2013513. Springer-Verlag, 1995. 396, 398, 399"},{"key":"27_CR9","series-title":"Lect Notes Comput Sci","volume-title":"Proc. CAV\u201999","author":"M. Bozga","year":"1999","unstructured":"M. Bozga and O. Maler. On the representation of probabilities over structured domains. In Proc. CAV\u201999, 1999. Available as Volume 1633 of LNCS. 396, 407"},{"key":"27_CR10","unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond. In LICS\u201990, June 1990. 395"},{"key":"27_CR11","unstructured":"G. Ciardo and A. Miner. SMART: Simulation and markovian analyzer for reliability and timing. In Tools Descriptions from PNPM\u201997, pages 41\u201343, 1997. 397"},{"key":"27_CR12","doi-asserted-by":"crossref","unstructured":"G. Ciardo and A. Miner. A data structure for the efficient Kronecker solution of GSPNs. In Proc. PNPM\u201999, 1999. 406, 407","DOI":"10.1109\/PNPM.1999.796529"},{"key":"27_CR13","doi-asserted-by":"crossref","unstructured":"E. Clarke, E. Emerson, and A. Sistla. Automatic verification of finite state concurrent systems using temporal logic specifications: A practical approach. In Proceedings, 10th Annual Symp. on Principles of Programming Languages, 1983. 398, 399","DOI":"10.1145\/567067.567080"},{"key":"27_CR14","unstructured":"E. Clarke, M. Fujita, P. McGeer, J. Yang, and X. Zhao. Multi-Terminal Binary Decision Diagrams: An Efficient Data Structure for Matrix Representation. In International Workshop on Logic Synthesis, 1993. 396, 401, 405"},{"key":"27_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"336","DOI":"10.1007\/BFb0032043","volume-title":"Proc. ICALP\u201990","author":"C. Courcoubetis","year":"1990","unstructured":"C. Courcoubetis and M. Yannakakis. Markov decision processes and regular events. In Proc. ICALP\u201990, volume 443 of LNCS, pages 336\u2013349. Springer-Verlag, 1990. 396, 400"},{"issue":"4","key":"27_CR16","doi-asserted-by":"publisher","first-page":"857","DOI":"10.1145\/210332.210339","volume":"42","author":"C. Courcoubetis","year":"1995","unstructured":"C. Courcoubetis and M. Yannakakis. The complexity of probabilistic verification. Journal of the ACM, 42(4):857\u2013907, 1995. 398, 400","journal-title":"Journal of the ACM"},{"key":"27_CR17","doi-asserted-by":"crossref","unstructured":"L. de Alfaro. How to specify and verify the long-run average behavior of probabilistic systems. In Proc. LICS\u201998, pages 454\u2013465, 1998. 396","DOI":"10.1109\/LICS.1998.705679"},{"key":"27_CR18","series-title":"Lect Notes Comput Sci","volume-title":"Proc. CONCUR\u201998","author":"L. Alfaro de","year":"1998","unstructured":"L. de Alfaro. Stochastic transition systems. In Proc. CONCUR\u201998, volume 1466 of LNCS. Springer-Verlag, 1998. 396"},{"key":"27_CR19","series-title":"Lect Notes Comput Sci","volume-title":"Proc. CONCUR\u201999","author":"L. Alfaro de","year":"1999","unstructured":"L. de Alfaro. Computing minimum and maximum reachability times in probabilistic systems. In Proc. CONCUR\u201999, volume 1664 of LNCS, 1999. 397, 400"},{"key":"27_CR20","doi-asserted-by":"crossref","unstructured":"L. de Alfaro. From fairness to chance. In Proc. PROBMIV\u201998, volume 21 of ENTCS. Elsevier, 1999. 398","DOI":"10.1016\/S1571-0661(05)80597-3"},{"issue":"12","key":"27_CR21","doi-asserted-by":"crossref","first-page":"1479","DOI":"10.1109\/43.552081","volume":"15","author":"G. Hachtel","year":"1996","unstructured":"G. Hachtel, E. Macii, A. Pardo, and F. Somenzi. Markovian Analysis of Large Finite State Machines. IEEE Transactions on CAD, 15(12):1479\u20131493, 1996. 397","journal-title":"IEEE Transactions on CAD"},{"key":"27_CR22","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H. Hansson","year":"1994","unstructured":"H. Hansson and B. Jonsson. A logic for reasoning about time and probability. Formal Aspects of Computing, 6:512\u2013535, 1994. 396, 398","journal-title":"Formal Aspects of Computing"},{"key":"27_CR23","unstructured":"H. Hermanns, J. Meyer-Kayser, and M. Siegle. Multi Terminal Binary Decision Diagrams to represent and analyse continuous time Markov chains. In Proc. NSMC\u201999, 1999. 397, 405"},{"key":"27_CR24","unstructured":"M. Kwiatkowska, G. Norman, D. Parker, and R. Segala. Symbolic model checking of concurrent probabilistic systems using MTBDDs and simplex. Technical Report CSR-99-1, University of Birmingham, 1999. 397"},{"key":"27_CR25","doi-asserted-by":"crossref","unstructured":"K. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993. 395","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"27_CR26","doi-asserted-by":"crossref","unstructured":"B. Plateau. On the Stochastic Structure of Parallelism and Synchronisation Models for Distributed Algorithms. In Proc. 1985 ACM SIGMETRICS Conference on Measurement and Modeling of Computer Systems, pages 147\u2013153, May 1985. 397, 402, 403","DOI":"10.1145\/317795.317819"},{"key":"27_CR27","doi-asserted-by":"crossref","unstructured":"B. Plateau, J. M. Fourneau, and K. H. Lee. PEPS: a package for solving complex Markov models of parallel systems. In R. Puigjaner and D. Potier, editors, Modelling techniques and tools for computer performance evaluation, 1988. 397","DOI":"10.1007\/978-1-4613-0533-0_19"},{"key":"27_CR28","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/BF01843570","volume":"1","author":"A. Pnueli","year":"1986","unstructured":"A. Pnueli and L. Zuck. Verification of multiprocess probabilistic protocols. Distributed Computing, 1:53\u201372, 1986. 396, 406","journal-title":"Distributed Computing"},{"key":"27_CR29","unstructured":"R. Segala. Modelling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, MIT, 1995. 398"},{"key":"27_CR30","unstructured":"M. Siegle. Compact representation of large performability models based on extended BDDs. In Fourth International Workshop on Performability Modeling of Computer and Communication Systems (PMCCS4), pages 77\u201380, 1998. 405"},{"key":"27_CR31","volume-title":"CUDD: CU decision diagram package","author":"F. Somenzi","year":"1997","unstructured":"F. Somenzi. CUDD: CU decision diagram package. Public software, Colorado University, Boulder, 1997. 396, 397, 405"},{"key":"27_CR32","doi-asserted-by":"crossref","unstructured":"M. Vardi. Automatic verification of probabilistic concurrent finite-state programs. In Proceedings, FOCS\u201985, pages 327\u2013338. IEEE Press, 1987. 396, 398","DOI":"10.1109\/SFCS.1985.12"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46419-0_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T06:00:47Z","timestamp":1737352847000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46419-0_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540672821","9783540464198"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/3-540-46419-0_27","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}