{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:25:01Z","timestamp":1761611101573,"version":"build-2065373602"},"reference-count":70,"publisher":"Elsevier BV","issue":"1-2","license":[{"start":{"date-parts":[[2003,5,1]],"date-time":"2003-05-01T00:00:00Z","timestamp":1051747200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2003,5,1]],"date-time":"2003-05-01T00:00:00Z","timestamp":1051747200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2013,8,22]],"date-time":"2013-08-22T00:00:00Z","timestamp":1377129600000},"content-version":"vor","delay-in-days":3766,"URL":"http:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["The Journal of Logic and Algebraic Programming"],"published-print":{"date-parts":[[2003,5]]},"DOI":"10.1016\/s1567-8326(02)00066-8","type":"journal-article","created":{"date-parts":[[2003,5,12]],"date-time":"2003-05-12T20:23:48Z","timestamp":1052771028000},"page":"23-67","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":47,"title":["On the use of MTBDDs for performability analysis and verification of stochastic systems"],"prefix":"10.1016","volume":"56","author":[{"given":"Holger","family":"Hermanns","sequence":"first","affiliation":[]},{"given":"Marta","family":"Kwiatkowska","sequence":"additional","affiliation":[]},{"given":"Gethin","family":"Norman","sequence":"additional","affiliation":[]},{"given":"David","family":"Parker","sequence":"additional","affiliation":[]},{"given":"Markus","family":"Siegle","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"year":"1994","series-title":"Markov Decision Processes","author":"Puterman","key":"10.1016\/S1567-8326(02)00066-8_BIB1"},{"issue":"4","key":"10.1016\/S1567-8326(02)00066-8_BIB2","doi-asserted-by":"crossref","first-page":"857","DOI":"10.1145\/210332.210339","article-title":"The complexity of probabilistic verification","volume":"42","author":"Courcoubetis","year":"1995","journal-title":"Journal of the ACM"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB3","unstructured":"R. Segala, Modelling and verification of randomized distributed real time systems, Ph.D. thesis, Massachusetts Institute of Technology, 1995"},{"year":"1989","series-title":"Communication and Concurrency","author":"Milner","key":"10.1016\/S1567-8326(02)00066-8_BIB4"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB5","series-title":"The Formal Description Technique LOTOS","first-page":"23","article-title":"Introduction to the ISO specification language LOTOS","author":"Bolognesi","year":"1989"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB6","doi-asserted-by":"crossref","unstructured":"N. G\u00f6tz, U. Herzog, M. Rettelbach, Multiprocessor and distributed system design: The integration of functional specification and performance analysis using stochastic process algebras, in: Proceedings of the 16th International Symposium on Computer Performance Modelling, Measurement and Evaluation, PERFORMANCE 1993, Tutorial, vol. 729 of Lecture Notes in Computer Science, Springer, 1993, pp. 121\u2013146","DOI":"10.1007\/BFb0013851"},{"year":"1996","series-title":"A Compositional Approach to Performance Modelling","author":"Hillston","key":"10.1016\/S1567-8326(02)00066-8_BIB7"},{"issue":"1\u20132","key":"10.1016\/S1567-8326(02)00066-8_BIB8","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1016\/S0304-3975(00)00305-4","article-title":"Process algebra for performance evaluation","volume":"274","author":"Hermanns","year":"2002","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB9","doi-asserted-by":"crossref","unstructured":"P. Courtois, Decomposability, queueing and computer system applications, ACM monograph series, 1977","DOI":"10.1016\/B978-0-12-193750-8.50011-8"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB10","doi-asserted-by":"crossref","unstructured":"B. Plateau, On the synchronization structure of parallelism and synchronization models for distributed algorithms, in: Proceedings of the ACM Sigmetrics Conference on Measurement and Modeling of Computer Systems, Austin, TX, 1985, pp. 147\u2013154","DOI":"10.1145\/317795.317819"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB11","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1007\/BF01189232","article-title":"A class of hierarchical queueing networks and their analysis","volume":"15","author":"Buchholz","year":"1994","journal-title":"Queueing Systems"},{"issue":"1","key":"10.1016\/S1567-8326(02)00066-8_BIB12","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/S0167-6423(99)00019-2","article-title":"Automated compositional Markov chain generation for a plain-old telephony system","volume":"36","author":"Hermanns","year":"1999","journal-title":"Science of Computer Programming"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB13","unstructured":"M. Siegle, Structured Markovian performance modelling with automatic symmetry exploitation, in: G. Haring, H. Wabnig (Eds.), Short Papers and Tool Descriptions Proceedings of the 7th International Conference on Modelling Techniques and Tools for Computer Performance Evaluation, Vienna, Austria, 1994, pp. 77\u201381"},{"issue":"8","key":"10.1016\/S1567-8326(02)00066-8_BIB14","first-page":"677","article-title":"Graph-based algorithms for boolean function manipulation","volume":"C-35","author":"Bryant","year":"1986","journal-title":"IEEE ToC"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB15","doi-asserted-by":"crossref","unstructured":"R. Bahar, E. Frohm, C. Gaona, G. Hachtel, E. Macii, A. Pardo, F. Somenzi, Algebraic decision diagrams and their applications, in: ICCAD-93: International Conference on Computer-Aided Design, ACM\/IEEE, Santa Clara, CA, 1993, pp. 188\u2013191, also available in Formal Methods in System Design 10 (2\/3) 1997","DOI":"10.1109\/ICCAD.1993.580054"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB16","doi-asserted-by":"crossref","unstructured":"E. Clarke, M. Fujita, P. McGeer, K. McMillan, J. Yang, X. Zhao, Multi-terminal binary decision diagrams: an efficient data structure for matrix representation, in: Proceedings of International Workshop on Logic Synthesis (IWLS\u201993), Tahoe City, 1993, pp. 6a:1\u201315, also available in Formal Methods in System Design 10 (2\/3) (1997) 149\u2013169","DOI":"10.1023\/A:1008647823331"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB17","series-title":"Proceedings of 10th IEEE Real-Time Systems Symposium","first-page":"102","article-title":"A framework for reasoning about time and reliability","author":"Hansson","year":"1990"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB18","doi-asserted-by":"crossref","unstructured":"C. Baier, B. Haverkort, H. Hermanns, J.-P. Katoen, On the logical characterisation of performability properties, in: ICALP, vol. 1853 of Lecture Notes in Computer Science, Springer, 2000, pp. 780\u2013792","DOI":"10.1007\/3-540-45022-X_65"},{"issue":"9\u201310","key":"10.1016\/S1567-8326(02)00066-8_BIB19","doi-asserted-by":"crossref","first-page":"901","DOI":"10.1016\/S0169-7552(97)00133-5","article-title":"Stochastic process algebras\u2013\u2013between LOTOS and Markov chains","volume":"30","author":"Hermanns","year":"1998","journal-title":"Computer Networks and ISDN (CNIS)"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB20","doi-asserted-by":"crossref","unstructured":"H. Hermanns, Interactive Markov chains, Lecture Notes in Computer Science, vol. 2428, Springer, 2002","DOI":"10.1007\/3-540-45804-2"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB21","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0304-3975(97)00127-8","article-title":"A tutorial on EMPA: a theory of concurrent processes with nondeterminism, priorities, probabilities and time","volume":"202","author":"Bernardo","year":"1998","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB22","doi-asserted-by":"crossref","unstructured":"M. Bravetti, M. Bernardo, Compositional asymmetric cooperations for process algebras with probabilities, priorities, and time, in: Proceedings of the 1st International Workshop on Models for Time Critical Systems (MTCS 2000), Electronic Notes in Theoretical Computer Science 39 (3), State College (PA), 2000","DOI":"10.1016\/S1571-0661(05)01220-X"},{"issue":"1","key":"10.1016\/S1567-8326(02)00066-8_BIB23","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1007\/BF00268075","article-title":"Specification-oriented semantics for communicating processes","volume":"23","author":"Olderog","year":"1986","journal-title":"Acta Informatica"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB24","unstructured":"G. Plotkin, A structural approach to operational semantics, technical report, Computer Science Department FN-19, DAIMI, Aarhus University, September 1981"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB25","doi-asserted-by":"crossref","unstructured":"A. Bianco, L. de Alfaro, Model checking of probabilistic and nondeterministic systems, in: P. Thiagarajan (Ed.), Proceedings of Foundations of Software Technology and Theoretical Computer Science, vol. 1026 of Lecture Notes in Computer Science, Springer-Verlag, 1995, pp. 499\u2013513","DOI":"10.1007\/3-540-60692-0_70"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB26","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1007\/s004460050046","article-title":"Model checking for a probabilistic branching time logic with fairness","volume":"11","author":"Baier","year":"1998","journal-title":"Distributed Computing"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB27","doi-asserted-by":"crossref","first-page":"356","DOI":"10.1145\/2166.357214","article-title":"Termination of probabilistic concurrent programs","volume":"5","author":"Hart","year":"1983","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB28","unstructured":"L. de Alfaro, From fairness to chance, in: C. Baier, M. Huth, M. Kwiatkowska, M. Ryan (Eds.), Proceedings of First International Workshop on Probabilistic Methods in Verification (PROBMIV\u201998), vol. 22 of Electronic Notes in Theoretical Computer Science, 1998"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB29","doi-asserted-by":"crossref","unstructured":"E. Clarke, E. Emerson, A. Sistla, Automatic verification of finite-state concurrent systems using temporal logics, in: 10th ACM Symposium on Principles of Programming Languages, 1983, pp. 24\u201326, the full version is available in ACM Transactions on Programming Languages and Systems 1(2), 1986","DOI":"10.1145\/5397.5399"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB30","unstructured":"C. Baier, On algorithmic verification methods for probabilistic systems, Habilitation thesis, Fakult\u00e4t f\u00fcr Mathematik & Informatik, Universit\u00e4t Mannheim, 1999"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB31","doi-asserted-by":"crossref","unstructured":"L. de Alfaro, Stochastic transition systems, in: D. Sangiorgi, R. de Simone (Eds.), Proceedings of CONCUR\u201998, Lecture Notes in Computer Science, Springer-Verlag, 1998, pp. 423\u2013438","DOI":"10.1007\/BFb0055639"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB32","doi-asserted-by":"crossref","unstructured":"L. de Alfaro, M. Kwiatkowska, G. Norman, D. Parker, R. Segala, Symbolic model checking for probabilistic processes using MTBDDs and the Kronecker representation, in: S. Graf, M. Schwartzbach (Eds.), TACAS\u20192000, LNCS 1785, Berlin, 2000, pp. 395\u2013410","DOI":"10.1007\/3-540-46419-0_27"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB33","doi-asserted-by":"crossref","unstructured":"G. Ciardo, R. Zijal, Well-defined stochastic Petri nets, in: MASCOTS, 1996, pp. 278\u2013284","DOI":"10.1109\/MASCOT.1996.501031"},{"issue":"9","key":"10.1016\/S1567-8326(02)00066-8_BIB34","doi-asserted-by":"crossref","first-page":"603","DOI":"10.1109\/32.541432","article-title":"Algorithms for the generation of state-level representations of stochastic activity networks with general reward structures","volume":"22","author":"Qureshi","year":"1996","journal-title":"IEEE Transactions on Software Engineering"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB35","doi-asserted-by":"crossref","unstructured":"D. Deavours, W. Sanders, An efficient well-specified check, in: P. Bucholz, M. Silva (Eds.), Proceedings of the 8th International Workshop on Petri Nets and Performance Models (PNPM \u201999), Zaragoza, Spain, 1999, pp. 124\u2013133","DOI":"10.1109\/PNPM.1999.796559"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB36","doi-asserted-by":"crossref","unstructured":"H. Hermanns, M. Siegle, Bisimulation algorithms for stochastic process algebras and their BDD-based implementation, in: J.-P. Katoen (Ed.), ARTS\u201999, 5th International AMAST Workshop on Real-Time and Probabilistic Systems, vol. 1601 of Lecture Notes in Computer Science, Springer, 1999, pp. 144\u2013264","DOI":"10.1007\/3-540-48778-6_15"},{"issue":"2","key":"10.1016\/S1567-8326(02)00066-8_BIB37","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1145\/190.191","article-title":"A class of generalized stochastic Petri nets for the performance evaluation of multiprocessor systems","volume":"2","author":"Ajmone Marsan","year":"1984","journal-title":"ACM Transactions on Computer Systems"},{"year":"1995","series-title":"Modelling with generalized stochastic Petri nets","author":"Ajmone Marsan","key":"10.1016\/S1567-8326(02)00066-8_BIB38"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB39","doi-asserted-by":"crossref","unstructured":"A. Shiryaev, Probability, 2nd edition, vol. 95 of Graduate Texts in Mathematics, Springer, 1996","DOI":"10.1007\/978-1-4757-2539-1"},{"year":"1994","series-title":"Introduction to the Numerical Solution of Markov Chains","author":"Stewart","key":"10.1016\/S1567-8326(02)00066-8_BIB40"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB41","first-page":"87","article-title":"Markoff chains as an aid in the study of Markoff processes","volume":"36","author":"Jensen","year":"1953","journal-title":"Skand. Aktuarietiedskr."},{"key":"10.1016\/S1567-8326(02)00066-8_BIB42","doi-asserted-by":"crossref","first-page":"396","DOI":"10.1016\/0377-2217(77)90049-2","article-title":"Transient solutions in Markovian queues","volume":"1","author":"Grassmann","year":"1977","journal-title":"European Journal of Operational Research"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB43","doi-asserted-by":"crossref","unstructured":"E. Clarke, K. McMillan, X. Zhao, M. Fujita, J. Yang, Spectral transforms for large boolean functions with applications to technology mapping, in: 30th Design Automation Conference, ACM\/IEEE, 1993, pp. 54\u201360","DOI":"10.1145\/157485.164569"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB44","doi-asserted-by":"crossref","unstructured":"K. Brace, R. Rudell, R. Bryant, Efficient implementation of a BDD package, in: 27th ACM\/IEEE Design Automation Conference, 1990, pp. 40\u201345","DOI":"10.1145\/123186.123222"},{"issue":"3","key":"10.1016\/S1567-8326(02)00066-8_BIB45","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/BF02242704","article-title":"Generating BDDs for symbolic model checking in CCS","volume":"6","author":"Enders","year":"1993","journal-title":"Distributed Computing"},{"year":"1993","series-title":"Symbolic Model Checking","author":"McMillan","key":"10.1016\/S1567-8326(02)00066-8_BIB46"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB47","unstructured":"M. Kwiatkowska, G. Norman, D. Parker, R. Segala, Symbolic model checking of concurrent probabilistic systems using MTBDDs and Simplex, Tech. rep., School of Computer Science, University of Birmingham, 1999"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB48","doi-asserted-by":"crossref","unstructured":"M. Kwiatkowska, G. Norman, D. Parker, PRISM: Probabilistic symbolic model checker, in: T. Field, P. Harrison, J. Bradley, U. Harder (Eds.), Proceedings of 12th International Conference on Modelling Techniques and Tools for Computer Performance Evaluation (TOOLS\u201902), vol. 2324 of LNCS, Springer, 2002, pp. 200\u2013204","DOI":"10.1007\/3-540-46029-2_13"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB49","unstructured":"F. Somenzi, Cudd: Colorado university decision diagram package, release 2.3.0, user\u2019s Manual and Programmer\u2019s Manual, http:\/\/vlsi.colorado.edu\/~fabio, September 1998"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB50","doi-asserted-by":"crossref","unstructured":"R. Alur, T. Henzinger, Reactive modules, in: Proceedings of 11th Annual IEEE Symposium on Logic in Computer Science (LICS\u201996), IEEE Computer Society Press, 1006, pp. 207\u2013218","DOI":"10.1109\/LICS.1996.561320"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB51","unstructured":"E. Frank, Codierung und numerische analyse von transitionssystemen unter verwendung von MTBDDs, student\u2019s thesis, Universit\u00e4t Erlangen-N\u00fcrnberg, IMMD 7, 1999 (in German)"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB52","unstructured":"E. Frank, Erweiterung eines MTBDD-basierten Werkzeugs f\u00fcr die Analyse stochastischer Transitionssysteme, Tech. Report Informatik 7, no. 01\/00, Universit\u00e4t Erlangen-N\u00fcrnberg, January 2000 (in German)"},{"issue":"1\u20134","key":"10.1016\/S1567-8326(02)00066-8_BIB53","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1016\/S0166-5316(99)00056-5","article-title":"Compositional performance modelling with the TIPPtool","volume":"39","author":"Hermanns","year":"2000","journal-title":"Performance Evaluation"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB54","doi-asserted-by":"crossref","unstructured":"C. Kelley, Iterative Methods for linear and nonlinear systems, Series on Frontiers in Applied Mathematics, SIAM, 1995","DOI":"10.1137\/1.9781611970944"},{"issue":"9","key":"10.1016\/S1567-8326(02)00066-8_BIB55","doi-asserted-by":"crossref","first-page":"1649","DOI":"10.1109\/49.62852","article-title":"Stochastic Petri net models of polling systems","volume":"8","author":"Ibe","year":"1990","journal-title":"IEEE Journal on Selected Areas in Communications"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB56","unstructured":"H. Hermanns, J. Meyer-Kayser, M. Siegle, Multi terminal binary decision diagrams to represent and analyse continuous time Markov chains, in: B. Plateau, W. Stewart, M. Silva (Eds.), 3rd International Workshop on the Numerical Solution of Markov Chains, Prensas Universitarias de Zaragoza, 1999, pp. 188\u2013207"},{"issue":"3","key":"10.1016\/S1567-8326(02)00066-8_BIB57","doi-asserted-by":"crossref","first-page":"441","DOI":"10.1016\/0196-6774(90)90021-6","article-title":"Fast randomized consensus using shared memory","volume":"11","author":"Aspnes","year":"1990","journal-title":"Journal of Algorithms"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB58","doi-asserted-by":"crossref","unstructured":"M. Vardi, Automatic verification of probabilistic concurrent finite state programs, in: Proceedings of IEEE Symposium on Foundations of Computer Science (FOCS\u201985), 1985, pp. 327\u2013338","DOI":"10.1109\/SFCS.1985.12"},{"issue":"9","key":"10.1016\/S1567-8326(02)00066-8_BIB59","doi-asserted-by":"crossref","first-page":"993","DOI":"10.1109\/12.537122","article-title":"Improving the variable ordering of OBDDs is NPcomplete","volume":"45","author":"Bollig","year":"1996","journal-title":"IEEE Transactions on Computers"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB60","doi-asserted-by":"crossref","unstructured":"S. Tani, K. Hamaguchi, S. Yajima, The complexity of optimal variable ordering of a shared binary decision diagram, in: Proceedings of 45th ISAAC, vol. 762 of Lecture Notes in Computer Science, Springer, 1993, pp. 389\u2013398","DOI":"10.1007\/3-540-57568-5_270"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB61","unstructured":"R. Rudell, Dynamic variable ordering for ordered binary decision diagrams, in: Proceedings of IEEE ICCAD\u201993, 1993, pp. 42\u201347"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB62","unstructured":"M. Fujita, Y. Matsunaga, T. Kakuda, On variable ordering of binary decision diagrams for the application of multi-level logic synthesis, in: Proceedings of European Design Automation Conference (EDAC 91), IEEE Computer Society Press, 1991, pp. 50\u201354"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB63","doi-asserted-by":"crossref","unstructured":"J. Bern, C. Meinel, A. Slobodova, Global rebuilding of OBDD\u2019s\u2013\u2013tunneling memory requirement maxima, in: P. Wolper (Ed.), Proceedings of International Conference On Computer Aided Verification, vol. 939 of Lecture Notes in Computer Science, Springer-Verlag, 1995, pp. 4\u201315","DOI":"10.1007\/3-540-60045-0_36"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB64","unstructured":"D. Parker, Implementation of symbolic model checking for probabilistic systems, Ph.D. thesis, School of Computer Science, University of Birmingham, submitted"},{"year":"1976","series-title":"Finite Markov Chains","author":"Kemeny","key":"10.1016\/S1567-8326(02)00066-8_BIB65"},{"issue":"1","key":"10.1016\/S1567-8326(02)00066-8_BIB66","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(91)90030-6","article-title":"Bisimulation through probabilistic testing","volume":"94","author":"Larsen","year":"1991","journal-title":"Information and Computation"},{"issue":"1\/2","key":"10.1016\/S1567-8326(02)00066-8_BIB67","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1007\/BF00625969","article-title":"Exploiting symmetry in temporal logic model checking","volume":"9","author":"Clarke","year":"1996","journal-title":"Formal Methods in System Design"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB68","doi-asserted-by":"crossref","unstructured":"J. Katoen, M. Kwiatkowska, G. Norman, D. Parker, Faster and symbolic CTMC model checking, in: L. de Alfaro, S. Gilmore (Eds.), Proceedings of Process Algebra and Probabilistic Methods (PAPM-PROBMIV 2001), vol. 2165 of Lecture Notes in Computer Science, Springer, 2001, pp. 23\u201338","DOI":"10.1007\/3-540-44804-7_2"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB69","doi-asserted-by":"crossref","unstructured":"M. Kwiatkowska, G. Norman, D. Parker, Probabilistic symbolic model checking with PRISM: a hybrid approach, in: J.-P. Katoen, P. Stevens (Eds.), Proceedings of 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201902), vol. 2280 of LNCS, Springer, 2002, pp. 52\u201366","DOI":"10.1007\/3-540-46002-0_5"},{"key":"10.1016\/S1567-8326(02)00066-8_BIB70","doi-asserted-by":"crossref","unstructured":"P. D\u2019Argenio, B. Jeannet, H. Jensen, K. Larsen, Reachability Analysis of Probabilistic Systems by Successive Refinements, in: L. de Alfaro, S. Gilmore (Eds.), Process Algebra and Probabilistic Methods. Joint International Workshop PAPMPROBMIV 2001, Springer, LNCS 2165, 2001, pp. 39\u201356","DOI":"10.1007\/3-540-44804-7_3"}],"container-title":["The Journal of Logic and Algebraic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1567832602000668?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1567832602000668?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T18:33:39Z","timestamp":1761590019000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1567832602000668"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,5]]},"references-count":70,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2003,5]]}},"alternative-id":["S1567832602000668"],"URL":"https:\/\/doi.org\/10.1016\/s1567-8326(02)00066-8","relation":{},"ISSN":["1567-8326"],"issn-type":[{"type":"print","value":"1567-8326"}],"subject":[],"published":{"date-parts":[[2003,5]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"On the use of MTBDDs for performability analysis and verification of stochastic systems","name":"articletitle","label":"Article Title"},{"value":"The Journal of Logic and Algebraic Programming","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S1567-8326(02)00066-8","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2002 Elsevier Science Inc. All rights reserved.","name":"copyright","label":"Copyright"}]}}