{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T12:40:01Z","timestamp":1746362401469,"version":"3.40.4"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319108841"},{"type":"electronic","value":"9783319108858"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-10885-8_17","type":"book-chapter","created":{"date-parts":[[2014,9,1]],"date-time":"2014-09-01T11:55:41Z","timestamp":1409572541000},"page":"240-254","source":"Crossref","is-referenced-by-count":0,"title":["Explicit State Space and Markov Chain Generation Using Decision Diagrams"],"prefix":"10.1007","author":[{"given":"Junaid","family":"Babar","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew S.","family":"Miner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"17_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/978-3-642-13675-7_19","volume-title":"Applications and Theory of Petri Nets","author":"J. Babar","year":"2010","unstructured":"Babar, J., Beccuti, M., Donatelli, S., Miner, A.: GreatSPN enhanced with decision diagram data structures. In: Lilius, J., Penczek, W. (eds.) PETRI NETS 2010. LNCS, vol.\u00a06128, pp. 308\u2013317. Springer, Heidelberg (2010)"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"Babar, J., Miner, A.: Meddly: Multi\u2013terminal and Edge\u2013valued Decision Diagram LibrarY. In: 7th Int. Conf. on Quantitative Evaluation of Systems (QEST 2010), pp. 195\u2013196 (September 2010)","DOI":"10.1109\/QEST.2010.34"},{"issue":"6","key":"17_CR3","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1109\/TSE.2003.1205180","volume":"29","author":"C. Baier","year":"2003","unstructured":"Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P.: Model checking algorithms for continuous-time Markov chains. IEEE Trans. Softw. Eng.\u00a029(6), 524\u2013541 (2003)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Bryant, R.E.: Graph\u2013based algorithms for boolean function manipulation. IEEE Trans. Comp. C-35(8), 677\u2013691 (1986)","DOI":"10.1109\/TC.1986.1676819"},{"issue":"2","key":"17_CR5","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. 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. Information and Computation\u00a098(2), 142\u2013170 (1992)","journal-title":"Information and Computation"},{"issue":"1-2","key":"17_CR6","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/0166-5316(95)00008-L","volume":"24","author":"G. Chiola","year":"1995","unstructured":"Chiola, G., Franceschinis, G., Gaeta, R., Ribaudo, M.: GreatSPN 1.7: Graphical Editor and Analyzer for Timed and Stochastic Petri Nets. Perf. Eval.\u00a024(1-2), 47\u201368 (1995)","journal-title":"Perf. Eval."},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"Chiola, G.: Compiling techniques for the analysis of stochastic Petri nets. In: Proc. 4th Int. Conf. on Modelling Techniques and Tools for Performance Evaluation, pp. 13\u201327 (1989)","DOI":"10.1007\/978-1-4613-0533-0_2"},{"issue":"11","key":"17_CR8","doi-asserted-by":"publisher","first-page":"1343","DOI":"10.1109\/12.247838","volume":"42","author":"G. Chiola","year":"1993","unstructured":"Chiola, G., Dutheillet, C., Franceschinis, G., Haddad, S.: Stochastic well-formed colored nets and symmetric modeling applications. IEEE Trans. Comp.\u00a042(11), 1343\u20131360 (1993)","journal-title":"IEEE Trans. Comp."},{"issue":"1","key":"17_CR9","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/s10703-006-0033-y","volume":"31","author":"G. Ciardo","year":"2007","unstructured":"Ciardo, G., L\u00fcttgen, G., Miner, A.S.: Exploiting interleaving semantics in symbolic state\u2013space generation. Formal Methods in System Design\u00a031(1), 63\u2013100 (2007)","journal-title":"Formal Methods in System Design"},{"issue":"4","key":"17_CR10","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1145\/1530873.1530885","volume":"36","author":"G. PCiardo","year":"2009","unstructured":"PCiardo, G., Miner, A.S., Wan, M.: Advanced features in SMART: the Stochastic Model checking Analyzer for Reliability and Timing. SIGMETRICS Perform. Eval. Rev.\u00a036(4), 58\u201363 (2009)","journal-title":"SIGMETRICS Perform. Eval. Rev."},{"issue":"1","key":"17_CR11","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/0166-5316(93)90026-Q","volume":"18","author":"G. Ciardo","year":"1993","unstructured":"Ciardo, G., Trivedi, K.S.: A decomposition approach for stochastic reward net models. Perf. Eval.\u00a018(1), 37\u201359 (1993)","journal-title":"Perf. Eval."},{"key":"17_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/11562436_32","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2005","author":"J.-M. Couvreur","year":"2005","unstructured":"Couvreur, J.-M., Thierry-Mieg, Y.: Hierarchical decision diagrams to exploit model structure. In: Wang, F. (ed.) FORTE 2005. LNCS, vol.\u00a03731, pp. 443\u2013457. Springer, Heidelberg (2005)"},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"Delamare, C., Gardan, Y., Moreaux, P.: Performance evaluation with asynchronously decomposable SWN: Implementation and case study. In: 10th Int. Workshop on Petri Nets and Performance Models (PNPM 2003), pp. 20\u201329. IEEE Comp. Soc. Press (September 2003)","DOI":"10.1109\/PNPM.2003.1231539"},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/978-3-540-71209-1_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Derisavi","year":"2007","unstructured":"Derisavi, S.: A symbolic algorithm for optimal Markov chain lumping. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 139\u2013154. Springer, Heidelberg (2007)"},{"issue":"1-2","key":"17_CR15","doi-asserted-by":"publisher","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"},{"issue":"1-2","key":"17_CR16","first-page":"9","volume":"4","author":"T. Kam","year":"1998","unstructured":"Kam, T., Villa, T., Brayton, R., Sangiovanni-Vincentelli, A.: Multi\u2013valued decision diagrams: theory and applications. Multiple-Valued Logic\u00a04(1-2), 9\u201362 (1998)","journal-title":"Multiple-Valued Logic"},{"key":"17_CR17","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1109\/12.506433","volume":"45","author":"Y.T. Lai","year":"1996","unstructured":"Lai, Y.T., Pedram, M., Vrudhula, S.B.K.: Formal verification using edge\u2013valued binary decision diagrams. IEEE Trans. Comp.\u00a045, 247\u2013255 (1996)","journal-title":"IEEE Trans. Comp."},{"key":"17_CR18","unstructured":"Miner, A., Parker, D.: Symbolic representations and analysis of large state spaces. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) AUTONOMY 2003. LNCS (LNAI), vol.\u00a02925, pp. 296\u2013338. Springer, Heidelberg (2004)"},{"key":"17_CR19","doi-asserted-by":"crossref","unstructured":"Miner, A.S.: Efficient solution of GSPNs using Canonical Matrix Diagrams. In: 9th Int. Workshop on Petri Nets and Performance Models (PNPM 2001), pp. 101\u2013110. IEEE Comp. Soc. Press (September 2001)","DOI":"10.1109\/PNPM.2001.953360"},{"issue":"1-4","key":"17_CR20","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1016\/j.peva.2003.07.005","volume":"56","author":"A.S. Miner","year":"2004","unstructured":"Miner, A.S.: Implicit GSPN reachability set generation using decision diagrams. Perf. Eval.\u00a056(1-4), 145\u2013165 (2004)","journal-title":"Perf. Eval."},{"key":"17_CR21","unstructured":"Model Checking Contest at Petri Nets (2014), http:\/\/mcc.lip6.fr\/models.php"},{"issue":"9","key":"17_CR22","doi-asserted-by":"publisher","first-page":"913","DOI":"10.1109\/TC.1982.1676110","volume":"31","author":"M.K. Molloy","year":"1982","unstructured":"Molloy, M.K.: Performance analysis using stochastic Petri nets. IEEE Trans. Comp.\u00a031(9), 913\u2013917 (1982)","journal-title":"IEEE Trans. Comp."},{"key":"17_CR23","first-page":"367","volume-title":"Proc. 1st Int. Workshop on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS 1993)","author":"J.K. Muppala","year":"1993","unstructured":"Muppala, J.K., Ciardo, G., Trivedi, K.S.: Modeling using Stochastic Reward Nets. In: Proc. 1st Int. Workshop on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS 1993), pp. 367\u2013372. IEEE Comp. Soc. Press, San Diego (1993)"},{"key":"17_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1007\/3-540-58152-9_23","volume-title":"Application and Theory of Petri Nets 1994","author":"E. Pastor","year":"1994","unstructured":"Pastor, E., Roig, O., Cortadella, J., Badia, R.M.: Petri net analysis using boolean manipulation. In: Valette, R. (ed.) ICATPN 1994. LNCS, vol.\u00a0815, pp. 416\u2013435. Springer, Heidelberg (1994)"},{"key":"17_CR25","unstructured":"Tilgner, M., Takahashi, Y., Ciardo, G.: SNS 1.0: Synchronized Network Solver. In: 1st International Workshop on Manufacturing and Petri Nets, Osaka, Japan, pp. 215\u2013234 (June 1996)"},{"issue":"5","key":"17_CR26","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1016\/j.peva.2011.02.005","volume":"68","author":"M. Wan","year":"2011","unstructured":"Wan, M., Ciardo, G., Miner, A.S.: Approximate steady\u2013state analysis of large Markov models based on the structure of their decision diagram encoding. Perf. Eval.\u00a068(5), 463\u2013486 (2011)","journal-title":"Perf. Eval."},{"key":"17_CR27","doi-asserted-by":"crossref","unstructured":"Wimmer, R., Braitling, B., Becker, B., Hahn, E.M., Crouzen, P., Hermanns, H., Dhama, A., Theel, O.: Symblicit calculation of long\u2013run averages for concurrent probabilistic systems. In: 7th Int. Conf. on Quantitative Evaluation of Systems (QEST 2010), pp. 27\u201336 (2010)","DOI":"10.1109\/QEST.2010.12"},{"key":"17_CR28","doi-asserted-by":"crossref","unstructured":"Woodside, C.M., Li, Y.: Performance Petri net analysis of communications protocol software by delay-equivalent aggregation. In: 4th Int. Workshop on Petri Nets and Performance Models (PNPM 1991), pp. 64\u201373. IEEE Comp. Soc. Press, Melbourne (1991)","DOI":"10.1109\/PNPM.1991.238781"},{"issue":"12","key":"17_CR29","doi-asserted-by":"publisher","first-page":"1334","DOI":"10.1109\/43.736573","volume":"17","author":"A. Xie","year":"1998","unstructured":"Xie, A., Beerel, P.A.: Efficient state classification of finite state Markov chains. IEEE Trans. Computer-Aided Design\u00a017(12), 1334\u20131339 (1998)","journal-title":"IEEE Trans. Computer-Aided Design"},{"key":"17_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1007\/BFb0031826","volume-title":"Formal Methods in Computer-Aided Design","author":"T. Yoneda","year":"1996","unstructured":"Yoneda, T., Hatori, H., Takahara, A., Minato, S.: BDDs vs. zero\u2013suppressed BDDs: for CTL symbolic model checking of Petri nets. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 435\u2013449. Springer, Heidelberg (1996)"}],"container-title":["Lecture Notes in Computer Science","Computer Performance Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10885-8_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T12:21:45Z","timestamp":1746361305000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10885-8_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319108841","9783319108858"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10885-8_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}