{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,12]],"date-time":"2026-01-12T23:30:52Z","timestamp":1768260652346,"version":"3.49.0"},"publisher-location":"Cham","reference-count":52,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030314224","type":"print"},{"value":"9783030314231","type":"electronic"}],"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-31423-1_8","type":"book-chapter","created":{"date-parts":[[2019,9,17]],"date-time":"2019-09-17T17:03:56Z","timestamp":1568739836000},"page":"250-276","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["A Modest Markov Automata Tutorial"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3268-8674","authenticated-orcid":false,"given":"Arnd","family":"Hartmanns","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2766-9615","authenticated-orcid":false,"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,9,13]]},"reference":[{"key":"8_CR1","series-title":"Springer Series in Reliability Engineering","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-3-319-30599-8_9","volume-title":"Principles of Performance and Reliability Modeling and Evaluation","author":"EG Amparore","year":"2016","unstructured":"Amparore, E.G., Balbo, G., Beccuti, M., Donatelli, S., Franceschinis, G.: 30 years of GreatSPN. In: Fiondella, L., Puliafito, A. (eds.) Principles of Performance and Reliability Modeling and Evaluation. SSRE, pp. 227\u2013254. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-30599-8_9"},{"issue":"9","key":"8_CR2","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1145\/1810891.1810912","volume":"53","author":"C Baier","year":"2010","unstructured":"Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.P.: Performance evaluation and model checking join forces. Commun. ACM 53(9), 76\u201385 (2010)","journal-title":"Commun. ACM"},{"key":"8_CR3","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"issue":"10","key":"8_CR4","doi-asserted-by":"publisher","first-page":"812","DOI":"10.1109\/TSE.2006.104","volume":"32","author":"HC Bohnenkamp","year":"2006","unstructured":"Bohnenkamp, H.C., D\u2019Argenio, P.R., Hermanns, H., Katoen, J.P.: MoDeST: a compositional modeling formalism for hard and softly timed systems. IEEE Trans. Softw. Eng. 32(10), 812\u2013830 (2006)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"8_CR5","doi-asserted-by":"publisher","DOI":"10.1002\/0471791571","volume-title":"Queueing Networks and Markov Chains - Modeling and Performance Evaluation with Computer Science Applications","author":"G Bolch","year":"2006","unstructured":"Bolch, G., Greiner, S., de Meer, H., Trivedi, K.S.: Queueing Networks and Markov Chains - Modeling and Performance Evaluation with Computer Science Applications, 2nd edn. Wiley, Hoboken (2006)","edition":"2"},{"key":"8_CR6","first-page":"25","volume":"14","author":"T Bolognesi","year":"1987","unstructured":"Bolognesi, T., Brinksma, E.: Introduction to the ISO specification language LOTOS. Comput. Netw. 14, 25\u201359 (1987)","journal-title":"Comput. Netw."},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Bonneau, J., Miller, A., Clark, J., Narayanan, A., Kroll, J.A., Felten, E.W.: SoK: research perspectives and challenges for Bitcoin and cryptocurrencies. In: SP, pp. 104\u2013121. IEEE Computer Society (2015)","DOI":"10.1109\/SP.2015.14"},{"key":"8_CR8","doi-asserted-by":"publisher","first-page":"48","DOI":"10.4204\/EPTCS.154.4","volume":"154","author":"Bettina Braitling","year":"2014","unstructured":"Braitling, B., Fioriti, L.M.F., Hatefi, H., Wimmer, R., Becker, B., Hermanns, H.: MeGARA: menu-based game abstraction and abstraction refinement of Markov automata. In: QAPL. EPTCS, vol. 154, pp. 48\u201363 (2014)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-662-46081-8_10","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"B Braitling","year":"2015","unstructured":"Braitling, B., Ferrer Fioriti, L.M., Hatefi, H., Wimmer, R., Becker, B., Hermanns, H.: Abstraction-based computation of reward measures for Markov automata. In: D\u2019Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 172\u2013189. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46081-8_10"},{"key":"8_CR10","unstructured":"Br\u00e1zdil, T., Hermanns, H., Krc\u00e1l, J., Kret\u00ednsk\u00fd, J., Reh\u00e1k, V.: Verification of open interactive Markov chains. In: FSTTCS. LIPIcs, vol. 18, pp. 474\u2013485. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2012)"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/978-3-319-89963-3_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"CE Budde","year":"2018","unstructured":"Budde, C.E., D\u2019Argenio, P.R., Hartmanns, A., Sedwards, S.: A statistical model checker for nondeterminism and rare events. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 340\u2013358. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_20"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-662-54580-5_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"CE Budde","year":"2017","unstructured":"Budde, C.E., Dehnert, C., Hahn, E.M., Hartmanns, A., Junges, S., Turrini, A.: JANI: quantitative model and tool interaction. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 151\u2013168. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_9"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-030-30281-8_4","volume-title":"Quantitative Evaluation of Systems","author":"Y Butkova","year":"2019","unstructured":"Butkova, Y., Hartmanns, A., Hermanns, H.: A Modest approach to modelling and checking Markov automata. In: Parker, D., Wolf, V. (eds.) QEST 2019. LNCS, vol. 1785, pp. 52\u201369. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30281-8_4"},{"key":"8_CR14","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). https:\/\/doi.org\/10.1007\/978-3-319-24953-7_12"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-662-54580-5_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y Butkova","year":"2017","unstructured":"Butkova, Y., Wimmer, R., Hermanns, H.: Long-run rewards for Markov automata. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 188\u2013203. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_11"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-319-74947-1_2","volume-title":"Measurement, Modelling and Evaluation of Computing Systems","author":"Y Butkova","year":"2018","unstructured":"Butkova, Y., Wimmer, R., Hermanns, H.: Markov automata on discount!. In: German, R., Hielscher, K.-S., Krieger, U.R. (eds.) MMB 2018. LNCS, vol. 10740, pp. 19\u201334. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-74947-1_2"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/978-3-030-03421-4_22","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Verification","author":"PR D\u2019Argenio","year":"2018","unstructured":"D\u2019Argenio, P.R., Hartmanns, A., Sedwards, S.: Lightweight statistical model checking in nondeterministic continuous time. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 336\u2013353. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03421-4_22"},{"key":"8_CR18","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.-P., 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). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_31"},{"key":"8_CR19","unstructured":"Eisentraut, C.: Principles of Markov automata. Ph.D. thesis, Saarland University, Saarbr\u00fccken, Germany (2017)"},{"key":"8_CR20","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.-P., 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). https:\/\/doi.org\/10.1007\/978-3-642-38697-8_6"},{"issue":"Part","key":"8_CR21","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1016\/j.ic.2018.08.003","volume":"262","author":"C Eisentraut","year":"2018","unstructured":"Eisentraut, C., Hermanns, H., Schuster, J., Turrini, A., Zhang, L.: The quest for minimal quotients for probabilistic and Markov automata. Inf. Comput. 262(Part), 162\u2013186 (2018)","journal-title":"Inf. Comput."},{"key":"8_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-642-15375-4_3","volume-title":"CONCUR 2010 - Concurrency Theory","author":"C Eisentraut","year":"2010","unstructured":"Eisentraut, C., Hermanns, H., Zhang, L.: Concurrency and composition in a stochastic world. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 21\u201339. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15375-4_3"},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: LICS, pp. 342\u2013351. IEEE Computer Society (2010)","DOI":"10.1109\/LICS.2010.41"},{"key":"8_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-319-77935-5_11","volume-title":"NASA Formal Methods","author":"A Fehnker","year":"2018","unstructured":"Fehnker, A., Chaudhary, K.: Twenty percent and a few days \u2013 optimising a Bitcoin majority attack. In: Dutle, A., Mu\u00f1oz, C., Narkawicz, A. (eds.) NFM 2018. LNCS, vol. 10811, pp. 157\u2013163. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-77935-5_11"},{"key":"8_CR25","doi-asserted-by":"crossref","unstructured":"Fr\u00e4nzle, M., Hahn, E.M., Hermanns, H., Wolovick, N., Zhang, L.: Measurability and safety verification for stochastic hybrid systems. In: HSCC, pp. 43\u201352. ACM (2011)","DOI":"10.1145\/1967701.1967710"},{"issue":"2","key":"8_CR26","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/s10009-012-0244-z","volume":"15","author":"H Garavel","year":"2013","unstructured":"Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: a toolbox for the construction and analysis of distributed processes. STTT 15(2), 89\u2013107 (2013)","journal-title":"STTT"},{"key":"8_CR27","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). https:\/\/doi.org\/10.1007\/978-3-642-28891-3_4"},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"Guck, D., Hatefi, H., Hermanns, H., Katoen, J.P., Timmer, M.: Analysis of timed and long-run objectives for Markov automata. Logical Methods Comput. Sci. 10(3) (2014)","DOI":"10.2168\/LMCS-10(3:17)2014"},{"key":"8_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-319-11936-6_13","volume-title":"Automated Technology for Verification and Analysis","author":"D Guck","year":"2014","unstructured":"Guck, D., Timmer, M., Hatefi, H., Ruijters, E., Stoelinga, M.: Modelling and analysis of Markov reward automata. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 168\u2013184. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11936-6_13"},{"issue":"2","key":"8_CR30","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s10703-012-0167-z","volume":"43","author":"EM Hahn","year":"2013","unstructured":"Hahn, E.M., Hartmanns, A., Hermanns, H., Katoen, J.P.: A compositional modelling and analysis framework for stochastic hybrid systems. Formal Methods Syst. Des. 43(2), 191\u2013232 (2013)","journal-title":"Formal Methods Syst. Des."},{"key":"8_CR31","doi-asserted-by":"publisher","unstructured":"Hartmanns, A.: A Modest Markov automata tutorial (artifact). 4TU.Centre for Research Data (2019). https:\/\/doi.org\/10.4121\/uuid:5a73169e-b494-411b-b3a8-051e62efba9e","DOI":"10.4121\/uuid:5a73169e-b494-411b-b3a8-051e62efba9e"},{"key":"8_CR32","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). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_51"},{"key":"8_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-319-24953-7_10","volume-title":"Automated Technology for Verification and Analysis","author":"A Hartmanns","year":"2015","unstructured":"Hartmanns, A., Hermanns, H.: Explicit model checking of very large MDP using partitioning and secondary storage. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 131\u2013147. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24953-7_10"},{"key":"8_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"344","DOI":"10.1007\/978-3-030-17462-0_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Hartmanns","year":"2019","unstructured":"Hartmanns, A., Klauck, M., Parker, D., Quatmann, T., Ruijters, E.: The quantitative verification benchmark set. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 344\u2013350. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_20"},{"key":"8_CR35","unstructured":"Hatefi, H.: Finite horizon analysis of Markov automata. Ph.D. thesis, Saarland University, Germany (2017). scidok.sulb.uni-saarland.de\/volltexte\/2017\/6743\/"},{"key":"8_CR36","unstructured":"Hatefi, H., Hermanns, H.: Model checking algorithms for Markov automata. Electron. Commun. EASST 53 (2012)"},{"issue":"4","key":"8_CR37","doi-asserted-by":"publisher","first-page":"629","DOI":"10.1007\/s00165-016-0411-1","volume":"29","author":"H Hatefi","year":"2017","unstructured":"Hatefi, H., Wimmer, R., Braitling, B., Fioriti, L.M.F., Becker, B., Hermanns, H.: Cost vs. time in stochastic games and Markov automata. Formal Asp. Comput. 29(4), 629\u2013649 (2017)","journal-title":"Formal Asp. Comput."},{"key":"8_CR38","doi-asserted-by":"publisher","DOI":"10.1002\/0470841923","volume-title":"Performance of Computer Communication Systems - A Model-Based Approach","author":"BR Haverkort","year":"1998","unstructured":"Haverkort, B.R.: Performance of Computer Communication Systems - A Model-Based Approach. Wiley, Hoboken (1998)"},{"key":"8_CR39","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/3-540-45804-2_3","volume-title":"Interactive Markov Chains","author":"Holger Hermanns","year":"2002","unstructured":"Hermanns, H.: Interactive Markov Chains: The Quest for Quantified Quality. LNCS, vol. 2428, pp. 35\u201355. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45804-2_3"},{"key":"8_CR40","volume-title":"Communicating Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Upper Saddle River (1985)"},{"issue":"1","key":"8_CR41","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1287\/mnsc.10.1.131","volume":"10","author":"JR Jackson","year":"1963","unstructured":"Jackson, J.R.: Jobshop-like queueing systems. Manag. Sci. 10(1), 131\u2013142 (1963)","journal-title":"Manag. Sci."},{"issue":"1","key":"8_CR42","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0304-3975(01)00046-9","volume":"282","author":"MZ Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M.Z., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Theor. Comput. Sci. 282(1), 101\u2013150 (2002)","journal-title":"Theor. Comput. Sci."},{"key":"8_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/978-3-319-15201-1_23","volume-title":"Software Engineering and Formal Methods","author":"A Legay","year":"2015","unstructured":"Legay, A., Sedwards, S., Traonouez, L.-M.: Scalable verification of Markov decision processes. In: Canal, C., Idani, A. (eds.) SEFM 2014. LNCS, vol. 8938, pp. 350\u2013362. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-15201-1_23"},{"key":"8_CR44","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall, Upper Saddle River (1989)"},{"key":"8_CR45","unstructured":"Nakamoto, S.: Bitcoin: A peer-to-peer electronic cash system (2009). bitcoin.org"},{"key":"8_CR46","doi-asserted-by":"crossref","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley Series in Probability and Statistics, Wiley, Hoboken (1994)","DOI":"10.1002\/9780470316887"},{"key":"8_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-319-63387-9_7","volume-title":"Computer Aided Verification","author":"T Quatmann","year":"2017","unstructured":"Quatmann, T., Junges, S., Katoen, J.-P.: Markov automata with multiple objectives. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 140\u2013159. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_7"},{"issue":"5\u20136","key":"8_CR48","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/s00236-011-0140-0","volume":"48","author":"MN Rabe","year":"2011","unstructured":"Rabe, M.N., Schewe, S.: Finite optimal control for time-bounded reachability in CTMDPs and continuous-time Markov games. Acta Inf. 48(5\u20136), 291\u2013315 (2011)","journal-title":"Acta Inf."},{"key":"8_CR49","unstructured":"Segala, R.: Modeling and verification of randomized distributed real-time systems. Ph.D. thesis, Massachusetts Institute of Technology, Cambridge (1995)"},{"key":"8_CR50","unstructured":"Timmer, M.: Efficient modelling, generation and analysis of Markov automata. Ph.D. thesis, University of Twente, Enschede (2013)"},{"key":"8_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/978-3-642-32940-1_26","volume-title":"CONCUR 2012 \u2013 Concurrency Theory","author":"M Timmer","year":"2012","unstructured":"Timmer, M., Katoen, J.-P., van de Pol, J., Stoelinga, M.I.A.: Efficient modelling and generation of Markov automata. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 364\u2013379. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32940-1_26"},{"key":"8_CR52","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1016\/j.tcs.2016.01.017","volume":"655","author":"M Timmer","year":"2016","unstructured":"Timmer, M., Katoen, J.P., van de Pol, J., Stoelinga, M.: Confluence reduction for Markov automata. Theor. Comput. Sci. 655, 193\u2013219 (2016)","journal-title":"Theor. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Reasoning Web. Explainable Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-31423-1_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,11]],"date-time":"2024-03-11T15:07:54Z","timestamp":1710169674000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-31423-1_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030314224","9783030314231"],"references-count":52,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-31423-1_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"13 September 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}