{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T04:55:23Z","timestamp":1725512123077},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540724827"},{"type":"electronic","value":"9783540725220"}],"license":[{"start":{"date-parts":[[2007,1,1]],"date-time":"2007-01-01T00:00:00Z","timestamp":1167609600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-72522-0_9","type":"book-chapter","created":{"date-parts":[[2007,6,5]],"date-time":"2007-06-05T19:02:12Z","timestamp":1181070132000},"page":"371-394","source":"Crossref","is-referenced-by-count":5,"title":["Data Representation and Efficient Solution: A Decision Diagram Approach"],"prefix":"10.1007","author":[{"given":"Gianfranco","family":"Ciardo","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"2-3","key":"9_CR1","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1023\/A:1008699807402","volume":"10","author":"R.I. Bahar","year":"1997","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. Formal Methods in System Design\u00a010(2-3), 171\u2013206 (1997)","journal-title":"Formal Methods in System Design"},{"issue":"9","key":"9_CR2","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1109\/12.537122","volume":"45","author":"B. Bollig","year":"1996","unstructured":"Bollig, B., Wegener, I.: Improving the variable ordering of OBDDs is NP-complete. IEEE Trans. Comp.\u00a045(9), 993\u20131002 (1996)","journal-title":"IEEE Trans. Comp."},{"issue":"8","key":"9_CR3","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comp.\u00a035(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comp."},{"issue":"3","key":"9_CR4","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R.E. Bryant","year":"1992","unstructured":"Bryant, R.E.: Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comp. Surv.\u00a024(3), 293\u2013318 (1992)","journal-title":"ACM Comp. Surv."},{"issue":"4","key":"9_CR5","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1016\/S0168-9274(99)00005-7","volume":"31","author":"P. Buchholz","year":"1999","unstructured":"Buchholz, P.: Structured analysis approaches for large Markov chains. Applied Numerical Mathematics\u00a031(4), 375\u2013404 (1999)","journal-title":"Applied Numerical Mathematics"},{"issue":"3","key":"9_CR6","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 memory-efficient Kronecker operations with applications to the solution of Markov models. INFORMS J. Comp.\u00a012(3), 203\u2013222 (2000)","journal-title":"INFORMS J. Comp."},{"issue":"1-2","key":"9_CR7","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1016\/S1567-8326(02)00067-X","volume":"56","author":"P. Buchholz","year":"2003","unstructured":"Buchholz, P., Katoen, J.P., Kemper, P., Tepper, C.: Model-checking large structured Markov chains. J. Logic & Algebraic Progr.\u00a056(1-2), 69\u201397 (2003)","journal-title":"J. Logic & Algebraic Progr."},{"key":"9_CR8","series-title":"IFIP Transactions","first-page":"49","volume-title":"Int. Conference on Very Large Scale Integration","author":"J.R. Burch","year":"1991","unstructured":"Burch, J.R., Clarke, E.M., Long, D.E.: Symbolic model checking with partitioned transition relations. In: Halaas, A., Denyer, P.B. (eds.) Int. Conference on Very Large Scale Integration, Edinburgh, Scotland, Aug. 1991. IFIP Transactions, pp. 49\u201358. North-Holland, Amsterdam (1991)"},{"key":"9_CR9","doi-asserted-by":"publisher","first-page":"578","DOI":"10.1016\/j.peva.2005.06.001","volume":"63","author":"G. Ciardo","year":"2006","unstructured":"Ciardo, G., Jones, R.L., Miner, A.S., Siminiceanu, R.: Logical and stochastic modeling with SMART. Perf. Eval.\u00a063, 578\u2013608 (2006)","journal-title":"Perf. Eval."},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-540-73094-1_8","volume-title":"Petri Nets and Other Models of Concurrency \u2013 ICATPN 2007","author":"G. Ciardo","year":"2007","unstructured":"Ciardo, G., L\u00fcttgen, G., Yu, A.J.: Improving Static Variable Orders Via Invariants. In: Kleijn, J., Yakovlev, A. (eds.) ICATPN 2007. LNCS, vol.\u00a04546, pp. 83\u2013103. Springer, Heidelberg (2007)"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"379","DOI":"10.1007\/3-540-36577-X_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Ciardo","year":"2003","unstructured":"Ciardo, G., Marmorstein, R., Siminiceanu, R.I.: Saturation Unbound. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol.\u00a02619, pp. 379\u2013393. Springer, Heidelberg (2003)"},{"issue":"1","key":"9_CR12","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/s10009-005-0188-7","volume":"8","author":"G. Ciardo","year":"2006","unstructured":"Ciardo, G., Marmorstein, R., Siminiceanu, R.: The saturation algorithm for symbolic state space exploration. Software Tools for Technology Transfer\u00a08(1), 4\u201325 (2006)","journal-title":"Software Tools for Technology Transfer"},{"key":"9_CR13","first-page":"22","volume-title":"Proc. 8th Int. Workshop on Petri Nets and Performance Models (PNPM\u201999)","author":"G. Ciardo","year":"1999","unstructured":"Ciardo, G., Miner, A.S.: A data structure for the efficient Kronecker solution of GSPNs. In: Buchholz, P. (ed.) Proc. 8th Int. Workshop on Petri Nets and Performance Models (PNPM\u201999), Zaragoza, Spain, Sep. 1999, pp. 22\u201331. IEEE Computer Society Press, Los Alamitos (1999)"},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1007\/978-3-540-45069-6_4","volume-title":"Computer Aided Verification","author":"G. Ciardo","year":"2003","unstructured":"Ciardo, G., Siminiceanu, R.I.: Structural Symbolic CTL Model Checking of Asynchronous Systems. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 40\u201353. Springer, Heidelberg (2003)"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/11560548_13","volume-title":"Correct Hardware Design and Verification Methods","author":"G. Ciardo","year":"2005","unstructured":"Ciardo, G., Yu, A.J.: Saturation-based symbolic reachability analysis using conjunctive and disjunctive partitioning. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol.\u00a03725, pp. 146\u2013161. Springer, Heidelberg (2005)"},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1982)"},{"key":"9_CR18","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1109\/TC.1981.1675863","volume":"30","author":"M. Davio","year":"1981","unstructured":"Davio, M.: Kronecker products and shuffle algebra. IEEE Trans. Comp.\u00a030, 116\u2013125 (1981)","journal-title":"IEEE Trans. Comp."},{"key":"9_CR19","first-page":"132","volume-title":"Proc. 7th Int. Workshop on Petri Nets and Performance Models (PNPM\u201997)","author":"D.D. Deavours","year":"1997","unstructured":"Deavours, D.D., Sanders, W.H.: \u201cOn-the-fly\u201d solution techniques for stochastic Petri nets and extensions. In: Proc. 7th Int. Workshop on Petri Nets and Performance Models (PNPM\u201997), Saint-Malo, France, June 1997, pp. 132\u2013141. IEEE Computer Society Press, Los Alamitos (1997)"},{"issue":"3","key":"9_CR20","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.J.: Efficient descriptor-vector multiplication in stochastic automata networks. J. ACM\u00a045(3), 381\u2013414 (1998)","journal-title":"J. ACM"},{"key":"9_CR21","doi-asserted-by":"publisher","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 in System Design\u00a010, 149\u2013169 (1997)","journal-title":"Formal Methods in System Design"},{"key":"9_CR22","first-page":"83","volume":"18","author":"O. Grumberg","year":"2003","unstructured":"Grumberg, O., Livne, S., Markovitch, S.: Learning to order BDD variables in verification. J. Art. Int. Res.\u00a018, 83\u2013116 (2003)","journal-title":"J. Art. Int. Res."},{"key":"9_CR23","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)"},{"issue":"1\u20132","key":"9_CR24","first-page":"9","volume":"4","author":"T. Kam","year":"1998","unstructured":"Kam, T., Villa, T., Brayton, R., 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_CR25","volume-title":"Finite Markov Chains","author":"J.G. Kemeny","year":"1960","unstructured":"Kemeny, J.G., Snell, J.L.: Finite Markov Chains. D. Van Nostrand-Reinhold, New York (1960)"},{"key":"9_CR26","doi-asserted-by":"publisher","first-page":"608","DOI":"10.1109\/DAC.1992.227813","volume-title":"Proceedings of the 29th Conference on Design Automation","author":"Y.-T. Lai","year":"1992","unstructured":"Lai, Y.-T., Sastry, S.: Edge-valued binary decision diagrams for multi-level hierarchical verification. In: Proceedings of the 29th Conference on Design Automation, June 1992, pp. 608\u2013613. IEEE Computer Society Press, Los Alamitos (1992)"},{"key":"9_CR27","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1109\/PNPM.2001.953360","volume-title":"Proc. 9th Int. Workshop on Petri Nets and Performance Models (PNPM\u201901)","author":"A.S. Miner","year":"2001","unstructured":"Miner, A.S.: Efficient solution of GSPNs using canonical matrix diagrams. In: German, R., Haverkort, B. (eds.) Proc. 9th Int. Workshop on Petri Nets and Performance Models (PNPM\u201901), Aachen, Germany, Sep. 2001, pp. 101\u2013110. IEEE Computer Society Press, Los Alamitos (2001)"},{"key":"9_CR28","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1145\/339331.339417","volume-title":"Proc. ACM SIGMETRICS","author":"A.S. Miner","year":"2000","unstructured":"Miner, A.S., Ciardo, G., Donatelli, S.: Using the exact state space of a Markov model to compute approximate stationary measures. In: Kurose, J., Nain, P. (eds.) Proc. ACM SIGMETRICS, Santa Clara, CA, USA, June 2000, pp. 207\u2013216. ACM Press, New York (2000)"},{"key":"9_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"296","DOI":"10.1007\/978-3-540-24611-4_9","volume-title":"Validation of Stochastic Systems","author":"A.S. Miner","year":"2004","unstructured":"Miner, A.S., Parker, D.: Symbolic Representations and Analysis of Large Probabilistic Systems. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol.\u00a02925, pp. 296\u2013338. Springer, Heidelberg (2004)"},{"key":"9_CR30","doi-asserted-by":"crossref","unstructured":"Plateau, B.: On the stochastic structure of parallelism and synchronisation models for distributed algorithms. In: Proc. ACM SIGMETRICS, Austin, TX, USA, May 1985, pp. 147\u2013153 (1985)","DOI":"10.1145\/317795.317819"},{"key":"9_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"374","DOI":"10.1007\/3-540-60029-9_50","volume-title":"Application and Theory of Petri Nets 1995","author":"O. Roig","year":"1995","unstructured":"Roig, O., Cortadella, J., Pastor, E.: Verification of asynchronous circuits by BDD-based model checking of Petri nets. In: DeMichelis, G., D\u00edaz, M. (eds.) ICATPN 1995. LNCS, vol.\u00a0935, pp. 374\u2013391. Springer, Heidelberg (1995)"},{"key":"9_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/11691372_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R.I. Siminiceanu","year":"2006","unstructured":"Siminiceanu, R.I., Ciardo, G.: New Metrics for Static Variable Ordering in Decision Diagrams. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol.\u00a03920, pp. 90\u2013104. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Performance Evaluation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-72522-0_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T13:46:15Z","timestamp":1558273575000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-72522-0_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540724827","9783540725220"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-72522-0_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}