{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,13]],"date-time":"2026-03-13T13:15:23Z","timestamp":1773407723208,"version":"3.50.1"},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2002,7,1]],"date-time":"2002-07-01T00:00:00Z","timestamp":1025481600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2002,7,1]],"date-time":"2002-07-01T00:00:00Z","timestamp":1025481600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Discrete Event Dynamic Systems"],"published-print":{"date-parts":[[2002,7]]},"DOI":"10.1023\/a:1015669415634","type":"journal-article","created":{"date-parts":[[2002,12,28]],"date-time":"2002-12-28T19:22:22Z","timestamp":1041103342000},"page":"265-286","source":"Crossref","is-referenced-by-count":16,"title":["Efficient Computation and Representation of Large Reachability Sets for Composed Automata"],"prefix":"10.1007","volume":"12","author":[{"given":"Peter","family":"Buchholz","sequence":"first","affiliation":[]},{"given":"Peter","family":"Kemper","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"406978_CR1","doi-asserted-by":"crossref","unstructured":"Bause, F., Buchholz, P., and Kemper, P. 1998. A toolbox for functional and quantitative analysis of DEDS. In R. Pujanger, N. N. Savino, and B. Serra, (eds), Quantitative Evaluation of Computing and Communication Systems 356-359, Springer LNCS 1469.","DOI":"10.1007\/3-540-68061-6_32"},{"key":"406978_CR2","doi-asserted-by":"crossref","unstructured":"Behrmann, G., Larsen, K., Andersen, H. R., Hulgaard, H., and Lind-Nielsen, J. 1999. Verification of hierarchical state\/event systems using reusability and compositionality. In W. R. Cleaveland (ed.) Tools and Algorithms for the Construction and Analysis of Systems 163-177, Springer LNCS 1579.","DOI":"10.1007\/3-540-49059-0_12"},{"key":"406978_CR3","doi-asserted-by":"crossref","first-page":"813","DOI":"10.1007\/s002360050144","volume":"35","author":"E. Best","year":"1998","unstructured":"Best, E., Fraczak, W., Hopkins, R. P., Klaudel, H., and Pelz, E. 1998. M-nets: An algebra of high-level Petri nets, with an application to the semantics of concurrent programming languages. Acta Informatica 35: 813-857.","journal-title":"Acta Informatica"},{"issue":"8","key":"406978_CR4","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R. E. Bryant","year":"1986","unstructured":"Bryant, R. E. 1986. Graph based algorithms for Boolean function manipulation. IEEE Transactions on Computer 35(8): 677-691.","journal-title":"IEEE Transactions on Computer"},{"issue":"1\/2","key":"406978_CR5","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1016\/S0304-3975(98)00169-8","volume":"215","author":"P. Buchholz","year":"1999","unstructured":"Buchholz, P. 1999a. Exact performance equivalence\u2014an equivalence relation for stochastic automata. Theoretical Computer Science 215(1\/2): 263-287.","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"406978_CR6","doi-asserted-by":"crossref","first-page":"166","DOI":"10.1109\/32.761443","volume":"25","author":"P. Buchholz","year":"1999","unstructured":"Buchholz, P. 1999b. Hierarchical structuring of superposed GSPNs. IEEE Transactions on Software Engineering 25(2): 166-181.","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"4","key":"406978_CR7","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1016\/S0168-9274(99)00005-7","volume":"31","author":"P. Buchholz","year":"1999","unstructured":"Buchholz, P. 1999c. Structured analysis approaches for large Markov chains. Applied Numerical Mathematics 31(4): 375-404.","journal-title":"Applied Numerical Mathematics"},{"key":"406978_CR8","doi-asserted-by":"crossref","unstructured":"Buchholz, P., and Kemper, P. 1999. Modular state level analysis of distributed systems\u2014techniques and tool support. In R. Cleaveland (ed.), Tools and Algorithms for the Construction and Analysis of Systems 420-434, Springer LNCS 1579.","DOI":"10.1007\/3-540-49059-0_29"},{"key":"406978_CR9","doi-asserted-by":"crossref","unstructured":"Buchholz, P., and Kemper, P. 2000. Efficient computation and representation of large reachability sets for composed automata. In R. Boel and G. Stremersch (eds), Discrete Event Systems Analysis and Control 49-56, Kluwer Academic.","DOI":"10.1007\/978-1-4615-4493-7_4"},{"issue":"2","key":"406978_CR10","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., and Hwang, L. J. 1992. Symbolic model checking: 1020 states and beyond. Information and Computation 98(2): 142-170.","journal-title":"Information and Computation"},{"key":"406978_CR11","doi-asserted-by":"crossref","unstructured":"Ciardo, G., and Miner, A. S. 1997. Storage alternatives for large structured state spaces. In R. Marie and B. Plateau (eds), Proc. 9th Int. Conf. on Modelling Techniques and Tools for Computer Performance Evaluation 44-57, Springer LNCS 1245.","DOI":"10.1007\/BFb0022196"},{"issue":"2","key":"406978_CR12","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. M. Clarke","year":"1986","unstructured":"Clarke, E. M., Emerson, E. A., and Sistla, A. P. 1986. Automatic verification of finite state concurrent systems using temporal logic specifications. ACM Transactions and Programming Languages and Systems 8(2): 244-263.","journal-title":"ACM Transactions and Programming Languages and Systems"},{"issue":"4","key":"406978_CR13","doi-asserted-by":"crossref","first-page":"626","DOI":"10.1145\/242223.242257","volume":"28","author":"E. M. Clarke","year":"1996","unstructured":"Clarke, E. M., and Wing, J. M. et al. 1996. Formal methods: State of the art and future directions. ACM Computing Surveys 28(4): 626-643.","journal-title":"ACM Computing Surveys"},{"issue":"1","key":"406978_CR14","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1145\/151646.151648","volume":"15","author":"R. Cleaveland","year":"1993","unstructured":"Cleaveland, R., Parrow, J., and Steffen, B. 1993. The concurrency workbench: a semantics based tool for the verification of concurrent systems. ACM Transactions on Programming Languages and Systems 15(1): 36-72.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"406978_CR15","doi-asserted-by":"crossref","first-page":"116","DOI":"10.1109\/TC.1981.6312174","volume":"30","author":"M. Davio","year":"1981","unstructured":"Davio, M. 1981. Kronecker products and shuffle algebra. IEEE Transactions on Computers 30: 116-125.","journal-title":"IEEE Transactions on Computers"},{"issue":"5","key":"406978_CR16","doi-asserted-by":"crossref","first-page":"607","DOI":"10.1007\/BF01211911","volume":"8","author":"S. Graf","year":"1996","unstructured":"Graf, S., Steffen, B., and L\u00fcttgen, G. 1996. Compositional minimization of finite state systems. Formal Aspects of Computing 8(5): 607-616.","journal-title":"Formal Aspects of Computing"},{"key":"406978_CR17","unstructured":"Heiner, M. 1997. Verification and optimization of control programs by Petri nets without state explosion. In Proc. 2nd Workshop on Manufacturing and Petri Nets 69-84, available via http:\/\/www-dssz.Informatik.TU-Cottbus.DE\/ wwwdssz\/"},{"key":"406978_CR18","doi-asserted-by":"crossref","unstructured":"Hoare, C. 1985. Communicating Sequential Processes. Prentice Hall.","DOI":"10.1007\/978-3-642-82921-5_4"},{"issue":"3","key":"406978_CR19","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1023\/A:1008696026254","volume":"13","author":"G. J. Holzmann","year":"1998","unstructured":"Holzmann, G. J. 1998. An analysis of bitstate hashing. Formal Methods in System Design 13(3): 301-314.","journal-title":"Formal Methods in System Design"},{"issue":"9","key":"406978_CR20","doi-asserted-by":"crossref","first-page":"615","DOI":"10.1109\/32.541433","volume":"22","author":"P. Kemper","year":"1996","unstructured":"Kemper, P. 1996a. Numerical analysis of superposed GSPNs. IEEE Transactions on Software Engineering 22(9): 615-628.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"406978_CR21","doi-asserted-by":"crossref","unstructured":"Kemper, P. 1996b. Reachability analysis based on structured representations. In J. Billington and W. Reisig (eds), Application and Theory of Petri Nets 1996 269-288, Springer LNCS 1091.","DOI":"10.1007\/3-540-61363-3_15"},{"key":"406978_CR22","unstructured":"Kemper, P., and L\u00fcbeck, R. 1998. Model checking based on Kronecker algebra. Forschungsbericht 669, Fachbereich Informatik, Universit\u00e4t Dortmund."},{"key":"406978_CR23","unstructured":"Lynch, N. A. 1996. Distributed Algorithms. Morgan Kaufmann."},{"key":"406978_CR24","unstructured":"Magee, J., and Kramer, J. 1999. Concurrency\u2014State models & Java programs. Wiley."},{"key":"406978_CR25","doi-asserted-by":"crossref","unstructured":"McMillan, K. L. 1993. Symbolic model checking: an approach to the state space explosion problem. Kluwer.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"406978_CR26","unstructured":"Milner, R. 1989. Communication and Concurrency. Prentice Hall."},{"key":"406978_CR27","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1145\/317786.317819","volume":"13","author":"B. Plateau","year":"1985","unstructured":"Plateau, B. 1985. On the stochastic structure of parallelism and synchronisation models for distributed algorithms. Performance Evaluation Review 13: 142-154.","journal-title":"Performance Evaluation Review"},{"key":"406978_CR28","doi-asserted-by":"crossref","unstructured":"Stern, U., and Dill, D. L. 1998. Using magnetic disk instead of main memory in the Mur\u03d5 verifier. In A. J. Hu and M. Y. Vardi (eds), CAV'98 172-183, Springer LNCS 1427.","DOI":"10.1007\/BFb0028743"},{"key":"406978_CR29","doi-asserted-by":"crossref","unstructured":"Stewart, W. J. 1994. Introduction to the Numerical Solution of Markov Chains. Princeton University Press.","DOI":"10.1515\/9780691223384"},{"key":"406978_CR30","doi-asserted-by":"crossref","unstructured":"Wegener, I. 2000. Branching Programs and Binary Decision Diagrams. Monographs on Discrete Mathematics and Applications. SIAM.","DOI":"10.1137\/1.9780898719789"}],"container-title":["Discrete Event Dynamic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1015669415634.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1015669415634\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1015669415634.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,29]],"date-time":"2025-07-29T04:16:16Z","timestamp":1753762576000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1015669415634"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,7]]},"references-count":30,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2002,7]]}},"alternative-id":["406978"],"URL":"https:\/\/doi.org\/10.1023\/a:1015669415634","relation":{},"ISSN":["0924-6703","1573-7594"],"issn-type":[{"value":"0924-6703","type":"print"},{"value":"1573-7594","type":"electronic"}],"subject":[],"published":{"date-parts":[[2002,7]]}}}