{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:09:30Z","timestamp":1725548970784},"publisher-location":"Berlin, Heidelberg","reference-count":73,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540222651"},{"type":"electronic","value":"9783540246114"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24611-4_9","type":"book-chapter","created":{"date-parts":[[2010,2,25]],"date-time":"2010-02-25T19:01:10Z","timestamp":1267124470000},"page":"296-338","source":"Crossref","is-referenced-by-count":32,"title":["Symbolic Representations and Analysis of Large Probabilistic Systems"],"prefix":"10.1007","author":[{"given":"Andrew","family":"Miner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Parker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"unstructured":"PRISM web site, www.cs.bham.ac.uk\/~dxp\/prism","key":"9_CR1"},{"unstructured":"SMART web site, http:\/\/www.cs.wm.edu\/~ciardo\/SMART\/","key":"9_CR2"},{"issue":"6","key":"9_CR3","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1109\/TC.1978.1675141","volume":"C-27","author":"S. Akers","year":"1978","unstructured":"Akers, S.: Binary decision diagrams. IEEE Transactions on Computers\u00a0C-27(6), 509\u2013516 (1978)","journal-title":"IEEE Transactions on Computers"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/3-540-61474-5_75","volume-title":"Computer Aided Verification","author":"A. Aziz","year":"1996","unstructured":"Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Verifying continuous time Markov chains. In: Alur, R., Henzinger, T. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 269\u2013276. Springer, Heidelberg (1996)"},{"doi-asserted-by":"crossref","unstructured":"Bahar, I., Frohm, E., Gaona, C., Hachtel, G., Macii, E., Pardo, A., Somenzi, F.: Algebraic decision diagrams and their applications. In Proc. International Conference on Computer-Aided Design (ICCAD 1993), pp. 188\u2013191 (1993);","key":"#cr-split#-9_CR5.1","DOI":"10.1109\/ICCAD.1993.580054"},{"doi-asserted-by":"crossref","unstructured":"Also available in Formal Methods in System Design 10(2\/3), 171\u2013206 (1997)","key":"#cr-split#-9_CR5.2","DOI":"10.1023\/A:1008699807402"},{"key":"9_CR6","volume-title":"Habilitation thesis","author":"C. Baier","year":"1998","unstructured":"Baier, C.: On algorithmic verification methods for probabilistic systems. In: Habilitation thesis, Fakult\u00e4t f\u00fcr Mathematik & Informatik, Universit\u00e4t Mannheim (1998)"},{"unstructured":"Baier, C., Clarke, E.: The algebraic mu-calculus and MTBDDs. In: Proc. 5th Workshop on Logic, Language, Information and Computation (WOLLIC 1998), pp. 27\u201338 (1998)","key":"9_CR7"},{"key":"9_CR8","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., 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.\u00a01256, pp. 430\u2013440. Springer, Heidelberg (1997)"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/3-540-48320-9_12","volume-title":"CONCUR 1999. Concurrency Theory","author":"C. Baier","year":"1999","unstructured":"Baier, C., Katoen, J.-P., Hermanns, H.: Approximate symbolic model checking of continuous-time markov chains (Extended abstract). In: Baeten, J., Mauw, S. (eds.) CONCUR 1999. LNCS, vol.\u00a01664, pp. 146\u2013161. Springer, Heidelberg (1999)"},{"issue":"9","key":"9_CR10","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1109\/12.537122","volume":"45","author":"B. Bollig","year":"1996","unstructured":"Bollig, B., Wegner, I.: Improving the variable ordering of OBDDs is NPcomplete. IEEE Transactions on Computers\u00a045(9), 993\u20131006 (1996)","journal-title":"IEEE Transactions on Computers"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/3-540-48683-6_24","volume-title":"Computer Aided Verification","author":"M. Bozga","year":"1999","unstructured":"Bozga, M., Maler, O.: On the representation of probabilities over structured domains. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 261\u2013273. Springer, Heidelberg (1999)"},{"key":"9_CR12","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1145\/123186.123222","volume-title":"Proc. 27th Design Automation Conference (DAC 1990)","author":"K. Brace","year":"1990","unstructured":"Brace, K., Rudell, R., Bryant, R.: Efficient implementation of a BDD package. In: Proc. 27th Design Automation Conference (DAC 1990), pp. 40\u201345. IEEE Computer Society Press, Los Alamitos (1990)"},{"issue":"8","key":"9_CR13","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R. Bryant","year":"1986","unstructured":"Bryant, R.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C\u00a035(8), 677\u2013691 (1986)","journal-title":"IEEE Transactions on Computers, C"},{"issue":"3","key":"9_CR14","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R. Bryant","year":"1992","unstructured":"Bryant, R.: Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys\u00a024(3), 293\u2013318 (1992)","journal-title":"ACM Computing Surveys"},{"issue":"3","key":"9_CR15","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1287\/ijoc.12.3.203.12634","volume":"12","author":"P. Buchholz","year":"2000","unstructured":"Buchholz, P., Ciardo, G., Donatelli, S., Kemper, P.: Complexity of memoryefficient Kronecker operations with applications to the solution of Markov models. INFORMS J. Comp.( SUMMER 2000)\u00a012(3), 203\u2013222 (2000)","journal-title":"INFORMS J. Comp.,( SUMMER 2000)"},{"key":"9_CR16","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1109\/PNPM.1995.524313","volume-title":"6th Int. Workshop on Petri Nets and Performance Models (PNPM 1995)","author":"P. Buchholz","year":"1995","unstructured":"Buchholz, P., Kemper, P.: Numerical analysis of stochastic marked graphs. In: 6th Int. Workshop on Petri Nets and Performance Models (PNPM 1995), Durham, NC, October 1995, pp. 32\u201341. IEEE Comp. Soc. Press, Los Alamitos (1995)"},{"key":"9_CR17","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1109\/PNPM.2001.953358","volume-title":"Proc. 9th International Workshop on Petri Nets and Performance Models (PNPM 2001)","author":"P. Buchholz","year":"2001","unstructured":"Buchholz, P., Kemper, P.: Compact representations of probability distributions in the analysis of superposed GSPNs. In: German, R., Haverkort, B. (eds.) Proc. 9th International Workshop on Petri Nets and Performance Models (PNPM 2001), pp. 81\u201390. IEEE Computer Society Press, Los Alamitos (2001)"},{"doi-asserted-by":"crossref","unstructured":"Buchholz, P., Kemper, P.: Kronecker based matrix representations for large Markov models. In: This proceedings (2003)","key":"9_CR18","DOI":"10.1007\/978-3-540-24611-4_8"},{"key":"9_CR19","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1109\/LICS.1990.113767","volume-title":"Proc. 5th Annual IEEE Symposium on Logic in Computer Science (LICS 1990)","author":"J.R. Burch","year":"1990","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, J.: Symbolic model checking: 1020 states and beyond. In: Proc. 5th Annual IEEE Symposium on Logic in Computer Science (LICS 1990), pp. 428\u2013439. IEEE Computer Society Press, Los Alamitos (1990)"},{"key":"9_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/3-540-44988-4_8","volume-title":"Application and Theory of Petri Nets 2000","author":"G. Ciardo","year":"2000","unstructured":"Ciardo, G., Luettgen, G., Siminiceanu, R.: Efficient symbolic state-space construction for asynchronous systems. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol.\u00a01825, pp. 103\u2013122. Springer, Heidelberg (2000)"},{"key":"9_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/3-540-45319-9_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Ciardo","year":"2001","unstructured":"Ciardo, G., Luettgen, G., Siminiceanu, R.: Saturation: An efficient iteration strategy for symbolic state-space generation. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 328\u2013342. Springer, Heidelberg (2001)"},{"key":"9_CR22","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1109\/IPDS.1996.540204","volume-title":"Proc. 2nd International Computer Performance and Dependability Symposium (IPDS1996)","author":"G. Ciardo","year":"1996","unstructured":"Ciardo, G., Miner, A.: SMART: Simulation and Markovian analyser for reliability and timing. In: Proc. 2nd International Computer Performance and Dependability Symposium (IPDS1996), p. 60. IEEE Computer Society Press, Los Alamitos (1996)"},{"key":"9_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/BFb0022196","volume-title":"Computer Performance Evaluation Modelling Techniques and Tools","author":"G. Ciardo","year":"1997","unstructured":"Ciardo, G., Miner, A.: Storage alternatives for large structured state spaces. In: Marie, R., Plateau, B., Calzarossa, M., Rubino, G. (eds.) TOOLS 1997. LNCS, vol.\u00a01245, pp. 44\u201357. Springer, Heidelberg (1997)"},{"key":"9_CR24","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1109\/PNPM.1999.796529","volume-title":"Proc. 8th International Workshop on Petri Nets and Performance Models (PNPM 1999)","author":"G. Ciardo","year":"1999","unstructured":"Ciardo, G., Miner, A.: A data structure for the efficient Kronecker solution of GSPNs. In: Buchholz, P., Silva, M. (eds.) Proc. 8th International Workshop on Petri Nets and Performance Models (PNPM 1999), pp. 22\u201331. IEEE Computer Society Press, Los Alamitos (1999)"},{"key":"9_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/3-540-36126-X_16","volume-title":"Formal Methods in Computer-Aided Design","author":"G. Ciardo","year":"2002","unstructured":"Ciardo, G., Siminiceanu, R.: Using edge-valued decision diagrams for symbolic generation of shortest paths. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517, pp. 256\u2013273. Springer, Heidelberg (2002)"},{"doi-asserted-by":"crossref","unstructured":"Ciesinski, F., Gr\u00f6ssner, F.: On probabilistic computation tree logic. This proceedings (2003)","key":"9_CR26","DOI":"10.1007\/978-3-540-24611-4_5"},{"unstructured":"Clarke, E., Fujita, M., McGeer, P., McMillan, K., Yang, J., Zhao, X.: Multi-terminal binary decision diagrams: An efficient data structure for matrix representation. In: Proc. International Workshop on Logic Synthesis (IWLS 1993), pp. 1\u201315 (1993);","key":"#cr-split#-9_CR27.1"},{"doi-asserted-by":"crossref","unstructured":"Also available in Formal Methods in System Design 10(2\/3), 149\u2013169 (1997)","key":"#cr-split#-9_CR27.2","DOI":"10.1023\/A:1008647823331"},{"key":"9_CR28","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1145\/157485.164569","volume-title":"Proc. 30th Design Automation Conference (DAC 1993)","author":"E. Clarke","year":"1993","unstructured":"Clarke, E., McMillan, K., Zhao, X., Fujita, M., Yang, J.: Spectral transforms for large Boolean functions with applications to technology mapping. In: Proc. 30th Design Automation Conference (DAC 1993), pp. 54\u201360. ACM Press, New York (1993); Also available in Formal Methods in System Design 10(2\/3), 137\u2013148 (1997)"},{"unstructured":"Cloth, L.: Specification and verification of Markov reward models. In: This proceedings (2003)","key":"9_CR29"},{"key":"9_CR30","series-title":"Lecture Notes in Computer Science","first-page":"365","volume-title":"Automatic Verification Methods for Finite State Systems","author":"O. Coudert","year":"1989","unstructured":"Coudert, O., Berthet, C., Madre, J.C.: Verification of synchronous sequential machines based on symbolic execution. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol.\u00a0407, pp. 365\u2013373. Springer, Heidelberg (1989)"},{"key":"9_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/3-540-44804-7_3","volume-title":"Process Algebra and Probabilistic Methods. Performance Modelling and Verification","author":"P. D\u2019Argenio","year":"2001","unstructured":"D\u2019Argenio, P., Jeannet, B., Jensen, H., Larsen, K.: Reachability analysis of probabilistic systems by successive refinements. In: de Alfaro, L., Gilmore, S. (eds.) PROBMIV 2001, PAPM-PROBMIV 2001, and PAPM 2001. LNCS, vol.\u00a02165, pp. 39\u201356. Springer, Heidelberg (2001)"},{"key":"9_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"188","DOI":"10.1007\/3-540-46029-2_12","volume-title":"Computer Performance Evaluation","author":"I. Davies","year":"2002","unstructured":"Davies, I., Knottenbelt, W., Kritzinger, P.: Symbolic methods for the state space exploration of GSPN models. In: Field, T., Harrison, P., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol.\u00a02324, pp. 188\u2013199. Springer, Heidelberg (2002)"},{"issue":"2","key":"9_CR33","doi-asserted-by":"crossref","first-page":"116","DOI":"10.1109\/TC.1981.6312174","volume":"30","author":"M. Davio","year":"1981","unstructured":"Davio, M.: Kronecker products and shuffle algebra. IEEE Transactions on Computers, C\u00a030(2), 116\u2013125 (1981)","journal-title":"IEEE Transactions on Computers, C"},{"key":"9_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/3-540-46419-0_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Alfaro de","year":"2000","unstructured":"de Alfaro, L., Kwiatkowska, M., Norman, G., Parker, D., Segala, R.: Symbolic model checking of probabilistic processes using mTBDDs and the kronecker representation. In: Graf, S., Schwartzbach, M. (eds.) TACAS 2000. LNCS, vol.\u00a01785, pp. 395\u2013410. Springer, Heidelberg (2000)"},{"key":"9_CR35","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/0166-5316(93)90025-P","volume":"18","author":"S. Donatelli","year":"1993","unstructured":"Donatelli, S.: Superposed stochastic automata: A class of stochastic Petri nets amenable to parallel solution. Performance Evaluation\u00a018, 21\u201336 (1993)","journal-title":"Performance Evaluation"},{"key":"9_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1007\/3-540-55179-4_20","volume-title":"Computer Aided Verification","author":"R. Enders","year":"1992","unstructured":"Enders, R., Filkorn, T., Taubner, D.: Generating BDDs for symbolic model checking in CCS. In: Larsen, K., Skou, A. (eds.) CAV 1991. LNCS, vol.\u00a0575, pp. 203\u2013213. Springer, Heidelberg (1992)"},{"issue":"3","key":"9_CR37","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1145\/278298.278303","volume":"45","author":"P. Fernandes","year":"1998","unstructured":"Fernandes, P., Plateau, B., Stewart, W.: Efficient descriptor-vector multiplication in stochastic automata networks. Journal of the ACM\u00a045(3), 381\u2013414 (1998)","journal-title":"Journal of the ACM"},{"doi-asserted-by":"crossref","unstructured":"Fujita, M., Matsunaga, Y., Kakuda, T.: On the variable ordering of binary decision diagrams for the application of multi-level synthesis. In: European conference on Design automation, pp. 50\u201354 (1991)","key":"9_CR38","DOI":"10.1109\/EDAC.1991.206358"},{"key":"9_CR39","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1145\/196244.196374","volume-title":"Proc. 31st Design Automation Conference (DAC 1994)","author":"G. Hachtel","year":"1994","unstructured":"Hachtel, G., Macii, E., Pardo, A., Somenzi, F.: Probabilistic analysis of large finite state machines. In: Proc. 31st Design Automation Conference (DAC 1994), pp. 270\u2013275. ACM Press, New York (1994)"},{"issue":"12","key":"9_CR40","doi-asserted-by":"crossref","first-page":"1479","DOI":"10.1109\/43.552081","volume":"15","author":"G. Hachtel","year":"1996","unstructured":"Hachtel, G., Macii, E., Pardo, A., Somenzi, F.: Markovian analysis of large finite state machines. IEEE Trans. on CAD\u00a015(12), 1479\u20131493 (1996)","journal-title":"IEEE Trans. on CAD"},{"issue":"5","key":"9_CR41","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H. Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and probability. Formal Aspects of Computing\u00a06(5), 512\u2013535 (1994)","journal-title":"Formal Aspects of Computing"},{"unstructured":"Hartonas-Garmhausen, V.: Probabilistic Symbolic Model Checking with Engineering Models and Applications. PhD thesis, Carnegie Mellon University (1998)","key":"9_CR42"},{"issue":"1-2","key":"9_CR43","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1016\/S1567-8326(02)00066-8","volume":"56","author":"H. Hermanns","year":"2003","unstructured":"Hermanns, H., Kwiatkowska, M., Norman, G., Parker, D., Siegle, M.: On the use of MTBDDs for performability analysis and verification of stochastic systems. Journal of Logic and Algebraic Programming: Special Issue on Probabilistic Techniques for the Design and Analysis of Systems\u00a056(1-2), 23\u201367 (2003)","journal-title":"Journal of Logic and Algebraic Programming: Special Issue on Probabilistic Techniques for the Design and Analysis of Systems"},{"unstructured":"Hermanns, H., Meyer-Kayser, J., Siegle, M.: Multi terminal binary decision diagrams to represent and analyse continuous time Markov chains. In: Plateau, B., Stewart, W., Silva, M. (eds.) 3rd International Workshop on Numerical Solution of Markov Chains (NSMC 1999), pp. 188\u2013207. Prensas Universitarias de Zaragoza (1999)","key":"9_CR44"},{"key":"9_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/3-540-48778-6_15","volume-title":"Formal Methods for Real-Time and Probabilistic Systems","author":"H. Hermanns","year":"1999","unstructured":"Hermanns, H., Siegle, M.: Bisimulation algorithms for stochastic process algebras and their BDD-based implementation. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol.\u00a01601, pp. 244\u2013264. Springer, Heidelberg (1999)"},{"key":"9_CR46","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/3-540-44804-7_8","volume-title":"Proc. Joint International Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification (PAPM\/PROBMIV 2001)","author":"J. Hillston","year":"2001","unstructured":"Hillston, J., Kloul, L.: An efficient Kronecker representation for PEPA models. In: Proc. Joint International Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification (PAPM\/PROBMIV 2001), pp. 120\u2013135. Springer, Heidelberg (2001)"},{"issue":"1\u20132","key":"9_CR47","first-page":"9","volume":"4","author":"T. Kam","year":"1998","unstructured":"Kam, T., Villa, T., Brayton, R.K., Sangiovanni-Vincentelli, A.: Multi-valued decision diagrams: theory and applications. Multiple-Valued Logic\u00a04(1\u20132), 9\u201362 (1998)","journal-title":"Multiple-Valued Logic"},{"key":"9_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/3-540-44804-7_2","volume-title":"Process Algebra and Probabilistic Methods. Performance Modelling and Verification","author":"J.-P. Katoen","year":"2001","unstructured":"Katoen, J.-P., Kwiatkowska, M., Norman, G., Parker, D.: Faster and symbolic CTMC model checking. In: de Alfaro, L., Gilmore, S. (eds.) PROBMIV 2001, PAPM-PROBMIV 2001, and PAPM 2001. LNCS, vol.\u00a02165, pp. 23\u201338. Springer, Heidelberg (2001)"},{"key":"9_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/3-540-45605-8_12","volume-title":"Process Algebra and Probabilistic Methods. Performance Modeling and Verification","author":"M. Kuntz","year":"2002","unstructured":"Kuntz, M., Siegle, M.: Deriving symbolic representations from stochastic process algebras. In: Hermanns, H., Segala, R. (eds.) PROBMIV 2002, PAPM-PROBMIV 2002, and PAPM 2002. LNCS, vol.\u00a02399, pp. 188\u2013206. Springer, Heidelberg (2002)"},{"key":"9_CR50","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"Proc. Workshop on Parallel and Distributed Model Checking (PDMC 2002)","author":"M. Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Mehmood, R., Norman, G., Parker, D.: A symbolic out-of-core solution method for Markov models. In: Proc. Workshop on Parallel and Distributed Model Checking (PDMC 2002). Electronic Notes in Theoretical Computer Science, vol.\u00a068.4. Elsevier, Amsterdam (2002)"},{"key":"9_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/3-540-46029-2_13","volume-title":"Computer Performance Evaluation","author":"M. Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM: Probabilistic symbolic model checker. In: Field, T., Harrison, P., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol.\u00a02324, pp. 200\u2013204. Springer, Heidelberg (2002)"},{"key":"9_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/3-540-46002-0_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic symbolic model checking with PRISM: A hybrid approach. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 52\u201366. Springer, Heidelberg (2002)"},{"unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Segala, R.: Symbolic model checking of concurrent probabilistic systems using MTBDDs and Simplex. Technical Report CSR-99-1, School of Computer Science, University of Birmingham (1999)","key":"9_CR53"},{"key":"9_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/3-540-44585-4_17","volume-title":"Computer Aided Verification","author":"M. Kwiatkowska","year":"2001","unstructured":"Kwiatkowska, M., Norman, G., Segala, R.: Automated verification of a randomized distributed consensus protocol using cadence SMV and PRISM. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 194\u2013206. Springer, Heidelberg (2001)"},{"key":"9_CR55","doi-asserted-by":"crossref","first-page":"985","DOI":"10.1002\/j.1538-7305.1959.tb01585.x","volume":"38","author":"C. Lee","year":"1959","unstructured":"Lee, C.: Representation of switching circuits by binary-decision programs. Bell System Technical Journal\u00a038, 985\u2013999 (1959)","journal-title":"Bell System Technical Journal"},{"key":"9_CR56","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K. McMillan","year":"1993","unstructured":"McMillan, K.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)"},{"unstructured":"Miner, A.: Data Structures for the Analysis of Large Structured Markov Chains. PhD thesis, Department of Computer Science, College of William & Mary, Virginia (2000)","key":"9_CR57"},{"key":"9_CR58","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1109\/PNPM.2001.953360","volume-title":"Proc. 9th International Workshop on Petri Nets and Performance Models (PNPM 2001)","author":"A. Miner","year":"2001","unstructured":"Miner, A.: Efficient solution of GSPNs using canonical matrix diagrams. In: German, R., Haverkort, B. (eds.) Proc. 9th International Workshop on Petri Nets and Performance Models (PNPM 2001), pp. 101\u2013110. IEEE Computer Society Press, Los Alamitos (2001)"},{"doi-asserted-by":"crossref","unstructured":"Miner, A.: Efficient state space generation of GSPNs using decision diagrams. In: Proc. 2002 Int. Conf. on Dependable Systems and Networks (DSN 2002), Washington, DC, June 2002, pp. 637\u2013646 (2002)","key":"9_CR59","DOI":"10.1109\/DSN.2002.1029009"},{"key":"9_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1007\/3-540-48745-X_2","volume-title":"Application and Theory of Petri Nets 1999","author":"A. Miner","year":"1999","unstructured":"Miner, A., Ciardo, G.: Efficient reachability set generation and storage using decision diagrams. In: Donatelli, S., Kleijn, J. (eds.) ICATPN 1999. LNCS, vol.\u00a01639, pp. 6\u201325. Springer, Heidelberg (1999)"},{"doi-asserted-by":"crossref","unstructured":"Miner, A., Ciardo, G., Donatelli, S.: Using the exact state space of a Markov model to compute approximate stationary measures. In: Proc. 2000 ACM SIGMETRICS Conf. on Measurement and Modeling of Computer Systems, Santa Clara, CA, June 2000, pp. 207\u2013216 (2000)","key":"9_CR61","DOI":"10.1145\/339331.339417"},{"unstructured":"Parker, D.: Implementation of Symbolic Model Checking for Probabilistic Systems. PhD thesis, University of Birmingham (2002)","key":"9_CR62"},{"doi-asserted-by":"crossref","unstructured":"Pastor, E., Cortadella, J.: Efficient encoding schemes for symbolic analysis of Petri nets. In: Design Automation and Test in Europe (DATE 1998), Paris (February 1998)","key":"9_CR63","DOI":"10.1109\/DATE.1998.655948"},{"doi-asserted-by":"crossref","unstructured":"Pastor, E., Cortadella, J., Pe\u00f1a, M.: Structural methods to improve the symbolic analysis of Petri nets. In: 20th International Conference on Application and Theory of Petri Nets, Williamsburg (June 1999)","key":"9_CR64","DOI":"10.1007\/3-540-48745-X_3"},{"doi-asserted-by":"crossref","unstructured":"Plateau, B.: 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, Performance Evaluation Review, vol. 13(2), pp. 147\u2013153 (1985)","key":"9_CR65","DOI":"10.1145\/317786.317819"},{"doi-asserted-by":"crossref","unstructured":"Rudell, R.: Dynamic variable ordering for ordered binary decision diagrams. In: Proc. International Conference on Computer-Aided Design (ICCAD 1993), pp. 42\u201347 (1993)","key":"9_CR66","DOI":"10.1109\/ICCAD.1993.580029"},{"unstructured":"Siegle, M.: Compositional representation and reduction of stochastic labelled transition systems based on decision node BDDs. In: Baum, D., Mueller, N., Roedler, R. (eds.) Proc. Messung, Modellierung und Bewertung von Rechen- und Kommunikationssystemen (MMB 1999), pp. 173\u2013185. VDE Verlag (1999)","key":"9_CR67"},{"unstructured":"Siegle, M.: Behaviour analysis of communication systems: Compositional modelling, compact representation and analysis of performability properties. Habilitation thesis, Universit\u00e4t Erlangen-N\u00fcrnberg (2002)","key":"9_CR68"},{"doi-asserted-by":"crossref","unstructured":"Stewart, W.J.: Introduction to the Numerical Solution of Markov Chains, Princeton (1994)","key":"9_CR69","DOI":"10.1515\/9780691223384"},{"key":"9_CR70","first-page":"64","volume-title":"Proc. 3rd International Symposium on Advanced Research in Asynchronous Circuits and Systems (ASYNC 1997)","author":"A. Xie","year":"1997","unstructured":"Xie, A., Beerel, A.: Symbolic techniques for performance analysis of timed circuits based on average time separation of events. In: Proc. 3rd International Symposium on Advanced Research in Asynchronous Circuits and Systems (ASYNC 1997), pp. 64\u201375. IEEE Computer Society Press, Los Alamitos (1997)"},{"unstructured":"Zampuni\u00e8ris, D.: The Sharing Tree Data Structure, Theory and Applications in Formal Verification. PhD thesis, Department of Computer Science, University of Namur, Belgium (1997)","key":"9_CR71"}],"container-title":["Lecture Notes in Computer Science","Validation of Stochastic Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24611-4_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,30]],"date-time":"2023-05-30T16:51:55Z","timestamp":1685465515000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24611-4_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540222651","9783540246114"],"references-count":73,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24611-4_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}