{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T02:39:53Z","timestamp":1743129593202,"version":"3.40.3"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030174644"},{"type":"electronic","value":"9783030174651"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-17465-1_11","type":"book-chapter","created":{"date-parts":[[2019,4,3]],"date-time":"2019-04-03T22:50:37Z","timestamp":1554331837000},"page":"191-208","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Optimal Time-Bounded Reachability Analysis for Concurrent Systems"],"prefix":"10.1007","author":[{"given":"Yuliya","family":"Butkova","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gereon","family":"Fox","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,4,3]]},"reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-540-72522-0_3","volume-title":"Formal Methods for Performance Evaluation","author":"G Balbo","year":"2007","unstructured":"Balbo, G.: Introduction to generalized stochastic Petri nets. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol. 4486, pp. 83\u2013131. Springer, Heidelberg (2007). \n                      https:\/\/doi.org\/10.1007\/978-3-540-72522-0_3"},{"issue":"2","key":"11_CR2","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1109\/TDSC.2009.45","volume":"7","author":"H Boudali","year":"2010","unstructured":"Boudali, H., Crouzen, P., Stoelinga, M.: A rigorous, compositional, and extensible framework for dynamic fault tree analysis. IEEE Trans. Dependable Sec. Comput. 7(2), 128\u2013143 (2010). \n                      https:\/\/doi.org\/10.1109\/TDSC.2009.45","journal-title":"IEEE Trans. Dependable Sec. Comput."},{"key":"11_CR3","volume-title":"Dynamic Programming and Optimal Control","author":"DP Bertsekas","year":"2000","unstructured":"Bertsekas, D.P.: Dynamic Programming and Optimal Control, 2nd edn. Athena Scientific, Belmont (2000)","edition":"2"},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-319-24953-7_12","volume-title":"Automated Technology for Verification and Analysis","author":"Y Butkova","year":"2015","unstructured":"Butkova, Y., Hatefi, H., Hermanns, H., Kr\u010d\u00e1l, J.: Optimal continuous time Markov decisions. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 166\u2013182. Springer, Cham (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-319-24953-7_12"},{"key":"11_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-319-63387-9_8","volume-title":"Computer Aided Verification","author":"C Baier","year":"2017","unstructured":"Baier, C., Klein, J., Leuschner, L., Parker, D., Wunderlich, S.: Ensuring the reliability of your model checker: interval iteration for Markov decision processes. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 160\u2013180. Springer, Cham (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-319-63387-9_8"},{"issue":"3","key":"11_CR6","doi-asserted-by":"publisher","first-page":"651","DOI":"10.1016\/j.cor.2010.08.011","volume":"38","author":"P Buchholz","year":"2011","unstructured":"Buchholz, P., Schulz, I.: Numerical analysis of continuous time Markov decision processes over finite horizons. Comput. OR 38(3), 651\u2013659 (2011). \n                      https:\/\/doi.org\/10.1016\/j.cor.2010.08.011","journal-title":"Comput. OR"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"592","DOI":"10.1007\/978-3-319-63390-9_31","volume-title":"Computer Aided Verification","author":"C Dehnert","year":"2017","unstructured":"Dehnert, C., Junges, S., Katoen, J., Volk, M.: A storm is coming: a modern probabilistic model checker. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 592\u2013600. Springer, Cham (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-319-63390-9_31"},{"key":"11_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/978-3-642-38697-8_6","volume-title":"Application and Theory of Petri Nets and Concurrency","author":"C Eisentraut","year":"2013","unstructured":"Eisentraut, C., Hermanns, H., Katoen, J., Zhang, L.: A semantics for every GSPN. In: Colom, J.-M., Desel, J. (eds.) PETRI NETS 2013. LNCS, vol. 7927, pp. 90\u2013109. Springer, Heidelberg (2013). \n                      https:\/\/doi.org\/10.1007\/978-3-642-38697-8_6"},{"key":"11_CR9","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1016\/j.ic.2015.12.002","volume":"247","author":"J Fearnley","year":"2016","unstructured":"Fearnley, J., Rabe, M.N., Schewe, S., Zhang, L.: Efficient approximation of optimal control for continuous-time Markov games. Inf. Comput. 247, 106\u2013129 (2016). \n                      https:\/\/doi.org\/10.1016\/j.ic.2015.12.002","journal-title":"Inf. Comput."},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-642-40196-1_5","volume-title":"Quantitative Evaluation of Systems","author":"D Guck","year":"2013","unstructured":"Guck, D., Hatefi, H., Hermanns, H., Katoen, J., Timmer, M.: Modelling, reduction and analysis of Markov automata. In: Joshi, K., Siegle, M., Stoelinga, M., D\u2019Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 55\u201371. Springer, Heidelberg (2013). \n                      https:\/\/doi.org\/10.1007\/978-3-642-40196-1_5"},{"key":"11_CR11","doi-asserted-by":"publisher","unstructured":"Guck, D., Hatefi, H., Hermanns, H., Katoen, J., Timmer, M.: Analysis of timed and long-run objectives for Markov automata. Log. Methods Comput. Sci. 10(3) (2014). \n                      https:\/\/doi.org\/10.2168\/LMCS-10(3:17)2014","DOI":"10.2168\/LMCS-10(3:17)2014"},{"key":"11_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1007\/978-3-642-28891-3_4","volume-title":"NASA Formal Methods","author":"D Guck","year":"2012","unstructured":"Guck, D., Han, T., Katoen, J.-P., Neuh\u00e4u\u00dfer, M.R.: Quantitative timed analysis of interactive Markov chains. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 8\u201323. Springer, Heidelberg (2012). \n                      https:\/\/doi.org\/10.1007\/978-3-642-28891-3_4"},{"key":"11_CR13","unstructured":"Hatefi-Ardakani, H.: Finite horizon analysis of Markov automata. Ph.D. thesis, Saarland University, Germany (2017). \n                      http:\/\/scidok.sulb.uni-saarland.de\/volltexte\/2017\/6743\/"},{"key":"11_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45804-2","volume-title":"Interactive Markov Chains: The Quest for Quantified Quality","author":"H Hermanns","year":"2002","unstructured":"Hermanns, H.: Interactive Markov Chains: The Quest for Quantified Quality. LNCS, vol. 2428. Springer, Heidelberg (2002). \n                      https:\/\/doi.org\/10.1007\/3-540-45804-2"},{"key":"11_CR15","unstructured":"Hatefi, H., Hermanns, H.: Model checking algorithms for Markov automata. ECEASST 53 (2012). \n                      http:\/\/journal.ub.tu-berlin.de\/eceasst\/article\/view\/783"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"593","DOI":"10.1007\/978-3-642-54862-8_51","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Hartmanns","year":"2014","unstructured":"Hartmanns, A., Hermanns, H.: The modest toolset: an integrated environment for quantitative modelling and verification. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 593\u2013598. Springer, Heidelberg (2014). \n                      https:\/\/doi.org\/10.1007\/978-3-642-54862-8_51"},{"key":"11_CR17","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1016\/j.scico.2015.05.003","volume":"112","author":"H Hatefi","year":"2015","unstructured":"Hatefi, H., Hermanns, H.: Improving time bounded reachability computations in interactive Markov chains. Sci. Comput. Program. 112, 58\u201374 (2015). \n                      https:\/\/doi.org\/10.1016\/j.scico.2015.05.003","journal-title":"Sci. Comput. Program."},{"key":"11_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-319-11439-2_10","volume-title":"Reachability Problems","author":"S Haddad","year":"2014","unstructured":"Haddad, S., Monmege, B.: Reachability in MDPs: refining convergence of value iteration. In: Ouaknine, J., Potapov, I., Worrell, J. (eds.) RP 2014. LNCS, vol. 8762, pp. 125\u2013137. Springer, Cham (2014). \n                      https:\/\/doi.org\/10.1007\/978-3-319-11439-2_10"},{"issue":"sup1","key":"11_CR19","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1080\/03461238.1953.10419459","volume":"1953","author":"A Jensen","year":"1953","unstructured":"Jensen, A.: Markoff chains as an aid in the study of markoff processes. Scand. Actuarial J. 1953(sup1), 87\u201391 (1953). \n                      https:\/\/doi.org\/10.1080\/03461238.1953.10419459","journal-title":"Scand. Actuarial J."},{"key":"11_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"MZ Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). \n                      https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"issue":"2","key":"11_CR21","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/288197.581193","volume":"26","author":"MA Marsan","year":"1998","unstructured":"Marsan, M.A., Balbo, G., Conte, G., Donatelli, S., Franceschinis, G.: Modelling with generalized stochastic Petri nets. SIGMETRICS Perform. Eval. Rev. 26(2), 2 (1998). \n                      https:\/\/doi.org\/10.1145\/288197.581193","journal-title":"SIGMETRICS Perform. Eval. Rev."},{"issue":"2","key":"11_CR22","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1145\/190.191","volume":"2","author":"MA Marsan","year":"1984","unstructured":"Marsan, M.A., Conte, G., Balbo, G.: A class of generalized stochastic Petri nets for the performance evaluation of multiprocessor systems. ACM Trans. Comput. Syst. 2(2), 93\u2013122 (1984). \n                      https:\/\/doi.org\/10.1145\/190.191","journal-title":"ACM Trans. Comput. Syst."},{"issue":"2","key":"11_CR23","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1137\/0306020","volume":"6","author":"B Miller","year":"1968","unstructured":"Miller, B.: Finite state continuous time Markov decision processes with a finite planning horizon. SIAM J. Control 6(2), 266\u2013280 (1968). \n                      https:\/\/doi.org\/10.1137\/0306020","journal-title":"SIAM J. Control"},{"key":"11_CR24","unstructured":"Meyer, J.F., Movaghar, A., Sanders, W.H.: Stochastic activity networks: structure, behavior, and application. In: International Workshop on Timed Petri Nets, Torino, pp. 106\u2013115. IEEE Computer Society (1985)"},{"issue":"9","key":"11_CR25","doi-asserted-by":"publisher","first-page":"913","DOI":"10.1109\/TC.1982.1676110","volume":"C\u201331","author":"MK Molloy","year":"1982","unstructured":"Molloy, M.K.: Performance analysis using stochastic Petri nets. IEEE Trans. Comput. C\u201331(9), 913\u2013917 (1982)","journal-title":"IEEE Trans. Comput."},{"key":"11_CR26","unstructured":"Neuh\u00e4u\u00dfer, M.R.: Model checking nondeterministic and randomly timed systems. Ph.D. thesis, RWTH Aachen University (2010). \n                      http:\/\/darwin.bth.rwth-aachen.de\/opus3\/volltexte\/2010\/3136\/"},{"key":"11_CR27","doi-asserted-by":"publisher","DOI":"10.1002\/9780470316887","volume-title":"Markov Decision Processes: Discrete Stochastic Dynamic Programming","author":"ML Puterman","year":"1994","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming, 1st edn. Wiley, Hoboken (1994)","edition":"1"},{"key":"11_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"643","DOI":"10.1007\/978-3-319-96145-3_37","volume-title":"Computer Aided Verification","author":"T Quatmann","year":"2018","unstructured":"Quatmann, T., Katoen, J.-P.: Sound value iteration. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 643\u2013661. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-319-96145-3_37"},{"key":"11_CR29","doi-asserted-by":"publisher","unstructured":"Qiu, Q. Wu, Q., Pedram, M.: Stochastic modeling of a power-managed system: construction and optimization. In: ISLPED, 1999, pp. 194\u2013199. ACM (1999). \n                      https:\/\/doi.org\/10.1145\/313817.313923","DOI":"10.1145\/313817.313923"},{"key":"11_CR30","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/j.tcs.2012.10.001","volume":"467","author":"MN Rabe","year":"2013","unstructured":"Rabe, M.N., Schewe, S.: Optimal time-abstract schedulers for CTMDPs and continuous-time Markov games. Theor. Comput. Sci. 467, 53\u201367 (2013). \n                      https:\/\/doi.org\/10.1016\/j.tcs.2012.10.001","journal-title":"Theor. Comput. Sci."},{"key":"11_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-319-99154-2_24","volume-title":"Quantitative Evaluation of Systems","author":"M Salamati","year":"2018","unstructured":"Salamati, M., Soudjani, S., Majumdar, R.: Approximate time bounded reachability for CTMCs and CTMDPs: a Lyapunov approach. In: McIver, A., Horvath, A. (eds.) QEST 2018. LNCS, vol. 11024, pp. 389\u2013406. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-319-99154-2_24"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-17465-1_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T09:52:00Z","timestamp":1558345920000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-17465-1_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030174644","9783030174651"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-17465-1_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"3 April 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2019\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"164","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"42","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"8","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"26% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"13","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"12 full papers and 11 short papers accepted for TOOLympics and SV-COMP (avg. 4 reviewers\/paper, selected from 43 submissions)","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}}]}}