{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:27:40Z","timestamp":1761611260992,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540008989"},{"type":"electronic","value":"9783540365778"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36577-x_27","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:12:04Z","timestamp":1269897124000},"page":"379-393","source":"Crossref","is-referenced-by-count":45,"title":["Saturation Unbound"],"prefix":"10.1007","author":[{"given":"Gianfranco","family":"Ciardo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert","family":"Marmorstein","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Radu","family":"Siminiceanu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,2,28]]},"reference":[{"key":"27_CR1","volume-title":"Modelling with Generalized Stochastic Petri Nets","author":"M. A. Marsan","year":"1995","unstructured":"M. Ajmone Marsan, G. Balbo, G. Conte, S. Donatelli, and G. Franceschinis. Modelling with Generalized Stochastic Petri Nets. John Wiley & Sons, New York, 1995."},{"key":"27_CR2","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1109\/TR.1981.5221004","volume":"30","author":"V. Amoia","year":"1981","unstructured":"V. Amoia, G. De Micheli, and M. Santomauro. Computer-oriented formulation of transition-rate matrices via Kronecker algebra. IEEE Trans. Rel., 30:123\u2013132, June 1981.","journal-title":"IEEE Trans. Rel."},{"key":"27_CR3","doi-asserted-by":"crossref","unstructured":"R. Bloem, K. Ravi, and F. Somenzi. Symbolic guided search for CTL model checking. In Proc. 37th Conf. on Design Automation, p. 29\u201334. ACM Press, 2000.","DOI":"10.1145\/337292.337306"},{"key":"27_CR4","doi-asserted-by":"crossref","unstructured":"A. Bouajjani, B. Jonsson, M. Nilsson, and T. Touili. Regular model checking. In Computer Aided Verification, pages 403\u2013418, 2000.","DOI":"10.1007\/10722167_31"},{"issue":"8","key":"27_CR5","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R. E. Bryant","year":"1986","unstructured":"R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. Comp., 35(8):677\u2013691, Aug. 1986.","journal-title":"IEEE Trans. Comp."},{"issue":"3","key":"27_CR6","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1145\/136035.136043","volume":"24","author":"R. E. Bryant","year":"1992","unstructured":"R. E. Bryant. Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comp. Surv., 24(3):393\u2013318, 1992.","journal-title":"ACM Comp. Surv."},{"issue":"3","key":"27_CR7","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1287\/ijoc.12.3.203.12634","volume":"12","author":"P. Buchholz","year":"2000","unstructured":"P. Buchholz, G. Ciardo, S. Donatelli, and P. Kemper. Complexity of memorye ficient Kronecker operations with applications to the solution of Markov models. INFORMS J. Comp., 12(3):203\u2013222, 2000.","journal-title":"INFORMS J. Comp."},{"key":"27_CR8","doi-asserted-by":"crossref","unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. In Proc. 5th Annual IEEE Symp. on Logic in Computer Science, pages 428\u2013439, Philadelphia, PA, 4\u20137 June 1990. IEEE Comp. Soc. Press.","DOI":"10.1109\/LICS.1990.113767"},{"key":"27_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1007\/3-540-58152-9_11","volume-title":"Petri nets with marking-dependent arc multiplicity: properties and analysis","author":"G. Ciardo","year":"1994","unstructured":"G. Ciardo. Petri nets with marking-dependent arc multiplicity: properties and analysis. In R. Valette, editor, Proc. 15th Int. Conf. on Applications and Theory of Petri Nets, LNCS 815, pages 179\u2013198, Zaragoza, Spain, June 1994. Springer-Verlag."},{"key":"27_CR10","unstructured":"G. Ciardo, R. L. Jones, A. S. Miner, and R. Siminiceanu. SMART: Stochastic Model Analyzer for Reliability and Timing. In P. Kemper, editor, Tools of Int. Multiconference on Measurement, Modelling and Evaluation of Computer-Communication Systems, pages 29\u201334, Aachen, Germany, Sept. 2001."},{"key":"27_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/3-540-44988-4_8","volume-title":"Efficient symbolic state-space construction for asynchronous systems","author":"G. Ciardo","year":"2000","unstructured":"G. Ciardo, G. Luettgen, and R. Siminiceanu. Efficient symbolic state-space construction for asynchronous systems. In M. Nielsen and D. Simpson, editors, Proc. 21th Int. Conf. on Applications and Theory of Petri Nets, LNCS 1825, pages 103\u2013122, Aarhus, Denmark, June 2000. Springer-Verlag."},{"key":"27_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1007\/3-540-45319-9_23","volume-title":"Saturation: An efficient iteration strategy for symbolic state space generation","author":"G. Ciardo","year":"2001","unstructured":"G. Ciardo, G. Luettgen, and R. Siminiceanu. Saturation: An efficient iteration strategy for symbolic state space generation. In T. Margaria and W. Yi, editors, Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS 2031, pages 328\u2013342, Genova, Italy, Apr. 2001. Springer-Verlag."},{"key":"27_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"256","DOI":"10.1007\/3-540-36126-X_16","volume-title":"Using edge-valued decision diagrams for symbolic generation of shortest paths","author":"G. Ciardo","year":"2002","unstructured":"G. Ciardo and R. Siminiceanu. Using edge-valued decision diagrams for symbolic generation of shortest paths. In M. D. Aagaard and J. W. O\u2019Leary, editors, Proc. Fourth International Conference on Formal Methods in Computer-Aided Design (FMCAD), LNCS 2517, pages 256\u2013273, Portland, OR, USA, Nov. 2002. Springer-Verlag."},{"key":"27_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"495","DOI":"10.1007\/3-540-48683-6_44","volume-title":"CAV\u2019 99","author":"A. Cimatti","year":"1999","unstructured":"A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri. NuSMV: A new symbolic model verifier. In CAV\u2019 99, LNCS 1633, pages 495\u2013499. Springer-Verlag, 1999."},{"key":"27_CR15","unstructured":"O. Coudert and J. C. Madre. Symbolic computation of the valid states of a sequential machine: algorithms and discussion. In 1991 Int. Workshop on Formal Methods in VLSI Design, pages 1\u201319, Miami, FL, USA, 1991."},{"issue":"1","key":"27_CR16","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1109\/43.184839","volume":"12","author":"M. Fujita","year":"1993","unstructured":"M. Fujita, H. Fujisawa, and Y. Matsunaga. Variable ordering algorithms for ordered binary decision diagrams and their evaluation. IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems, 12(1):6\u201312, 1993.","journal-title":"IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"27_CR17","unstructured":"A. Geser, J. Knoop, G. L\u00fcttgen, B. Steffen, and O. R\u00fcthing. Chaotic fixed point iterations. Technical Report MIP-9403, Univ. of Passau, 1994."},{"issue":"3","key":"27_CR18","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1023\/A:1008771008310","volume":"14","author":"P. Godefroid","year":"1999","unstructured":"P. Godefroid and D. E. Long. Symbolic protocol verification with queue BDDs. Formal Methods in System Design, 14(3):257\u2013271, May 1999.","journal-title":"Formal Methods in System Design"},{"key":"27_CR19","doi-asserted-by":"crossref","unstructured":"J. G. Henriksen, J. L. Jensen, M. E. J\u00f8rgensen, N. Klarlund, R. Paige, T. Rauhe, and A. Sandholm. Mona: Monadic second-order logic in practice. In E. Brinksma, R. Cleaveland, K. G. Larsen, T. Margaria, and B. Steffen, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 1019, pages 89\u2013110. Springer, 1995.","DOI":"10.1007\/3-540-60630-0_5"},{"key":"27_CR20","unstructured":"J.R. Burch, E.M. Clarke, and D.E. Long. Symbolic model checking with partitioned transition relations. In A. Halaas and P.B. Denyer, editors, Int. Conference on Very Large Scale Integration, pages 49\u201358, Edinburgh, Scotland, Aug. 1991. IFIP Transactions, North-Holland."},{"issue":"1","key":"27_CR21","first-page":"9","volume":"4","author":"T. Kam","year":"1998","unstructured":"T. Kam, T. Villa, R. Brayton, and A. Sangiovanni-Vincentelli. Multi-valued decision diagrams: theory and applications. Multiple-Valued Logic, 4(1\u20132):9\u201362, 1998.","journal-title":"Multiple-Valued Logic"},{"key":"27_CR22","unstructured":"J. Martinez and M. Silva. A simple and fast algorithm to obtain all invariants of a generalised Petri net. In Proc. 2nd European Workshop on Application and Theory of Petri Nets, pages 411\u2013422, Bad Honnef, Germany, 1981."},{"key":"27_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"6","DOI":"10.1007\/3-540-48745-X_2","volume-title":"Effcient reachability set generation and storage using decision diagrams","author":"A. S. Miner","year":"1999","unstructured":"A. S. Miner and G. Ciardo. Effcient reachability set generation and storage using decision diagrams. In H. Kleijn and S. Donatelli, editors, Proc. 20th Int. Conf. on Applications and Theory of Petri Nets, LNCS 1639, pages 6\u201325, Williamsburg, VA, USA, June 1999. Springer-Verlag."},{"key":"27_CR24","unstructured":"T. Murata and R. Church. Analysis of marked graphs and Petri nets by matrix equations. Research report MDC 1.1.8, Department of information engineering, Univeristy of Illinois, Chicago, IL, Nov. 1975."},{"key":"27_CR25","doi-asserted-by":"crossref","unstructured":"B. Plateau. On the stochastic structure of parallelism and synchronisation models for distributed algorithms. In Proc. ACM SIGMETRICS, pages 147\u2013153, Austin, TX, USA, May 1985.","DOI":"10.1145\/317786.317819"},{"key":"27_CR26","doi-asserted-by":"crossref","unstructured":"K. Ravi and F. Somenzi. Efficient fixpoint computation for invariant checking. In Proc. Int. Conference on Computer Design (ICCD), pages 467\u2013474, Austin, TX, Oct. 1999. IEEE Comp. Soc. Press.","DOI":"10.1109\/ICCD.1999.808582"},{"key":"27_CR27","unstructured":"F. Somenzi. CUDD: CU Decision Diagram Package, Release 2.3.1. http:\/\/vlsi.colorado.edu\/~fabio\/CUDD\/cuddIntro.html ."}],"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-36577-X_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T19:09:50Z","timestamp":1739992190000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36577-X_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540008989","9783540365778"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-36577-x_27","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}