{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,5]],"date-time":"2026-06-05T03:04:09Z","timestamp":1780628649958,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":100,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540653066","type":"print"},{"value":"9783540494423","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/3-540-65306-6_21","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T18:42:45Z","timestamp":1330281765000},"page":"429-528","source":"Crossref","is-referenced-by-count":287,"title":["The state explosion problem"],"prefix":"10.1007","author":[{"given":"Antti","family":"Valmari","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"9_CR1","unstructured":"Aho, A. V., Hopcroft, J. E. & Ullman, J. D.: The Design and Analysis of Computer Algorithms. Addison-Wesley 1974, 470 p."},{"issue":"4","key":"9_CR2","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B. Alpern","year":"1985","unstructured":"Alpern, B. & Schneider, F. B.: \u201cDefining Liveness\u201d. Information Processing Letters 21(4), 1985, pp. 181\u2013185.","journal-title":"Information Processing Letters"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Alur, R., Brayton, R. K., Henzinger, T. A., Qadeer, S. & Rajamani, S. K.: \u201cPartial-Order Reduction in Symbolic State Space Exploration\u201d. Proc. Computer Aided Verification (CAV) '97, Lecture Notes in Computer Science 1254, Springer-Verlag 1997, pp. 340\u2013351.","DOI":"10.1007\/3-540-63166-6_34"},{"key":"9_CR4","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1016\/0169-7552(87)90085-7","volume":"14","author":"T. Bolognesi","year":"1987","unstructured":"Bolognesi, T. & Brinksma, E.: \u201cIntroduction to the ISO Specification Language LOTOS\u201d. Computer Networks and ISDN Systems 14 (1987), pp. 25\u201359.","journal-title":"Computer Networks and ISDN Systems"},{"key":"9_CR5","unstructured":"Brinksma, E.: \u201cA Theory for the Derivation of Tests\u201d. Protocol Specification, Testing and Verification VIII (Proc. International IFIP WG 6.1 Symposium, 1988), North-Holland 1988, pp. 63\u201374."},{"issue":"3","key":"9_CR6","doi-asserted-by":"crossref","first-page":"560","DOI":"10.1145\/828.833","volume":"31","author":"S. D. Brookes","year":"1984","unstructured":"Brookes, S. D., Hoare, C. A. R. & Roscoe, A. W.: \u201cA Theory of Communicating Sequential Processes\u201d. Journal of the ACM, 31 (3) 1984, pp. 560\u2013599.","journal-title":"Journal of the ACM"},{"key":"9_CR7","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/0304-3975(88)90098-9","volume":"59","author":"M. C. Browne","year":"1988","unstructured":"Browne, M. C., Clarke, E. M. & Grumberg, O.: \u201cCharacterizing Finite Kripke Structures in Propositional Temporal Logic\u201d. Theoretical Computer Science 59, 1988, pp. 115\u2013131.","journal-title":"Theoretical Computer Science"},{"issue":"8","key":"9_CR8","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. E. Bryant","year":"1986","unstructured":"Bryant, R. E.: \u201cGraph-Based Algorithms for Boolean Function Manipulation\u201d. IEEE Transactions on Computers C-35 (8) 1986, pp. 677\u2013691.","journal-title":"IEEE Transactions on Computers"},{"issue":"2","key":"9_CR9","doi-asserted-by":"crossref","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.: \u201cSymbolic Model Checking: 102\u00b0 States and Beyond\u201d. Information and Computation 98 (2) 1992, pp. 142\u2013170.","journal-title":"Information and Computation"},{"key":"9_CR10","unstructured":"Chandy, K. M. & Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley 1988, 516 p."},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"Clarke, E. M. & Emerson, E. A.: \u201cDesign and Synthesis of Synchronization Skeletons using Branching Time Temporal Logic\u201d. Proc. Workshop on Logics of Programs, Lecture Notes in Computer Science 131, Springer-Verlag 1981, pp. 52\u201371.","DOI":"10.1007\/BFb0025774"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Clarke, E. M., Filkorn, T. & Jha, S.: \u201cExploiting Symmetry in Temporal Logic Model Checking\u201d. Proc. Computer-Aided Verification (CAV) '93, Lecture Notes in Computer Science 697, Springer-Verlag 1993, pp. 450\u2013462.","DOI":"10.1007\/3-540-56922-7_37"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Clarke, E. M., Grumberg, O. & Jha, S.: \u201cVerifying Parameterized Networks using Abstraction and Regular Languages\u201d. Proc. CONCUR '95, 6th International Conference on Concurrency Theory, Lecture Notes in Computer Science 962, Springer-Verlag 1995, pp. 395\u2013407.","DOI":"10.1007\/3-540-60218-6_30"},{"issue":"1","key":"9_CR14","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF01211314","volume":"5","author":"R. Cleaveland","year":"1993","unstructured":"Cleaveland, R. & Hennessy, M.: \u201cTesting Equivalence as a Bisimulation Equivalence\u201d. Formal Aspects of Computing, 5 (1) 1993, pp. 1\u201320.","journal-title":"Formal Aspects of Computing"},{"key":"9_CR15","unstructured":"Cormen, T. H., Leiserson, C. E. & Rivest, R. L.: Introduction to Algorithms. The MIT Press, 1990, 1028 p."},{"key":"9_CR16","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C. Courcoubetis","year":"1992","unstructured":"Courcoubetis, C., Vardi, M., Wolper, P. & Yannakakis, M.: \u201cMemory-Efficient Algorithms for the Verification of Temporal Properties\u201d, Formal Methods in System Design 1 (1992), pp. 275\u2013288.","journal-title":"Formal Methods in System Design"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"Desel, J. & Esparza, J.: Free Choice Petri Nets. Cambridge Tracts in Theoretical Computer Science 40, Cambridge University Press 1995, 244 p.","DOI":"10.1017\/CBO9780511526558"},{"key":"9_CR18","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1016\/S0304-3975(96)00281-2","volume":"179","author":"J. Eloranta","year":"1997","unstructured":"Eloranta, J., Tienari, M. & Valmari, A.: \u201cEssential Transitions to Bisimulation Equivalences\u201d. Theoretical Computer Science 179 (1997) pp. 397\u2013419.","journal-title":"Theoretical Computer Science"},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"Emerson, E. A.: \u201cTemporal and Modal Logic\u201d. Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, Elsevier Science Publishers 1990, pp. 995\u20131072.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"issue":"1","key":"9_CR20","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E. A. Emerson","year":"1986","unstructured":"Emerson, E. A., & Halpern, J. Y.: \u201c'Sometimes\u2019 and \u2018Not Never\u2019 Revisited: on Branching Versus Linear Time Temporal Logic\u201d. Journal of the ACM 33 (1) 1986, pp. 151\u2013178.","journal-title":"Journal of the ACM"},{"key":"9_CR21","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1016\/0167-6423(87)90036-0","volume":"8","author":"E. A. Emerson","year":"1987","unstructured":"Emerson, E. A., & Lei, C.-L.: \u201cModalities for Model Checking: Branching Time Strikes Back\u201d. Science of Computer Programming, 8, 1987, pp. 275\u2013306.","journal-title":"Science of Computer Programming"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Emerson, E. A. & Sistla, A. P.: \u201cSymmetry and Model Checking\u201d. Proc. Computer-Aided Verification (CAV) '93, Lecture Notes in Computer Science 697, Springer-Verlag 1993, pp. 463\u2013477.","DOI":"10.1007\/3-540-56922-7_38"},{"issue":"4","key":"9_CR23","doi-asserted-by":"crossref","first-page":"617","DOI":"10.1145\/262004.262008","volume":"19","author":"E. A. Emerson","year":"1997","unstructured":"Emerson, E. A. & Sistla, A. P.: \u201cUtilizing Symmetry when Model-Checking under Fairness Assumptions: An Automata-Theoretic Approach\u201d. ACM Transactions on Programming Languages and Systems, 19 (4) 1997, pp. 617\u2013638.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"9_CR24","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1016\/0167-6423(94)00019-0","volume":"23","author":"J. Esparza","year":"1994","unstructured":"Esparza, J.: \u201cModel Checking Using Net Unfoldings\u201d. Science of Computer Programming (1994) 23: 151\u2013195.","journal-title":"Science of Computer Programming"},{"key":"9_CR25","doi-asserted-by":"crossref","unstructured":"Esparza, J., R\u00f6mer, S. & Vogler, W.: \u201cAn Improvement of McMillan's Unfolding Algorithm\u201d. Proc. Tools and Algorithms for the Construction and Analysis of Systems '96, Lecture Notes in Computer Science 1055, Springer-Verlag 1996, pp. 87\u2013106.","DOI":"10.1007\/3-540-61042-1_40"},{"key":"9_CR26","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1016\/0167-6423(90)90071-K","volume":"13","author":"J.-C. Fernandez","year":"1989\/90","unstructured":"Fernandez, J.-C.: \u201cAn Implementation of an Efficient Algorithm for Bisimulation Equivalence\u201d. Science of Computer Programming 13 (1989\/90) pp. 219\u2013236.","journal-title":"Science of Computer Programming"},{"key":"9_CR27","doi-asserted-by":"crossref","unstructured":"Finkel, A.: \u201cThe Minimal Coverability Graph for Petri Nets\u201d. Advances in Petri Nets 1993, Lecture Notes in Computer Science 674, pp. 210\u2013243.","DOI":"10.1007\/3-540-56689-9_45"},{"key":"9_CR28","doi-asserted-by":"crossref","unstructured":"Francez, N.: Fairness. Springer-Verlag 1986, 295 p.","DOI":"10.1007\/978-1-4612-4886-6"},{"key":"9_CR29","unstructured":"Francez, N.: Program Verification. Addison-Wesley 1992, 312 p."},{"key":"9_CR30","unstructured":"Garey, M. R. & Johnson, D. S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman and Company, 1979, 340 p."},{"key":"9_CR31","doi-asserted-by":"crossref","unstructured":"Gerth, R., Kuiper, R., Peled, D. & Penczek, W.: \u201cA Partial Order Approach to Branching Time Logic Model Checking\u201d. Proc. Third Israel Symposium on the Theory of Computing and Systems, IEEE 1995, pp. 130\u2013139.","DOI":"10.1109\/ISTCS.1995.377038"},{"key":"9_CR32","doi-asserted-by":"crossref","unstructured":"Gerth, R., Peled, D., Vardi, M. & Wolper, P.: \u201cSimple On-the-fly Automatic Verification of Linear Temporal Logic\u201d. Proc. Protocol Specification, Testing and Verification 1995, Chapman & Hall 1995, pp. 3\u201318.","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"9_CR33","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: \u201cUsing Partial Orders to Improve Automatic Verification Methods\u201d. Proc. Computer-Aided Verification 90, AMS-ACM DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol. 3, 1991, pp. 321\u2013340.","DOI":"10.1090\/dimacs\/003\/21"},{"key":"9_CR34","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems, An Approach to the State-Explosion Problem. Lecture Notes in Computer Science 1032, Springer-Verlag 1996, 143 p. (Earlier version: Ph.D. Thesis, University of Li\u00e9ge, 1994.)","DOI":"10.1007\/3-540-60761-7"},{"key":"9_CR35","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Holzmann, G. J. & Pirottin, D.: \u201cState Space Caching Revisited\u201d. Proc. Computer-Aided Verification (CAV) '92, Lecture Notes in Computer Science 663, Springer-Verlag 1993, pp. 178\u2013191.","DOI":"10.1007\/3-540-56496-9_15"},{"key":"9_CR36","doi-asserted-by":"crossref","unstructured":"Godefroid, P. & Pirottin, D.: \u201cRefining Dependencies Improves Partial-Order Verification Methods\u201d. Proc. Computer-Aided Verification (CAV) '9.3, Lecture Notes in Computer Science 697, Springer-Verlag 1993, pp. 438\u2013449.","DOI":"10.1007\/3-540-56922-7_36"},{"key":"9_CR37","doi-asserted-by":"crossref","unstructured":"Godefroid, P., & Wolper, P.: \u201cUsing Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties\u201d. Proc. Computer Aided Verification (CAV) '91, Lecture Notes in Computer Science 575, Springer-Verlag 1992, pp. 332\u2013342.","DOI":"10.1007\/3-540-55179-4_32"},{"key":"9_CR38","doi-asserted-by":"crossref","unstructured":"Graf, S. & Steffen, B.: \u201cCompositional Minimization of Finite State Processes\u201d. Proc. Computer-Aided Verification '90, AMS-ACM DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol. 3, 1991, pp. 57\u201373.","DOI":"10.1090\/dimacs\/003\/06"},{"key":"9_CR39","doi-asserted-by":"crossref","unstructured":"Gyuris, V. & Sistla, P.: \u201cOn-the-Fly Model Checking Under Fairness That Exploits Symmetry\u201d. Proc. Computer Aided Verification (CAV) '97, Lecture Notes in Computer Science 1254, Springer-Verlag 1997, pp. 232\u2013243.","DOI":"10.1007\/3-540-63166-6_24"},{"key":"9_CR40","doi-asserted-by":"crossref","unstructured":"Haddad, S.: \u201cA Reduction Theory for Coloured Nets\u201d. Advances in Petri Nets 1989, Lecture Notes in Computer Science 424, Springer-Verlag 1990, pp. 209\u2013235. Also in High-level Petri Nets. Theory and Application, Springer-Verlag 1991, pp. 399\u2013425.","DOI":"10.1007\/3-540-52494-0_31"},{"issue":"4","key":"9_CR41","doi-asserted-by":"crossref","first-page":"896","DOI":"10.1145\/4221.4249","volume":"32","author":"M. Hennessy","year":"1985","unstructured":"Hennessy, M.: \u201cAcceptance Trees\u201d. Journal of the ACM, 32 (4) 1985, pp. 896\u2013928.","journal-title":"Journal of the ACM"},{"key":"9_CR42","unstructured":"Hoare, C. A. R.: Communicating Sequential Processes. Prentice-Hall 1985, 256 p."},{"key":"9_CR43","unstructured":"Holzmann, G. J.: Design and Validation of Computer Protocols. Prentice-Hall 1991, 500 p."},{"key":"9_CR44","unstructured":"ISO 8807 International Standard: Information processing systems \u2014 Open Systems Interconnection \u2014 LOTOS \u2014 A formal description technique based on the temporal ordering of observational behaviour. International Organization for Standardization 1989, 142 p."},{"key":"9_CR45","doi-asserted-by":"crossref","unstructured":"Jard, C. & J\u00e9ron, T.: \u201cBounded-memory Algorithms for Verification On-the-fly\u201d. Proc. Computer Aided Verification (CA V) '91, Lecture Notes in Computer Science 575, Springer-Verlag 1992, pp. 192\u2013202.","DOI":"10.1007\/3-540-55179-4_19"},{"key":"9_CR46","doi-asserted-by":"crossref","unstructured":"Jensen, K.: Coloured Petri Nets. Volume 2, Analysis Methods. Monographs in Theoretical Computer Science, Springer-Verlag 1995, 174 p.","DOI":"10.1007\/978-3-662-03241-1"},{"key":"9_CR47","doi-asserted-by":"crossref","unstructured":"Kaivola, R. & Valmari, A.: \u201cThe Weakest Compositional Semantic Equivalence Preserving Nexttime-less Linear Temporal Logic\u201d. Proc. CONCUR '92, Third International Conference on Concurrency Theory, Lecture Notes in Computer Science 630, Springer-Verlag 1992, pp. 207\u2013221.","DOI":"10.1007\/BFb0084793"},{"key":"9_CR48","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1016\/0890-5401(90)90025-D","volume":"86","author":"P. C. Kanellakis","year":"1990","unstructured":"Kanellakis, P. C. & Smolka, S. A.: \u201cCCS Expressions, Finite State Processes, and Three Problems of Equivalence\u201d. Information and Computation 86 (1990) pp. 43\u201368.","journal-title":"Information and Computation"},{"key":"9_CR49","doi-asserted-by":"crossref","unstructured":"Katz, S. & Peled, D.: \u201cAn Efficient Verification Method for Parallel and Distributed Programs\u201d. Proc. Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency 1988, Lecture Notes in Computer Science 354, Springer-Verlag 1989, pp. 489\u2013507.","DOI":"10.1007\/BFb0013032"},{"key":"9_CR50","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1016\/0304-3975(92)90054-J","volume":"101","author":"S. Katz","year":"1992","unstructured":"Katz, S. & Peled, D.: \u201cDefining Conditional Independence Using Collapses\u201d. Theoretical Computer Science 101 (1992), pp. 337\u2013359.","journal-title":"Theoretical Computer Science"},{"key":"9_CR51","first-page":"105","volume-title":"A Verification-Oriented Theory of Data in Labelled Transition Systems","author":"I. Kokkarinen","year":"1998","unstructured":"Kokkarinen, I.: A Verification-Oriented Theory of Data in Labelled Transition Systems. Ph.D. Thesis, Tampere University of Technology Publications 234, Tampere, Finland 1998, 105 p."},{"key":"9_CR52","doi-asserted-by":"crossref","unstructured":"Kokkarinen, I., Peled, D. & Valmari, A.: \u201cRelaxed Visibility Enhances Partial Order Reduction\u201d. Proc. Computer Aided Verification (CAV) '97, Lecture Notes in Computer Science 1254, Springer-Verlag 1997, pp. 328\u2013339.","DOI":"10.1007\/3-540-63166-6_33"},{"key":"9_CR53","doi-asserted-by":"crossref","unstructured":"Kristensen, L. M. & Valmari, A.: \u201cFinding Stubborn Sets of Coloured Petri Nets Without Unfolding\u201d. To appear in Proc. International Conference on Application and Theory of Petri Nets, 1998, 20 p.","DOI":"10.1007\/3-540-69108-1_7"},{"key":"9_CR54","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1007\/BF01383832","volume":"5","author":"R. P. Kurshan","year":"1994","unstructured":"Kurshan, R. P., Merritt, M., Orda, A. & Sachs, S. R.: \u201cA Structural Linearization Principle for Processes\u201d. Formal Methods in System Design 5, 1994, pp. 227\u2013244.","journal-title":"Formal Methods in System Design"},{"issue":"2","key":"9_CR55","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"SE-3","author":"L. Lamport","year":"1977","unstructured":"Lamport, L.: \u201cProving the Correctness of Multiprocess Programs\u201d. IEEE Transactions on Software Engineering, SE-3(2), 1977, pp. 125\u2013143.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"9_CR56","doi-asserted-by":"crossref","unstructured":"Lamport, L. & Lynch, N.: \u201cDistributed Computing: Models and Methods\u201d. Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, Elsevier Science Publishers 1990, pp. 1157\u20131199.","DOI":"10.1016\/B978-0-444-88074-1.50023-8"},{"key":"9_CR57","doi-asserted-by":"crossref","unstructured":"Lichtenstein, O. & Pnueli, A.: \u201cChecking that Finite State Concurrent Programs Satisfy Their Linear Specifications\u201d. Proc. 12th ACM Symposium on Principles of Programming Languages, 1985, pp. 97\u2013107.","DOI":"10.1145\/318593.318622"},{"key":"9_CR58","unstructured":"Madelaine, E. & Vergamini, D.: \u201cAUTO: A Verification Tool for Distributed Systems Using Reduction of Finite Automata Networks\u201d. Proc. Formal Description Techniques II (FORTE '89), North-Holland 1990, pp. 61\u201366."},{"key":"9_CR59","doi-asserted-by":"crossref","unstructured":"Manna, Z. & Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems, Volume I: Specification. Springer-Verlag 1992, 427 p.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"9_CR60","doi-asserted-by":"crossref","unstructured":"Manna, Z. & Pnueli, A.: Temporal Verification of Reactive Systems, Volume II: Safety. Springer-Verlag 1995, 512 p.","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"9_CR61","doi-asserted-by":"crossref","unstructured":"Mazurkiewicz, A.: \u201cTrace Theory\u201d. Petri Nets: Applications and Relationships to Other Models of Concurrency, Lecture Notes in Computer Science 255, Springer-Verlag 1987, pp. 279\u2013324.","DOI":"10.1007\/3-540-17906-2_30"},{"key":"9_CR62","doi-asserted-by":"crossref","unstructured":"McMillan, K.: \u201cUsing Unfoldings to Avoid the State Explosion Problem in the Verification of Asynchronous Circuits\u201d. Proc. Computer-Aided Verification (CAV) '92, Lecture Notes in Computer Science 663, Springer-Verlag 1993, pp. 164\u2013177.","DOI":"10.1007\/3-540-56496-9_14"},{"key":"9_CR63","first-page":"171","volume":"64","author":"C. Meinel","year":"1998","unstructured":"Meinel, C. & Theobald, T.: \u201cOrdered Binary Decision Diagrams and Their Significance in Computer-Aided Design of VLSI Circuits\u201d. Bulletin of the European Association for Theoretical Computer Science 64, 1998, pp. 171\u2013187.","journal-title":"Bulletin of the European Association for Theoretical Computer Science"},{"key":"9_CR64","doi-asserted-by":"crossref","unstructured":"Melzer, S. & R\u00f6mer, S.: \u201cDeadlock Checking Using Net Unfoldings\u201d. Proc. Computer Aided Verification (CAV) '97, Lecture Notes in Computer Science 1254, Springer-Verlag 1997, pp. 352\u2013363.","DOI":"10.1007\/3-540-63166-6_35"},{"key":"9_CR65","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall 1989, 260 p."},{"key":"9_CR66","doi-asserted-by":"crossref","unstructured":"Park, D.: \u201cConcurrency and Automata on Infinite Sequences\u201d. Theoretical Computer Science: 5th GI-Conference, Lecture Notes in Computer Science 104, Springer-Verlag 1981, pp. 167\u2013183.","DOI":"10.1007\/BFb0017309"},{"key":"9_CR67","doi-asserted-by":"crossref","unstructured":"Pastor, E., Roig, O., Cortadella, J. & Badia, R.: \u201cPetri Net Analysis Using Boolean Manipulation\u201d. Proc. Application and Theory of Petri Nets 1994, Lecture Notes in Computer Science 815, Springer-Verlag 1994, pp. 416\u2013435.","DOI":"10.1007\/3-540-58152-9_23"},{"key":"9_CR68","doi-asserted-by":"crossref","unstructured":"Peled, D.: \u201cAll from One, One for All: On Model Checking Using Representatives\u201d. Proc. Computer-Aided Verification (CA V) '93, Lecture Notes in Computer Science 697, Springer-Verlag 1993, pp. 409\u2013423.","DOI":"10.1007\/3-540-56922-7_34"},{"issue":"1","key":"9_CR69","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/BF00121262","volume":"8","author":"D. Peled","year":"1996","unstructured":"Peled, D.: \u201cCombining Partial Order Reductions with On-the-fly Model-Checkingrd. Formal Methods in System Design 8 (1) 1996: 39\u201364.","journal-title":"Formal Methods in System Design"},{"key":"9_CR70","doi-asserted-by":"crossref","unstructured":"Peled, D.: \u201cPartial Order Reduction: Linear and Branching Temporal Logics and Process Algebras\u201d. Proc. POMIV'96, Workshop on Partial Order Methods in Verification, DIMACS Series in Discrete Mathematics and Theoretical Computer Science Vol. 29, American Mathematical Society 1997, pp. 233\u2013257.","DOI":"10.1090\/dimacs\/029\/13"},{"key":"9_CR71","unstructured":"Puhakka, A. & Valmari, A.: \u201cVerification of Self-Synchronizing Alternating Bit Protocols with ARA\u201d. Proc. Fifth Symposium on Programming Languages and Software Tools, University of Helsinki, Department of Computer Science, Report C-1997-37, pp. 167\u2013178."},{"key":"9_CR72","series-title":"Research Report A-14","volume-title":"A Comparative Study of Methods for Efficient Reachability Analysis","author":"M. Rauhamaa","year":"1990","unstructured":"Rauhamaa, M.: A Comparative Study of Methods for Efficient Reachability Analysis. Lic.Tech. Thesis, Helsinki University of Technology, Digital Systems Laboratory, Research Report A-14, Espoo, Finland 1990, 61 p."},{"key":"9_CR73","unstructured":"Reisig, W.: Petri Nets, An Introduction. EATCS Monographs on Theoretical Computer Science, Vol. 4, Springer-Verlag 1985, 161 p."},{"key":"9_CR74","unstructured":"Roscoe, A. W.: \u201cModel-Checking CSP\u201d. A Classical Mind: Essays in Honour of C. A. R. Hoare, Prentice-Hall 1994, pp. 353\u2013378."},{"key":"9_CR75","unstructured":"Roscoe, A. W.: The Theory and Practice of Concurrency. Prentice-Hall 1998, 565 p."},{"key":"9_CR76","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/S0022-0000(70)80006-X","volume":"4","author":"W. J. Savitch","year":"1970","unstructured":"Savitch, W. J.: \u201cRelationships Between Nondeterministic and Deterministic Tape Complexities\u201d. Journal of Computer and System Sciences 4, 1970, pp. 177\u2013192.","journal-title":"Journal of Computer and System Sciences"},{"issue":"12","key":"9_CR77","doi-asserted-by":"crossref","first-page":"1307","DOI":"10.1109\/71.553301","volume":"7","author":"S. M. Shatz","year":"1996","unstructured":"Shatz, S. M., Tu, S., Murata, T. & Duri, S.: \u201cApplication of Petri Net Reduction for Ada Tasking Deadlock Analysis\u201d. IEEE Transactions on Parallel and Distributed Systems 7 (12) 1996, pp. 1307\u20131322.","journal-title":"IEEE Transactions on Parallel and Distributed Systems"},{"issue":"3","key":"9_CR78","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A. P. Sistla","year":"1985","unstructured":"Sistla, A. P. & Clarke, E. M.: \u201cThe Complexity of Propositional Linear Temporal Logics\u201d. Journal of the ACM 32 (3) 1985, pp. 733\u2013749.","journal-title":"Journal of the ACM"},{"issue":"2","key":"9_CR79","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"R. E. Tarjan","year":"1972","unstructured":"Tarjan, R. E.: \u201cDepth-first Search and Linear Graph Algorithms\u201d. SIAM Journal on Computing, 1 (2) 1972, pp. 146\u2013160.","journal-title":"SIAM Journal on Computing"},{"key":"9_CR80","doi-asserted-by":"crossref","unstructured":"Thomas, W.: \u201cAutomata on Infinite Objects\u201d. Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, Elsevier Science Publishers 1990, pp. 133\u2013191.","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"9_CR81","unstructured":"Valmari, A.: \u201cError Detection by Reduced Reachability Graph Generation\u201d. Proc. 9th European Workshop on Application and Theory of Petri Nets, 1988, pp. 95\u2013112."},{"key":"9_CR82","volume-title":"State Space Generation: Efficiency and Practicality","author":"A. Valmari","year":"1988","unstructured":"Valmari, A.: State Space Generation: Efficiency and Practicality. Ph.D. Thesis, Tampere University of Technology Publications 55, Tampere, Finland 1988, 169 p."},{"key":"9_CR83","doi-asserted-by":"crossref","unstructured":"Valmari, A.: \u201cStubborn Sets for Reduced State Space Generation\u201d. Advances in Petri Nets 1990, Lecture Notes in Computer Science 483, Springer-Verlag 1991, pp. 491\u2013515.","DOI":"10.1007\/3-540-53863-1_36"},{"key":"9_CR84","unstructured":"Valmari, A.: \u201cStubborn Sets of Coloured Petri Nets\u201d. Proc. 12th International Conference on Application and Theory of Petri Nets, 1991, pp. 102\u2013121."},{"key":"9_CR85","series-title":"Report A-1992-4","volume-title":"Alleviating State Explosion during Verification of Behavioural Equivalence","author":"A. Valmari","year":"1992","unstructured":"Valmari, A.: Alleviating State Explosion during Verification of Behavioural Equivalence. Department of Computer Science, University of Helsinki, Report A-1992-4, Helsinki, Finland 1992, 57 p."},{"key":"9_CR86","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/BF00709154","volume":"1","author":"A. Valmari","year":"1992","unstructured":"Valmari, A.: \u201cA Stubborn Attack on State Explosion\u201d. Formal Methods in System Design, 1: 297\u2013322 (1992).","journal-title":"Formal Methods in System Design"},{"key":"9_CR87","doi-asserted-by":"crossref","unstructured":"Valmari, A.: \u201cOn-the-fly Verification with Stubborn Sets\u201d. Proc. Computer-Aided Verification (CAV) '93, Lecture Notes in Computer Science 697, Springer-Verlag 1993, pp. 397\u2013408.","DOI":"10.1007\/3-540-56922-7_33"},{"key":"9_CR88","doi-asserted-by":"crossref","unstructured":"Valmari, A.: \u201cCompositional Analysis with Place-Bordered Subnets\u201d. Proc. Application and Theory of Petri Nets 1994, Lecture Notes in Computer Science 815, Springer-Verlag 1994, pp. 531\u2013547.","DOI":"10.1007\/3-540-58152-9_29"},{"key":"9_CR89","doi-asserted-by":"crossref","unstructured":"Valmari, A.: \u201cFailure-based Equivalences Are Faster Than Many Believe\u201d. Proc. Structures in Concurrency Theory 1995, Springer-Verlag \u201cWorkshops in Computing\u201d series, 1995, pp. 326\u2013340.","DOI":"10.1007\/978-1-4471-3078-9_22"},{"key":"9_CR90","doi-asserted-by":"crossref","unstructured":"Valmari, A.: \u201cCompositionality in State Space Verification Methods\u201d. Invited talk, Proc. Application and Theory of Petri Nets 1996, Lecture Notes in Computer Science 1091, Springer-Verlag 1996, pp. 29\u201356.","DOI":"10.1007\/3-540-61363-3_3"},{"key":"9_CR91","doi-asserted-by":"crossref","unstructured":"Valmari, A.: \u201cStubborn Set Methods for Process Algebras\u201d. Proc. POMIV'96, Workshop on Partial Order Methods in Verification, DIMACS Series in Discrete Mathematics and Theoretical Computer Science Vol. 29, American Mathematical Society 1997, pp. 213\u2013231.","DOI":"10.1090\/dimacs\/029\/12"},{"key":"9_CR92","unstructured":"Valmari, A. & Kokkarinen, I.: \u201cUnbounded Verification Results by Finite-State Compositional Techniques: 10any States and Beyond\u201d. Proc. 1998 International Conference on Application of Concurrency to System Design, IEEE Computer Society 1998, pp. 75\u201385."},{"key":"9_CR93","unstructured":"Valmari, A. & Tienari, M.: \u201cAn Improved Failures Equivalence for Finite-State Systems with a Reduction Algorithm\u201d. Proc. Protocol Specification, Testing and Verification XI, North-Holland 1991, pp. 3\u201318."},{"key":"9_CR94","doi-asserted-by":"crossref","first-page":"440","DOI":"10.1007\/BF01211218","volume":"7","author":"A. Valmari","year":"1995","unstructured":"Valmari, A. & Tienari, M.: \u201cCompositional Failure-Based Semantic Models for Basic LOTOS\u201d. Formal Aspects of Computing (1995) 7: 440\u2013468.","journal-title":"Formal Aspects of Computing"},{"key":"9_CR95","doi-asserted-by":"crossref","unstructured":"van Glabbeek, R.: \u201cThe Linear Time \u2014 Branching Time Spectrum II: The Semantics of Sequential Systems with Silent Moves\u201d. Proc. CONCUR '93, Fourth International Conference on Concurrency Theory, Lecture Notes in Computer Science 715, Springer-Verlag 1993, pp. 66\u201381.","DOI":"10.1007\/3-540-57208-2_6"},{"key":"9_CR96","unstructured":"van Glabbeek, R. & Weijland, W.: \u201cBranching Time and Abstraction in Bisimulation Semantics (Extended Abstract)\u201d. Proc. IFIP International Conference on Information Processing '89, North-Holland 1989, pp. 613\u2013618."},{"key":"9_CR97","unstructured":"Vardi, M. Y. & Wolper, P.: \u201cAn Automata-Theoretic Approach to Automatic Program Verification\u201d. Proc. IEEE Symposium on Logic in Computer Science, 1986, pp. 332\u2013344."},{"key":"9_CR98","series-title":"Research Report A-51","first-page":"105","volume-title":"On the Stubborn Set Method in Reduced State Space Generation","author":"K. Varpaaniemi","year":"1998","unstructured":"Varpaaniemi, K.: On the Stubborn Set Method in Reduced State Space Generation. Ph.D. Thesis, Helsinki University of Technology, Digital Systems Laboratory, Research Report A-51, Espoo, Finland 1998, 105 p."},{"key":"9_CR99","doi-asserted-by":"crossref","unstructured":"Wolper, P.: \u201cExpressing Interesting Properties of Programs in Propositional Temporal Logic\u201d. Proc. 13th ACM Symposium on Principles of Programming Languages, 1986, pp. 184\u2013193.","DOI":"10.1145\/512644.512661"},{"key":"9_CR100","doi-asserted-by":"crossref","unstructured":"Wolper, P. & Lovinfosse, V.: \u201cVerifying Properties of Large Sets of Processes with Network Invariants\u201d. Proc. Workshop on Automatic Verification Methods for Finite State Systems, Lecture Notes in Computer Science 407, Springer-Verlag 1989, pp. 68\u201380.","DOI":"10.1007\/3-540-52148-8_6"}],"container-title":["Lecture Notes in Computer Science","Lectures on Petri Nets I: Basic Models"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-65306-6_21.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:20:55Z","timestamp":1605630055000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-65306-6_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540653066","9783540494423"],"references-count":100,"URL":"https:\/\/doi.org\/10.1007\/3-540-65306-6_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1998]]}}}