{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:56:54Z","timestamp":1776333414293,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":57,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662545799","type":"print"},{"value":"9783662545805","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-662-54580-5_9","type":"book-chapter","created":{"date-parts":[[2017,3,30]],"date-time":"2017-03-30T06:50:09Z","timestamp":1490856609000},"page":"151-168","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":81,"title":["JANI: Quantitative Model and Tool Interaction"],"prefix":"10.1007","author":[{"given":"Carlos E.","family":"Budde","sequence":"first","affiliation":[]},{"given":"Christian","family":"Dehnert","sequence":"additional","affiliation":[]},{"given":"Ernst Moritz","family":"Hahn","sequence":"additional","affiliation":[]},{"given":"Arnd","family":"Hartmanns","sequence":"additional","affiliation":[]},{"given":"Sebastian","family":"Junges","sequence":"additional","affiliation":[]},{"given":"Andrea","family":"Turrini","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,3,31]]},"reference":[{"issue":"1","key":"9_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.jlap.2012.07.001","volume":"82","author":"DEN Agut","year":"2013","unstructured":"Agut, D.E.N., van Beek, D.A., Rooda, J.E.: Syntax and semantics of the compositional interchange format for hybrid systems. J. Log. Algebr. Program. 82(1), 1\u201352 (2013)","journal-title":"J. Log. Algebr. Program."},{"issue":"1","key":"9_CR2","first-page":"7","volume":"15","author":"R Alur","year":"1999","unstructured":"Alur, R., Henzinger, T.A.: Reactive modules. FMSD 15(1), 7\u201348 (1999)","journal-title":"FMSD"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/978-3-319-10696-0_13","volume-title":"Quantitative Evaluation of Systems","author":"EG Amparore","year":"2014","unstructured":"Amparore, E.G.: A new greatSPN GUI for GSPN editing and CSLTA model checking. In: Norman, G., Sanders, W. (eds.) QEST 2014. LNCS, vol. 8657, pp. 170\u2013173. Springer, Heidelberg (2014). doi:10.1007\/978-3-319-10696-0_13"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/978-3-319-21690-4_31","volume-title":"Computer Aided Verification","author":"T Babiak","year":"2015","unstructured":"Babiak, T., Blahoudek, F., Duret-Lutz, A., Klein, J., K\u0159et\u00ednsk\u00fd, J., M\u00fcller, D., Parker, D., Strej\u010dek, J.: The Hanoi omega-automata format. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 479\u2013486. Springer, Heidelberg (2015). doi:10.1007\/978-3-319-21690-4_31"},{"key":"9_CR5","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard: version 2.5. Technical report, Department of Computer Science, The University of Iowa (2015). www.smt-lib.org"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"575","DOI":"10.1007\/978-3-642-54862-8_48","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"DA van Beek","year":"2014","unstructured":"van Beek, D.A., Fokkink, W.J., Hendriks, D., Hofkamp, A., Markovski, J., van de Mortel-Fronczak, J.M., Reniers, M.A.: CIF 3: model-based engineering of supervisory controllers. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 575\u2013580. Springer, Heidelberg (2014). doi:10.1007\/978-3-642-54862-8_48"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Behrmann, G., David, A., Larsen, K.G., H\u00e5kansson, J., Pettersson, P., Yi, W., Hendriks, M.: UPPAAL 4.0. In: QEST, pp. 125\u2013126. IEEE CS (2006)","DOI":"10.1109\/QEST.2006.59"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/978-3-662-46681-0_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Beyer","year":"2015","unstructured":"Beyer, D.: Software verification and verifiable witnesses (report on SV-COMP 2015). In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 401\u2013416. Springer, Heidelberg (2015). doi:10.1007\/978-3-662-46681-0_31"},{"issue":"10","key":"9_CR9","first-page":"812","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 TSE 32(10), 812\u2013830 (2006)","journal-title":"IEEE TSE"},{"key":"9_CR10","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":"9_CR11","doi-asserted-by":"crossref","unstructured":"Bray, T.: The JavaScript Object Notation (JSON) data interchange format. RFC 7159, RFC Editor, March 2014. rfc-editor.org\/rfc\/rfc7159.txt","DOI":"10.17487\/rfc7159"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Budde, C.E., D\u2019Argenio, P.R., Monti, R.E.: Compositional construction of importance functions in fully automated importance splitting. In: VALUETOOLS, ICST (2016)","DOI":"10.4108\/eai.25-10-2016.2266501"},{"key":"9_CR13","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. IEEE CS (2009)","DOI":"10.1109\/DSN.2009.5270318"},{"issue":"1","key":"9_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.ic.2005.07.001","volume":"203","author":"PR D\u2019Argenio","year":"2005","unstructured":"D\u2019Argenio, P.R., Katoen, J.-P.: A theory of stochastic systems part I: stochastic automata. Inf. Comput. 203(1), 1\u201338 (2005)","journal-title":"Inf. Comput."},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-319-44878-7_4","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"PR D\u2019Argenio","year":"2016","unstructured":"D\u2019Argenio, P.R., Lee, M.D., Monti, R.E.: Input\/Output stochastic automata - compositionality and determinism. In: Fr\u00e4nzle, M., Markey, N. (eds.) FORMATS 2016. LNCS, vol. 9884, pp. 53\u201368. Springer, Cham (2016). doi:10.1007\/978-3-319-44878-7_4"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-319-21690-4_13","volume-title":"Computer Aided Verification","author":"C Dehnert","year":"2015","unstructured":"Dehnert, C., Junges, S., Jansen, N., Corzilius, F., Volk, M., Bruintjes, H., Katoen, J.-P., \u00c1brah\u00e1m, E.: PROPhESY: a PRObabilistic ParamEter SYnthesis tool. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 214\u2013231. Springer, Heidelberg (2015). doi:10.1007\/978-3-319-21690-4_13"},{"key":"9_CR17","unstructured":"Dehnert, C., Junges, S., Katoen, J.-P., Volk, M.: The probabilistic model checker Storm (extended abstract). CoRR abs\/1610.08713 (2016)"},{"key":"9_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-319-25942-0_3","volume-title":"Dependable Software Engineering: Theories, Tools, and Applications","author":"T van Dijk","year":"2015","unstructured":"van Dijk, T., Hahn, E.M., Jansen, D.N., Li, Y., Neele, T., Stoelinga, M., Turrini, A., Zhang, L.: A comparative study of BDD packages for probabilistic symbolic model checking. In: Li, X., Liu, Z., Yi, W. (eds.) SETTA 2015. LNCS, vol. 9409, pp. 35\u201351. Springer, Heidelberg (2015). doi:10.1007\/978-3-319-25942-0_3"},{"key":"9_CR19","unstructured":"Eclipse Foundation: Eclipse Modeling Framework (EMF). eclipse.org\/modeling\/emf. Accessed 27 Jan 2016"},{"key":"9_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). doi:10.1007\/978-3-642-38697-8_6"},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: LICS, pp. 342\u2013351. IEEE CS (2010)","DOI":"10.1109\/LICS.2010.41"},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-319-19249-9_17","volume-title":"FM 2015: Formal Methods","author":"Y Feng","year":"2015","unstructured":"Feng, Y., Hahn, E.M., Turrini, A., Zhang, L.: QPMC: a model checker for quantum programs and protocols. In: Bj\u00f8rner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 265\u2013272. Springer, Heidelberg (2015). doi:10.1007\/978-3-319-19249-9_17"},{"key":"9_CR23","unstructured":"Fette, I., Melnikov, A.: The WebSocket protocol. RFC 6455, RFC Editor, December 2011. rfc-editor.org\/rfc\/rfc6455.txt"},{"key":"9_CR24","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"},{"key":"9_CR25","doi-asserted-by":"crossref","unstructured":"Fritzson, P.: Modelica - a cyber-physical modeling language and the OpenModelica environment. In: IWCMC, pp. 1648\u20131653. IEEE (2011)","DOI":"10.1109\/IWCMC.2011.5982782"},{"issue":"2","key":"9_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":"9_CR27","doi-asserted-by":"crossref","unstructured":"Gordon, A.D., Henzinger, T.A., Nori, A.V., Rajamani, S.K.: Probabilistic programming. In: FOSE, pp. 167\u2013181. ACM (2014)","DOI":"10.1145\/2593882.2593900"},{"key":"9_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-319-47677-3_6","volume-title":"Dependable Software Engineering: Theories, Tools, and Applications","author":"EM Hahn","year":"2016","unstructured":"Hahn, E.M., Hartmanns, A.: A comparison of time- and reward-bounded probabilistic model checking techniques. In: Fr\u00e4nzle, M., Kapur, D., Zhan, N. (eds.) SETTA 2016. LNCS, vol. 9984, pp. 85\u2013100. Springer, Heidelberg (2016). doi:10.1007\/978-3-319-47677-3_6"},{"issue":"2","key":"9_CR29","first-page":"191","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. FMSD 43(2), 191\u2013232 (2013)","journal-title":"FMSD"},{"key":"9_CR30","unstructured":"Hahn, E.M., Li, G., Schewe, S., Turrini, A., Zhang, L.: Lazy probabilistic model checking without determinisation. In: CONCUR, vol. 42. LIPIcs, pp. 354\u2013367. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2015)"},{"key":"9_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-319-06410-9_22","volume-title":"FM 2014: Formal Methods","author":"EM Hahn","year":"2014","unstructured":"Hahn, E.M., Li, Y., Schewe, S., Turrini, A., Zhang, L.: IscasMc: a web-based probabilistic model checker. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 312\u2013317. Springer, Heidelberg (2014). doi:10.1007\/978-3-319-06410-9_22"},{"key":"9_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-319-41540-6_16","volume-title":"Computer Aided Verification","author":"EM Hahn","year":"2016","unstructured":"Hahn, E.M., Schewe, S., Turrini, A., Zhang, L.: A simple algorithm for solving qualitative probabilistic parity games. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 291\u2013311. Springer, Heidelberg (2016). doi:10.1007\/978-3-319-41540-6_16"},{"key":"9_CR33","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). doi:10.1007\/978-3-642-54862-8_51"},{"key":"9_CR34","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, Heidelberg (2015). doi:10.1007\/978-3-319-24953-7_10"},{"key":"9_CR35","doi-asserted-by":"crossref","unstructured":"Hartmanns, A., Hermanns, H., Bungert, M.: Flexible support for time and costs in scenario-aware dataflow. In: EMSOFT, pp. 3:1\u20133:10. ACM (2016)","DOI":"10.1145\/2968478.2968496"},{"key":"9_CR36","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":"5","key":"9_CR37","first-page":"279","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE TSE 23(5), 279\u2013295 (1997)","journal-title":"IEEE TSE"},{"key":"9_CR38","unstructured":"ISO 15909-2:2011. High-level Petri nets \u2013 Part 2: Transfer format (2011)"},{"key":"9_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"692","DOI":"10.1007\/978-3-662-46681-0_61","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Kant","year":"2015","unstructured":"Kant, G., Laarman, A., Meijer, J., van de Pol, J., Blom, S., van Dijk, T.: LTSmin: high-performance language-independent model checking. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 692\u2013707. Springer, Heidelberg (2015). doi:10.1007\/978-3-662-46681-0_61"},{"key":"9_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-319-23506-6_4","volume-title":"Correct System Design","author":"J-P Katoen","year":"2015","unstructured":"Katoen, J.-P., Gretz, F., Jansen, N., Kaminski, B.L., Olmedo, F.: Understanding probabilistic programs. In: Meyer, R., Platzer, A., Wehrheim, H. (eds.) Correct System Design. LNCS, vol. 9360, pp. 15\u201332. Springer, Heidelberg (2015). doi:10.1007\/978-3-319-23506-6_4"},{"issue":"2","key":"9_CR41","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. Perform. Eval. 68(2), 90\u2013104 (2011)","journal-title":"Perform. Eval."},{"key":"9_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/978-3-642-40196-1_24","volume-title":"Quantitative Evaluation of Systems","author":"K Keefe","year":"2013","unstructured":"Keefe, K., Sanders, W.H.: M\u00f6bius shell: a command-line interface for M\u00f6bius. In: Joshi, K., Siegle, M., Stoelinga, M., D\u2019Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 282\u2013285. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-40196-1_24"},{"key":"9_CR43","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":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., 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). doi:10.1007\/978-3-642-22110-1_47"},{"key":"9_CR44","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: The PRISM benchmark suite. In: QEST, pp. 203\u2013204. IEEE CS (2012)","DOI":"10.1109\/QEST.2012.14"},{"issue":"1","key":"9_CR45","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0304-3975(01)00046-9","volume":"282","author":"M Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. TCS 282(1), 101\u2013150 (2002)","journal-title":"TCS"},{"key":"9_CR46","doi-asserted-by":"crossref","unstructured":"L\u2019Ecuyer, P., Le Gland, F., Lezaud, P., Tuffin, B.: Splitting techniques. In: Rare Event Simulation using Monte Carlo Methods, pp. 39\u201361. Wiley, Ltd. (2009)","DOI":"10.1002\/9780470745403.ch3"},{"key":"9_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-642-12002-2_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M., R\u00fcmmer, P.: A polymorphic intermediate verification language: design and logical encoding. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 312\u2013327. Springer, Heidelberg (2010). doi:10.1007\/978-3-642-12002-2_26"},{"key":"9_CR48","volume-title":"Modelling with Generalized Stochastic Petri Nets","author":"MA Marsan","year":"1994","unstructured":"Marsan, M.A., Balbo, G., Conte, G., Donatelli, S., Franceschinis, G.: Modelling with Generalized Stochastic Petri Nets, 1st edn. Wiley, New York (1994)","edition":"1"},{"key":"9_CR49","series-title":"Monographs in Computer Science","volume-title":"Abstraction, Refinement and Proof for Probabilistic Systems","author":"A McIver","year":"2005","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science. Springer, New York (2005)"},{"key":"9_CR50","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-10235-3","volume-title":"A Calculus of Communicating Systems","author":"R Milner","year":"1980","unstructured":"Milner, R.: A Calculus of Communicating Systems. LNCS, vol. 92. Springer, Heidelberg (1980)"},{"key":"9_CR51","unstructured":"Moln\u00e1r, G.: js-schema website. molnarg.github.io\/js-schema. Accessed 28 Jan 2016"},{"key":"9_CR52","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. Wiley, New York (1994)"},{"key":"9_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-319-46520-3_4","volume-title":"Automated Technology for Verification and Analysis","author":"T Quatmann","year":"2016","unstructured":"Quatmann, T., Dehnert, C., Jansen, N., Junges, S., Katoen, J.-P.: Parameter synthesis for Markov models: faster than ever. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 50\u201367. Springer, Heidelberg (2016). doi:10.1007\/978-3-319-46520-3_4"},{"key":"9_CR54","unstructured":"Sanner, S.: Relational dynamic influence diagram language (RDDL): Language description (2010). http:\/\/users.cecs.anu.edu.au\/~ssanner\/IPPC_2011\/RDDL.pdf"},{"key":"9_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-642-00255-7_7","volume-title":"Integrated Formal Methods","author":"J St\u00f6cker","year":"2009","unstructured":"St\u00f6cker, J., Lang, F., Garavel, H.: Parallel processes with real-time and data: the ATLANTIF intermediate format. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol. 5423, pp. 88\u2013102. Springer, Heidelberg (2009). doi:10.1007\/978-3-642-00255-7_7"},{"key":"9_CR56","doi-asserted-by":"crossref","unstructured":"Theelen, B.D., Geilen, M., Basten, T., Voeten, J., Gheorghita, S.V., Stuijk, S.: A scenario-aware data flow model for combined long-run average and worst-case performance analysis. In: MEMOCODE, pp. 185\u2013194. IEEE CS (2006)","DOI":"10.1109\/MEMCOD.2006.1695924"},{"key":"9_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1007\/978-3-642-02742-0_22","volume-title":"Network Performance Engineering","author":"M Vill\u00e9n-Altamirano","year":"2011","unstructured":"Vill\u00e9n-Altamirano, M., Vill\u00e9n-Altamirano, J.: The rare event simulation method RESTART: efficiency analysis and guidelines for its application. In: Kouvatsos, D.D. (ed.) Network Performance Engineering. LNCS, vol. 5233, pp. 509\u2013547. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-02742-0_22"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-54580-5_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:27:04Z","timestamp":1750188424000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-54580-5_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783662545799","9783662545805"],"references-count":57,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-54580-5_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"31 March 2017","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":"Uppsala","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Sweden","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 April 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 April 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.etaps.org\/index.php\/2017\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}