{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,11]],"date-time":"2026-01-11T02:01:19Z","timestamp":1768096879294,"version":"3.49.0"},"reference-count":44,"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)00067-x","type":"journal-article","created":{"date-parts":[[2003,5,12]],"date-time":"2003-05-12T20:23:48Z","timestamp":1052771028000},"page":"69-97","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":33,"title":["Model-checking large structured Markov chains"],"prefix":"10.1016","volume":"56","author":[{"given":"Peter","family":"Buchholz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Kemper","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carsten","family":"Tepper","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1567-8326(02)00067-X_BIB1","series-title":"Computer-Aided Verification, LNCS 1102","first-page":"269","article-title":"Verifying continuous time Markov chains","author":"Aziz","year":"1996"},{"issue":"1","key":"10.1016\/S1567-8326(02)00067-X_BIB2","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1145\/343369.343402","article-title":"Model checking continuous time Markov chains","volume":"1","author":"Aziz","year":"2000","journal-title":"ACM Trans. Comput. Logic"},{"issue":"2\/3","key":"10.1016\/S1567-8326(02)00067-X_BIB3","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1023\/A:1008699807402","article-title":"Algebraic decision diagrams and their applications","volume":"10","author":"Bahar","year":"1997","journal-title":"Formal Meth. Syst. Des."},{"key":"10.1016\/S1567-8326(02)00067-X_BIB4","series-title":"Automata, Languages, and Programming (ICALP) LNCS 1853","first-page":"780","article-title":"On the logical characterisation of performability properties","author":"Baier","year":"2000"},{"key":"10.1016\/S1567-8326(02)00067-X_BIB5","series-title":"Computer-Aided Verification, LNCS 1855","first-page":"358","article-title":"Model checking continuous-time Markov chains by transient analysis","author":"Baier","year":"2000"},{"key":"10.1016\/S1567-8326(02)00067-X_BIB6","series-title":"Concurrency Theory, LNCS 1664","first-page":"146","article-title":"Approximate symbolic model checking of continuous-time Markov chains","author":"Baier","year":"1999"},{"issue":"8","key":"10.1016\/S1567-8326(02)00067-X_BIB7","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","article-title":"Graph-based algorithms for Boolean function manipulation","volume":"35","author":"Bryant","year":"1986","journal-title":"IEEE Trans. Comput."},{"key":"10.1016\/S1567-8326(02)00067-X_BIB8","series-title":"Die Strukturierte Analyse Markovscher Modelle, IFB 282","author":"Buchholz","year":"1991"},{"key":"10.1016\/S1567-8326(02)00067-X_BIB9","unstructured":"P. Buchholz, Markovian process algebra: composition and equivalence, in: U. Herzog, M. Rettelbach (Eds.), Proc. of the 2nd Work. on Process Algebras and Perf. Modelling, vol. 27, Arbeitsberichte des IMMD, University of Erlangen, 1994, pp. 11\u201330"},{"key":"10.1016\/S1567-8326(02)00067-X_BIB10","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1016\/0166-5316(93)E0040-C","article-title":"Hierarchical Markovian models: symmetries and reduction","volume":"22","author":"Buchholz","year":"1995","journal-title":"Perform. Eval."},{"issue":"2","key":"10.1016\/S1567-8326(02)00067-X_BIB11","first-page":"93","article-title":"Efficient computation of equivalent and reduced representations for stochastic automata","volume":"15","author":"Buchholz","year":"2000","journal-title":"Int. J. Comput. Syst. Sci. Eng."},{"issue":"2","key":"10.1016\/S1567-8326(02)00067-X_BIB12","doi-asserted-by":"crossref","first-page":"166","DOI":"10.1109\/32.761443","article-title":"Hierarchical structuring of superposed GSPNs","volume":"25","author":"Buchholz","year":"1999","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"4","key":"10.1016\/S1567-8326(02)00067-X_BIB13","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1016\/S0168-9274(99)00005-7","article-title":"Structured analysis approaches for large Markov chains","volume":"31","author":"Buchholz","year":"1999","journal-title":"Appl. Numer. Math."},{"issue":"3","key":"10.1016\/S1567-8326(02)00067-X_BIB14","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1287\/ijoc.12.3.203.12634","article-title":"Complexity of Kronecker operations and sparse matrices with applications to the solution of Markov models","volume":"12","author":"Buchholz","year":"2000","journal-title":"INFORMS J. Comput."},{"key":"10.1016\/S1567-8326(02)00067-X_BIB15","unstructured":"P. Buchholz, M. Fischer, P. Kemper, C. Tepper, New features in the APNN toolbox, in: P. Kemper (Ed.), Tools of Aachen 2001 Int. Multiconference on Measurement, Modeling and Evaluation of Computer-Communication Systems, Universit\u00e4t Dortmund, Fachbereich Informatik, Forschungsbericht Nr. 760, 2001, pp. 62\u201368"},{"issue":"3","key":"10.1016\/S1567-8326(02)00067-X_BIB16","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1023\/A:1015669415634","article-title":"Efficient computation and representation of large reachability sets for composed automata","volume":"12","author":"Buchholz","year":"2002","journal-title":"Discrete Event Dyn. Syst.\u2013\u2013Theory Applic."},{"issue":"2","key":"10.1016\/S1567-8326(02)00067-X_BIB17","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1109\/32.761442","article-title":"Structured solution of asynchronously communicating stochastic modules","volume":"25","author":"Campos","year":"1999","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"2","key":"10.1016\/S1567-8326(02)00067-X_BIB18","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1109\/32.214828","article-title":"Generalized stochastic Petri nets: a definition at the net level and its implications","volume":"19","author":"Chiola","year":"1993","journal-title":"IEEE Trans. Softw. Eng."},{"key":"10.1016\/S1567-8326(02)00067-X_BIB19","series-title":"Lectures on Formal Methods and Performance Analysis, LNCS 2090","first-page":"344","article-title":"Distributed and structured analysis approaches to study large and complex systems","author":"Ciardo","year":"2001"},{"key":"10.1016\/S1567-8326(02)00067-X_BIB20","series-title":"Proc. 8th Int. Workshop on Petri Nets and Perf. Models","first-page":"22","article-title":"A data structure for the efficient Kronecker solution of GSPNs","author":"Ciardo","year":"1999"},{"key":"10.1016\/S1567-8326(02)00067-X_BIB21","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","article-title":"Automatic verification of finite-state concurrent systems using temporal logic specifications","volume":"8","author":"Clarke","year":"1986","journal-title":"ACM Trans. Program. Languages Syst."},{"issue":"2\/3","key":"10.1016\/S1567-8326(02)00067-X_BIB22","first-page":"149","article-title":"Multi-terminal binary decision diagrams: an efficient data structure for matrix representation","volume":"10","author":"Clarke","year":"1997","journal-title":"Formal Meth. Syst. Des."},{"key":"10.1016\/S1567-8326(02)00067-X_BIB23","series-title":"Model Checking","author":"Clarke","year":"1999"},{"key":"10.1016\/S1567-8326(02)00067-X_BIB24","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1016\/0166-5316(93)90025-P","article-title":"Superposed stochastic automata: a class of stochastic Petri nets amenable to parallel solution","volume":"18","author":"Donatelli","year":"1994","journal-title":"Perform. Eval."},{"issue":"1\u20134","key":"10.1016\/S1567-8326(02)00067-X_BIB25","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/S0166-5316(00)00060-2","article-title":"Integrating synchronization with priority into a Kronecker representation","volume":"44","author":"Donatelli","year":"2001","journal-title":"Perform. Eval."},{"key":"10.1016\/S1567-8326(02)00067-X_BIB26","doi-asserted-by":"crossref","first-page":"440","DOI":"10.1145\/42404.42409","article-title":"Computing Poisson probabilities","volume":"31","author":"Fox","year":"1988","journal-title":"Commun. ACM"},{"issue":"2","key":"10.1016\/S1567-8326(02)00067-X_BIB27","doi-asserted-by":"crossref","first-page":"926","DOI":"10.1287\/opre.32.2.343","article-title":"The randomization technique as a modeling tool and solution procedure for transient Markov processes","volume":"32","author":"Gross","year":"1984","journal-title":"Oper. Res."},{"key":"10.1016\/S1567-8326(02)00067-X_BIB28","doi-asserted-by":"crossref","first-page":"512","DOI":"10.1007\/BF01211866","article-title":"A logic for reasoning about time and reliability","volume":"6","author":"Hansson","year":"1994","journal-title":"Formal Aspects Comput."},{"key":"10.1016\/S1567-8326(02)00067-X_BIB29","series-title":"IEEE Symp. on Reliable Distr. Sys.","first-page":"228","article-title":"The use of model checking techniques for quantitative dependability evaluation","author":"Haverkort","year":"2000"},{"key":"10.1016\/S1567-8326(02)00067-X_BIB30","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1007\/BF01439850","article-title":"Specification techniques for Markov reward models","volume":"3","author":"Haverkort","year":"1993","journal-title":"Discrete Event Syst.: Theory Applic."},{"key":"10.1016\/S1567-8326(02)00067-X_BIB31","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":"Theor. Comput. Sci."},{"key":"10.1016\/S1567-8326(02)00067-X_BIB32","series-title":"Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1785","first-page":"347","article-title":"A Markov chain model checker","author":"Hermanns","year":"2000"},{"issue":"7","key":"10.1016\/S1567-8326(02)00067-X_BIB33","doi-asserted-by":"crossref","first-page":"530","DOI":"10.1093\/comjnl\/38.7.530","article-title":"Formal characterisation of immediate actions in SPA with non-deterministic branching","volume":"38","author":"Hermanns","year":"1995","journal-title":"The Comput. J."},{"key":"10.1016\/S1567-8326(02)00067-X_BIB34","series-title":"Formal Methods for Real-Time and Probabilistic Systems, LNCS 1601","first-page":"244","article-title":"Bisimulation algorithms for stochastic process algebras and their BDD-based implementation","author":"Hermanns","year":"1999"},{"key":"10.1016\/S1567-8326(02)00067-X_BIB35","series-title":"A Compositional Approach to Performance Modelling","author":"Hillston","year":"1996"},{"key":"10.1016\/S1567-8326(02)00067-X_BIB36","series-title":"Process Algebra and Probabilistic Methods, LNCS 2165","first-page":"23","article-title":"Faster and symbolic CTMC model checking","author":"Katoen","year":"2001"},{"key":"10.1016\/S1567-8326(02)00067-X_BIB37","series-title":"Application and Theory of Petri Nets 1996, LNCS 1091","first-page":"269","article-title":"Reachability analysis based on structured representations","author":"Kemper","year":"1996"},{"issue":"9","key":"10.1016\/S1567-8326(02)00067-X_BIB38","doi-asserted-by":"crossref","first-page":"615","DOI":"10.1109\/32.541433","article-title":"Numerical analysis of superposed GSPNs","volume":"22","author":"Kemper","year":"1996","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"2","key":"10.1016\/S1567-8326(02)00067-X_BIB39","doi-asserted-by":"crossref","first-page":"182","DOI":"10.1109\/32.761444","article-title":"Transient analysis of superposed GSPNs","volume":"25","author":"Kemper","year":"1999","journal-title":"IEEE Trans. Softw. Eng."},{"key":"10.1016\/S1567-8326(02)00067-X_BIB40","unstructured":"P. Kemper, R. L\u00fcbeck, Model checking based on Kronecker algebra, Technical Report 669, Fachbereich Informatik, Universit\u00e4t Dortmund (Germany), 1998"},{"key":"10.1016\/S1567-8326(02)00067-X_BIB41","series-title":"Tools and Algorithms for the Construction and Analysis of Systems, LNCS 2280","first-page":"52","article-title":"Probabilistic symbolic model checking with PRISM: a hybrid approach","author":"Kwiatkowska","year":"2002"},{"key":"10.1016\/S1567-8326(02)00067-X_BIB42","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1145\/317786.317819","article-title":"On the stochastic structure of parallelism and synchronisation models for distributed algorithms","volume":"13","author":"Plateau","year":"1985","journal-title":"Perform. Eval. Rev."},{"key":"10.1016\/S1567-8326(02)00067-X_BIB43","series-title":"Introduction to the Numerical Solution of Markov Chains","author":"Stewart","year":"1994"},{"key":"10.1016\/S1567-8326(02)00067-X_BIB44","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1137\/0201010","article-title":"Depth-first search and linear graph algorithms","volume":"1","author":"Tarjan","year":"1972","journal-title":"SIAM. J. Comput."}],"container-title":["The Journal of Logic and Algebraic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S156783260200067X?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S156783260200067X?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:48Z","timestamp":1761590028000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S156783260200067X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,5]]},"references-count":44,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2003,5]]}},"alternative-id":["S156783260200067X"],"URL":"https:\/\/doi.org\/10.1016\/s1567-8326(02)00067-x","relation":{},"ISSN":["1567-8326"],"issn-type":[{"value":"1567-8326","type":"print"}],"subject":[],"published":{"date-parts":[[2003,5]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Model-checking large structured Markov chains","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)00067-X","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"}]}}