{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T19:16:52Z","timestamp":1770751012465,"version":"3.50.0"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642386961","type":"print"},{"value":"9783642386978","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38697-8_21","type":"book-chapter","created":{"date-parts":[[2013,6,18]],"date-time":"2013-06-18T21:48:46Z","timestamp":1371592126000},"page":"389-399","source":"Crossref","is-referenced-by-count":44,"title":["MARCIE \u2013 Model Checking and Reachability Analysis Done Efficiently"],"prefix":"10.1007","author":[{"given":"Monika","family":"Heiner","sequence":"first","affiliation":[]},{"given":"Christian","family":"Rohr","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Schwarick","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"21_CR1","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1145\/343369.343402","volume":"1","author":"A. Aziz","year":"2000","unstructured":"Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Model checking continuous-time Markov chains. ACM Trans. on Computational Logic\u00a01(1), 162\u2013170 (2000)","journal-title":"ACM Trans. on Computational Logic"},{"key":"21_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/3-540-48320-9_12","volume-title":"CONCUR\u201999. Concurrency Theory","author":"C. Baier","year":"1999","unstructured":"Baier, C., Katoen, J.-P., Hermanns, H.: Approximate Symbolic Model Checking of Continuous-Time Markov Chains (Extended Abstract). In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol.\u00a01664, pp. 146\u2013161. Springer, Heidelberg (1999)"},{"issue":"1","key":"21_CR3","doi-asserted-by":"publisher","first-page":"578","DOI":"10.1016\/j.peva.2005.06.001","volume":"63","author":"G. Ciardo","year":"2006","unstructured":"Ciardo, G., Jones, R.L., Miner, A.S., Siminiceanu, R.: Logical and stochastic modeling with SMART. Perform. Eval.\u00a063(1), 578\u2013608 (2006)","journal-title":"Perform. Eval."},{"issue":"2","key":"21_CR4","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite state concurrent systems using temporal logic specifications. ACM TOPLAS\u00a08(2), 244\u2013263 (1986)","journal-title":"ACM TOPLAS"},{"key":"21_CR5","first-page":"39","volume-title":"MAM 2006","author":"L. Cloth","year":"2006","unstructured":"Cloth, L., Haverkort, B.R.: Five performability algorithms. A comparison. In: MAM 2006, pp. 39\u201354. Boson Books, Raleigh (2006)"},{"key":"21_CR6","doi-asserted-by":"crossref","unstructured":"Courtney, T., Gaonkar, S., Keefe, K., Rozier, E., Sanders, W.H.: M\u00f6bius 2.3: An extensible tool for dependability, security, and performance evaluation of large and complex system models. In: DSN, pp. 353\u2013358 (2009)","DOI":"10.1109\/DSN.2009.5270318"},{"key":"21_CR7","doi-asserted-by":"crossref","unstructured":"Didier, F., Henzinger, T.A., Mateescu, M., Wolf, V.: Fast Adaptive Uniformization for the Chemical Master Equation. In: HIBI, pp. 118\u2013127. IEEE Comp. Soc. (2009)","DOI":"10.1109\/HiBi.2009.23"},{"key":"21_CR8","doi-asserted-by":"crossref","unstructured":"Didier, F., Henzinger, T.A., Mateescu, M., Wolf, V.: Sabre: A tool for stochastic analysis of biochemical reaction networks. In: Proc. QEST, pp. 217\u2013218. IEEE Computer Society (2010)","DOI":"10.1109\/QEST.2010.33"},{"key":"21_CR9","unstructured":"Donaldson, R., Gilbert, D.: A Monte Carlo model checker for probabilistic LTL with numerical constraints. Tech. rep., University of Glasgow, Dep. of CS (2008)"},{"key":"21_CR10","unstructured":"Franzke, A.: Charlie 2.0 - a multi-threaded Petri net analyzer. Diploma Thesis (in German), BTU Cottbus, Dep. of CS (2009)"},{"key":"21_CR11","doi-asserted-by":"publisher","first-page":"1876","DOI":"10.1021\/jp993732q","volume":"104","author":"M.A. Gibson","year":"2000","unstructured":"Gibson, M.A., Bruck, J.: Efficient exact stochastic simulation of chemical systems with many species and many channels. J. Phys. Chem. A\u00a0104, 1876\u20131889 (2000)","journal-title":"J. Phys. Chem. A"},{"issue":"25","key":"21_CR12","doi-asserted-by":"publisher","first-page":"2340","DOI":"10.1021\/j100540a008","volume":"81","author":"D. Gillespie","year":"1977","unstructured":"Gillespie, D.: Exact stochastic simulation of coupled chemical reactions. J. Phys. Chem.\u00a081(25), 2340\u20132361 (1977)","journal-title":"J. Phys. Chem."},{"key":"21_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/978-3-642-31131-4_22","volume-title":"Application and Theory of Petri Nets","author":"M. Heiner","year":"2012","unstructured":"Heiner, M., Herajy, M., Liu, F., Rohr, C., Schwarick, M.: Snoopy \u2013 a unifying Petri net tool. In: Haddad, S., Pomello, L. (eds.) PETRI NETS 2012. LNCS, vol.\u00a07347, pp. 398\u2013407. Springer, Heidelberg (2012)"},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"Heiner, M., Rohr, C., Schwarick, M., Streif, S.: A comparative study of stochastic analysis techniques. In: Proc. CMSB 2010, pp. 96\u2013106. ACM (2010)","DOI":"10.1145\/1839764.1839776"},{"key":"21_CR15","first-page":"9","volume":"76","author":"L. Hillah","year":"2009","unstructured":"Hillah, L., Kindler, E., Kordon, F., Petrucci, L., Tr\u00e8ves, N.: A primer on the Petri Net Markup Language and ISO\/IEC 15909-2. PNNL\u00a076, 9\u201328 (2009)","journal-title":"PNNL"},{"key":"21_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/11691372_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Hinton","year":"2006","unstructured":"Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: A tool for automatic verification of probabilistic systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 441\u2013444. Springer, Heidelberg (2006)"},{"key":"21_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-540-77966-7_9","volume-title":"Hardware and Software: Verification and Testing","author":"D.N. Jansen","year":"2008","unstructured":"Jansen, D.N., Katoen, J.-P., Oldenkamp, M., Stoelinga, M., Zapreev, I.: How fast and fat is your probabilistic model checker? An experimental performance comparison. In: Yorav, K. (ed.) HVC 2007. LNCS, vol.\u00a04899, pp. 69\u201385. Springer, Heidelberg (2008)"},{"issue":"2","key":"21_CR18","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1016\/j.peva.2010.04.001","volume":"68","author":"J.P. Katoen","year":"2011","unstructured":"Katoen, J.P., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker MRMC. Performance Evaluation\u00a068(2), 90\u2013104 (2011)","journal-title":"Performance Evaluation"},{"key":"21_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/978-3-540-72522-0_6","volume-title":"Formal Methods for Performance Evaluation","author":"M. Kwiatkowska","year":"2007","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol.\u00a04486, pp. 220\u2013270. Springer, Heidelberg (2007)"},{"key":"21_CR20","unstructured":"Noack, A.: A ZBDD Package for Efficient Model Checking of Petri Nets (in German). Tech. rep., BTU Cottbus, Dep. of CS (1999)"},{"key":"21_CR21","unstructured":"Rohr, C.: Simulative Model Checking of Steady-State and Time-Unbounded Temporal Operators. In: Proc. BioPPN 2012, CEUR Workshop Proceedings, vol.\u00a0852, pp. 62\u201375. CEUR-WS.org (June 2012)"},{"key":"21_CR22","unstructured":"Sandmann, W., Maier, C.: On the statistical accuracy of stochastic simulation algorithms implemented in Dizzy. In: Proc. WCSB 2008, pp. 153\u2013156 (2008)"},{"issue":"17","key":"21_CR23","doi-asserted-by":"publisher","first-page":"2457","DOI":"10.1093\/bioinformatics\/btr401","volume":"27","author":"K.R. Sanft","year":"2011","unstructured":"Sanft, K.R., Wu, S., Roh, M., Fu, J., Lim, R.K., Petzold, L.R.: Stochkit2: software for discrete stochastic simulation of biochemical systems with events. Bioinformatics\u00a027(17), 2457\u20132458 (2011)","journal-title":"Bioinformatics"},{"key":"21_CR24","unstructured":"Schwarick, M.: Manual: Marcie - An analysis tool for Generalized Stochastic Petri nets. BTU Cottbus, Dep. of CS (2010)"},{"key":"21_CR25","unstructured":"Schwarick, M.: Symbolic model checking of stochastic reward nets. In: Proc. CS&P 2012, CEUR Workshop Proceedings, vol.\u00a0928, pp. 343\u2013357. CEUR-WS.org (2012)"},{"key":"21_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/978-3-642-03845-7_20","volume-title":"Computational Methods in Systems Biology","author":"M. Schwarick","year":"2009","unstructured":"Schwarick, M., Heiner, M.: CSL model checking of biochemical networks with interval decision diagrams. In: Degano, P., Gorrieri, R. (eds.) CMSB 2009. LNCS, vol.\u00a05688, pp. 296\u2013312. Springer, Heidelberg (2009)"},{"key":"21_CR27","doi-asserted-by":"crossref","unstructured":"Schwarick, M., Rohr, C., Heiner, M.: Marcie - model checking and reachability analysis done efficiently. In: Proc. QEST 2011, pp. 91\u2013100. IEEE CS Press (2011)","DOI":"10.1109\/QEST.2011.19"},{"key":"21_CR28","doi-asserted-by":"publisher","first-page":"2884","DOI":"10.1016\/j.tcs.2010.06.030","volume":"412","author":"M. Schwarick","year":"2010","unstructured":"Schwarick, M., Tovchigrechko, A.: IDD-based model validation of biochemical networks. TCS\u00a0412, 2884\u20132908 (2010)","journal-title":"TCS"},{"key":"21_CR29","unstructured":"Tovchigrechko, A.: Model Checking Using Interval Decision Diagrams. Ph.D. thesis, BTU Cottbus, Dep. of CS (2008)"}],"container-title":["Lecture Notes in Computer Science","Application and Theory of Petri Nets and Concurrency"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38697-8_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,14]],"date-time":"2019-05-14T04:01:33Z","timestamp":1557806493000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38697-8_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642386961","9783642386978"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38697-8_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}