{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T15:26:52Z","timestamp":1759073212797},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2007,1,11]],"date-time":"2007-01-11T00:00:00Z","timestamp":1168473600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2007,6,14]]},"DOI":"10.1007\/s10703-006-0033-y","type":"journal-article","created":{"date-parts":[[2007,1,10]],"date-time":"2007-01-10T15:37:18Z","timestamp":1168443438000},"page":"63-100","source":"Crossref","is-referenced-by-count":21,"title":["Exploiting interleaving semantics in symbolic state-space generation"],"prefix":"10.1007","volume":"31","author":[{"given":"Gianfranco","family":"Ciardo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gerald","family":"L\u00fcttgen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew S.","family":"Miner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2007,1,11]]},"reference":[{"key":"33_CR1","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1023\/A:1008767206905","volume":"18","author":"R Alur","year":"2001","unstructured":"Alur R, Brayton R, Henzinger T, Qadeer S, Rajamani S (2001) Partial-order reduction in symbolic state-space exploration. Formal Methods Syst Design 18:97\u2013116","journal-title":"Formal Methods Syst Design"},{"key":"33_CR2","doi-asserted-by":"crossref","unstructured":"Barner S, Rabinovitz I (2003) Efficient symbolic model checking of software using partial disjunctive partitioning. In Correct Hardware Design and Verification Methods, LNCS 2860, Springer-Verlag, pp 35\u201350","DOI":"10.1007\/978-3-540-39724-3_6"},{"issue":"8","key":"33_CR3","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant RE (1986) Graph-based algorithms for boolean function manipulation. IEEE Trans Comp 35(8):677\u2013691","journal-title":"IEEE Trans Comp"},{"issue":"2","key":"33_CR4","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"JR Burch","year":"1992","unstructured":"Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang L (1992) Symbolic model checking: 1020 states and beyond. Inf Comput 98(2):142\u2013170","journal-title":"Inf Comput"},{"key":"33_CR5","unstructured":"Burch JR, Clarke EM, Long DE (1991) Symbolic model checking with partitioned transition relations. In Very Large Scale Integration. IFIP Transactions, North-Holland, pp 49\u201358"},{"issue":"4","key":"33_CR6","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1109\/43.275352","volume":"13","author":"JR Burch","year":"1994","unstructured":"Burch JR, Clarke EM, Long DE, McMillan KL, Dill DL (1994) Symbolic model checking for sequential circuit verification. IEEE Trans Comput-Aided Design Integrated Circuits Syst 13(4):401\u2013424","journal-title":"IEEE Trans Comput-Aided Design Integrated Circuits Syst"},{"key":"33_CR7","unstructured":"Cabodi G, Camurati P, Quer S (1999) Improving symbolic traversals by means of activity profiles. In Design Automation Conference. IEEE Comp Soc Press, pp 306\u2013311"},{"key":"33_CR8","doi-asserted-by":"crossref","unstructured":"Ciardo G, Jones RL, Miner AS, Siminiceanu R (2003) Logical and stochastic modeling with SMART. In Modeling Techniques and Tools for Computer Performance Evaluation, LNCS 2794. Springer-Verlag, pp 78\u201397","DOI":"10.1007\/978-3-540-45232-4_6"},{"key":"33_CR9","doi-asserted-by":"crossref","unstructured":"Ciardo G, L\u00fcttgen G, Siminiceanu R (2000) Efficient symbolic state-space construction for asynchronous systems. In Applications and Theory of Petri Nets, LNCS 1825. Springer-Verlag, pp 103\u2013122","DOI":"10.1007\/3-540-44988-4_8"},{"key":"33_CR10","doi-asserted-by":"crossref","unstructured":"Ciardo G, L\u00fcttgen G, Siminiceanu R (2001) Saturation: An efficient iteration strategy for symbolic state space generation. In Tools and Algorithms for the Construction and Analysis of Systems, LNCS 2031. Springer-Verlag, pp 328\u2013342","DOI":"10.1007\/3-540-45319-9_23"},{"key":"33_CR11","doi-asserted-by":"crossref","unstructured":"Ciardo G, Marmorstein R, Siminiceanu R (2003) Saturation unbound. In Tools and Algorithms for the Construction and Analysis of Systems, LNCS 2619. Springer-Verlag, pp 379\u2013393","DOI":"10.1007\/3-540-36577-X_27"},{"key":"33_CR12","doi-asserted-by":"crossref","unstructured":"Ciardo G, Siminiceanu R (2003) Structural symbolic CTL model checking of asynchronous systems. In Computer-Aided Verification, LNCS 2725. Springer-Verlag, pp 40\u201353","DOI":"10.1007\/978-3-540-45069-6_4"},{"key":"33_CR13","doi-asserted-by":"crossref","unstructured":"Ciardo G, Siminiceanu R (2002) Using edge-valued decision diagrams for symbolic generation of shortest paths. In Formal Methods in Computer-Aided Design, LNCS 2517. Springer-Verlag, pp 256\u2013273","DOI":"10.1007\/3-540-36126-X_16"},{"issue":"1","key":"33_CR14","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1016\/0166-5316(93)90026-Q","volume":"18","author":"G Ciardo","year":"1993","unstructured":"Ciardo G, Trivedi KS (1993) A decomposition approach for stochastic reward net models. Performance Evaluation 18(1):37\u201359","journal-title":"Performance Evaluation"},{"key":"33_CR15","doi-asserted-by":"crossref","unstructured":"Cimatti A, Clarke EM, Giunchiglia F, Roveri M (1999) NuSMV: A new Symbolic Model Verifier. In Computer-Aided Verification, LNCS 1633. Springer-Verlag, pp 495\u2013499","DOI":"10.1007\/3-540-48683-6_44"},{"key":"33_CR16","unstructured":"Clarke EM, Grumberg O, Peled DA (1999) Model Checking. MIT Press"},{"issue":"3","key":"33_CR17","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1016\/0196-6774(82)90023-2","volume":"3","author":"D Dolev","year":"1982","unstructured":"Dolev D, Klawe M, Rodeh M (1982) An O(n log n) unidirectional distributed algorithm for extrema finding in a circle. J Algorithms 3(3):245\u2013260","journal-title":"J Algorithms"},{"key":"33_CR18","doi-asserted-by":"crossref","unstructured":"Ezekiel J, L\u00fcttgen G (2006) Can Saturation be parallelised? On the parallelisation of a symbolic state-space generator. In Parallel and Distributed Methods in Verification, LNCS. Springer-Verlag, To appear.","DOI":"10.1007\/978-3-540-70952-7_23"},{"issue":"3","key":"33_CR19","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1145\/278298.278303","volume":"45","author":"P Fernandes","year":"1998","unstructured":"Fernandes P, Plateau B, Stewart WJ (1998) Efficient descriptor-vector multiplication in stochastic automata networks. J ACM 45(3):381\u2013414","journal-title":"J ACM"},{"issue":"1","key":"33_CR20","doi-asserted-by":"crossref","first-page":"6","DOI":"10.1109\/43.184839","volume":"12","author":"M Fujita","year":"1993","unstructured":"Fujita M, Fujisawa H, Matsunaga Y (1993) Variable ordering algorithms for ordered binary decision diagrams and their evaluation. IEEE Trans Comput-Aided Design Integrated Circuits Syst 12(1):6\u201312","journal-title":"IEEE Trans Comput-Aided Design Integrated Circuits Syst"},{"key":"33_CR21","doi-asserted-by":"crossref","unstructured":"Geldenhuys J, Valmari A (2001) Techniques for smaller intermediary BDDs. In Concurrency Theory, LNCS 2154. Springer-Verlag, pp 233\u2013247","DOI":"10.1007\/3-540-44685-0_16"},{"issue":"5","key":"33_CR22","doi-asserted-by":"crossref","first-page":"607","DOI":"10.1007\/BF01211911","volume":"8","author":"S Graf","year":"1996","unstructured":"Graf S, Steffen B, L\u00fcttgen G (1996) Compositional minimisation of finite state systems using interface specifications. Formal Aspects Comput 8(5):607\u2013616","journal-title":"Formal Aspects Comput"},{"key":"33_CR23","unstructured":"Holzmann G (2003) The Spin Model Checker: Primer and Reference Manual. Addison Wesley"},{"issue":"1\u20132","key":"33_CR24","first-page":"9","volume":"4","author":"T Kam","year":"1998","unstructured":"Kam T, Villa T, Brayton R, Sangiovanni-Vincentelli A (1998) Multi-valued decision diagrams: Theory and applications. Multiple-Valued Logic 4(1\u20132):9\u201362","journal-title":"Multiple-Valued Logic"},{"issue":"4","key":"33_CR25","doi-asserted-by":"crossref","first-page":"615","DOI":"10.1109\/32.541433","volume":"22","author":"P Kemper","year":"1996","unstructured":"Kemper P (1996) Numerical analysis of superposed GSPNs. IEEE Trans. Software Eng. 22(4):615\u2013628","journal-title":"IEEE Trans. Software Eng."},{"key":"33_CR26","doi-asserted-by":"crossref","unstructured":"Kimura S, Clarke EM (1990) A parallel algorithm for constructing binary decision diagrams. In Computer Design. IEEE Comp Soc Press, pp 220\u2013223","DOI":"10.1109\/ICCD.1990.130209"},{"key":"33_CR27","unstructured":"McMillan KL (1992) Symbolic model checking: An approach to the state explosion problem. PhD thesis, Carnegie Mellon University. CMU\u2013CS\u201392\u2013131"},{"issue":"8","key":"33_CR28","doi-asserted-by":"crossref","first-page":"559","DOI":"10.1109\/TSE.2006.81","volume":"32","author":"AS Miner","year":"2006","unstructured":"Miner AS (2006) Saturation for a general class of models. IEEE Trans Software Eng 32(8):559\u2013570","journal-title":"IEEE Trans Software Eng"},{"key":"33_CR29","doi-asserted-by":"crossref","unstructured":"Miner AS, Ciardo G (1999) Efficient reachability set generation and storage using decision diagrams. In Applications and Theory of Petri Nets, LNCS 1639. Springer-Verlag, pp 6\u201325","DOI":"10.1007\/3-540-48745-X_2"},{"issue":"4","key":"33_CR30","doi-asserted-by":"crossref","first-page":"541","DOI":"10.1109\/5.24143","volume":"77","author":"T Murata","year":"1989","unstructured":"Murata T (1989) Petri Nets: Properties, analysis and applications. Proc IEEE 77(4):541\u2013579","journal-title":"Proc IEEE"},{"key":"33_CR31","doi-asserted-by":"crossref","unstructured":"Narayan A, Isles AJ, Jain J, Brayton RK, Sangiovanni-Vincentelli A (1997) Reachability analysis using Partitioned-ROBDDs. In Computer-Aided Design. ACM and IEEE Comp Soc Press, pp 388\u2013393","DOI":"10.1109\/ICCAD.1997.643565"},{"key":"33_CR32","doi-asserted-by":"crossref","unstructured":"Pastor E, Roig O, Cortadella J, Badia R (1994) Petri net analysis using boolean manipulation. In Applications and Theory of Petri Nets, LNCS 815. Springer-Verlag, pp 416\u2013435","DOI":"10.1007\/3-540-58152-9_23"},{"key":"33_CR33","doi-asserted-by":"crossref","unstructured":"Plateau B (1985) On the stochastic structure of parallelism and synchronisation models for distributed algorithms. In ACM SIGMETRICS. ACM, pp 147\u2013153","DOI":"10.1145\/317786.317819"},{"key":"33_CR34","doi-asserted-by":"crossref","unstructured":"Ravi K, Somenzi F (1999) Hints to accelerate symbolic traversal. In Correct Hardware Design and Verification Methods, LNCS 1703. Springer-Verlag, pp 250\u2013264","DOI":"10.1007\/3-540-48153-2_19"},{"key":"33_CR35","doi-asserted-by":"crossref","unstructured":"Roig O, Cortadella J, Pastor E (1995) Verification of asynchronous circuits by BDD-based model checking of Petri nets. In Applications and Theory of Petri Nets, LNCS 935. Springer-Verlag, pp 374\u2013391","DOI":"10.1007\/3-540-60029-9_50"},{"issue":"3","key":"33_CR36","doi-asserted-by":"crossref","first-page":"238","DOI":"10.1016\/0743-7315(92)90006-9","volume":"15","author":"WH Sanders","year":"1992","unstructured":"Sanders WH, Malhis LM (1992) Dependability evaluation using composed SAN-based reward models. J Parallel Distributed Comput 15(3):238\u2013254","journal-title":"J Parallel Distributed Comput"},{"key":"33_CR37","unstructured":"Somenzi F (2001) CUDD: CU Decision Diagram Package, Release 2.3.1. University of Colorado at Boulder."},{"key":"33_CR38","unstructured":"Tilgner M, Takahashi Y, Ciardo G (1996) SNS 1.0: Synchronized Network Solver. In Manufacturing and Petri Nets, pp 215\u2013234"},{"key":"33_CR39","unstructured":"Valmari A (1990) A stubborn attack on the state explosion problem. In Computer-Aided Verification. AMS, pp 25\u201342"},{"key":"33_CR40","doi-asserted-by":"crossref","unstructured":"Yoneda T, Hatori H, Takahara A, Minato S-I (1996) BDDs vs. zero-suppressed BDDs for CTL symbolic model checking of Petri nets. In Formal Methods Comput Aided Design, LNCS 1166. Springer-Verlag, pp 435\u2013449","DOI":"10.1007\/BFb0031826"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-006-0033-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-006-0033-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-006-0033-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,10]],"date-time":"2023-05-10T09:52:11Z","timestamp":1683712331000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-006-0033-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,1,11]]},"references-count":40,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2007,6,14]]}},"alternative-id":["33"],"URL":"https:\/\/doi.org\/10.1007\/s10703-006-0033-y","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,1,11]]}}}