{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T09:26:07Z","timestamp":1750843567883,"version":"3.40.3"},"publisher-location":"Cham","reference-count":54,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030851712"},{"type":"electronic","value":"9783030851729"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"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":[[2021]]},"DOI":"10.1007\/978-3-030-85172-9_3","type":"book-chapter","created":{"date-parts":[[2021,8,18]],"date-time":"2021-08-18T23:04:46Z","timestamp":1629327886000},"page":"39-58","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Tweaking the Odds in Probabilistic Timed Automata"],"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-6143-1926","authenticated-orcid":false,"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2908-8838","authenticated-orcid":false,"given":"Bram","family":"Kohlen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9113-2791","authenticated-orcid":false,"given":"Jip","family":"Spel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,8,19]]},"reference":[{"doi-asserted-by":"publisher","unstructured":"Agha, G., Palmskog, K.: A survey of statistical model checking. ACM Trans. Model. Comput. Simul. 28(1), 6:1\u20136:39 (2018). https:\/\/doi.org\/10.1145\/3158668","key":"3_CR1","DOI":"10.1145\/3158668"},{"issue":"2","key":"3_CR2","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"doi-asserted-by":"publisher","unstructured":"Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: STOC, pp. 592\u2013601. ACM (1993). https:\/\/doi.org\/10.1145\/167088.167242","key":"3_CR3","DOI":"10.1145\/167088.167242"},{"issue":"2","key":"3_CR4","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/s10009-017-0467-0","volume":"21","author":"\u00c9 Andr\u00e9","year":"2019","unstructured":"Andr\u00e9, \u00c9.: What\u2019s decidable about parametric timed automata? Int. J. Softw. Tools Technol. Transf. 21(2), 203\u2013219 (2019). https:\/\/doi.org\/10.1007\/s10009-017-0467-0","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-030-72016-2_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"\u00c9 Andr\u00e9","year":"2021","unstructured":"Andr\u00e9, \u00c9., Arias, J., Petrucci, L., Pol, J.: Iterative bounded synthesis for efficient cycle detection in parametric timed automata. In: TACAS 2021. LNCS, vol. 12651, pp. 311\u2013329. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72016-2_17"},{"issue":"5","key":"3_CR6","doi-asserted-by":"publisher","first-page":"819","DOI":"10.1142\/S0129054109006905","volume":"20","author":"\u00c9 Andr\u00e9","year":"2009","unstructured":"Andr\u00e9, \u00c9., Chatain, T., Fribourg, L., Encrenaz, E.: An inverse method for parametric timed automata. Int. J. Found. Comput. Sci. 20(5), 819\u2013836 (2009). https:\/\/doi.org\/10.1142\/S0129054109006905","journal-title":"Int. J. Found. Comput. Sci."},{"doi-asserted-by":"publisher","unstructured":"Andr\u00e9, \u00c9., Delahaye, B., Fournier, P.: Consistency in parametric interval probabilistic timed automata. J. Log. Algebraic Methods Program. 110, 100459 (2020). https:\/\/doi.org\/10.1016\/j.jlamp.2019.04.007","key":"3_CR7","DOI":"10.1016\/j.jlamp.2019.04.007"},{"issue":"2","key":"3_CR8","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/s10703-012-0169-x","volume":"42","author":"\u00c9 Andr\u00e9","year":"2013","unstructured":"Andr\u00e9, \u00c9., Fribourg, L., Sproston, J.: An extension of the inverse method to probabilistic timed automata. Formal Methods Syst. Des. 42(2), 119\u2013145 (2013). https:\/\/doi.org\/10.1007\/s10703-012-0169-x","journal-title":"Formal Methods Syst. Des."},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1007\/BFb0055642","volume-title":"CONCUR 1998 Concurrency Theory","author":"E Asarin","year":"1998","unstructured":"Asarin, E., Maler, O., Pnueli, A.: On discretization of delays in timed automata and digital circuits. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 470\u2013484. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0055642"},{"key":"3_CR10","doi-asserted-by":"publisher","first-page":"963","DOI":"10.1007\/978-3-319-10575-8_28","volume-title":"Handbook of Model Checking","author":"C Baier","year":"2018","unstructured":"Baier, C., de Alfaro, L., Forejt, V., Kwiatkowska, M.: Model checking probabilistic systems. In: Clarke, E., Henzinger, T., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 963\u2013999. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_28"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-319-91908-9_21","volume-title":"Computing and Software Science","author":"C Baier","year":"2019","unstructured":"Baier, C., Hermanns, H., Katoen, J.-P.: The 10,000 facets of MDP model checking. In: Steffen, B., Woeginger, G. (eds.) Computing and Software Science. LNCS, vol. 10000, pp. 420\u2013451. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-319-91908-9_21"},{"key":"3_CR12","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"issue":"10","key":"3_CR13","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. Software Eng. 32(10), 812\u2013830 (2006). https:\/\/doi.org\/10.1109\/TSE.2006.104","journal-title":"IEEE Trans. Software Eng."},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-642-39799-8_7","volume-title":"Computer Aided Verification","author":"L Brim","year":"2013","unstructured":"Brim, L., \u010ce\u0161ka, M., Dra\u017ean, S., \u0160afr\u00e1nek, D.: Exploring parameter space of stochastic biochemical systems using quantitative model checking. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 107\u2013123. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_7"},{"issue":"6","key":"3_CR15","doi-asserted-by":"publisher","first-page":"759","DOI":"10.1007\/s10009-020-00563-2","volume":"22","author":"CE Budde","year":"2020","unstructured":"Budde, C.E., D\u2019Argenio, P.R., Hartmanns, A., Sedwards, S.: An efficient statistical model checker for nondeterminism and rare events. Int. J. Softw. Tools Technol. Transf. 22(6), 759\u2013780 (2020). https:\/\/doi.org\/10.1007\/s10009-020-00563-2","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"3_CR16","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"},{"doi-asserted-by":"publisher","unstructured":"Chen, T., Han, T., Katoen, J.: Time-abstracting bisimulation for probabilistic timed automata. In: Second IEEE\/IFIP International Symposium on Theoretical Aspects of Software Engineering, TASE 2008, 17\u201319 June, 2008, Nanjing, China, pp. 177\u2013184. IEEE Computer Society (2008). https:\/\/doi.org\/10.1109\/TASE.2008.29","key":"3_CR17","DOI":"10.1109\/TASE.2008.29"},{"key":"3_CR18","first-page":"1","volume":"3927","author":"S Cheshire","year":"2005","unstructured":"Cheshire, S., Aboba, B., Guttman, E.: Dynamic configuration of ipv4 link-local addresses. RFC 3927, 1\u201333 (2005)","journal-title":"RFC"},{"key":"3_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-030-01090-4_10","volume-title":"Automated Technology for Verification and Analysis","author":"M Cubuktepe","year":"2018","unstructured":"Cubuktepe, M., Jansen, N., Junges, S., Katoen, J.-P., Topcu, U.: Synthesis in pMDPs: a tale of 1001 parameters. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 160\u2013176. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_10"},{"key":"3_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-319-33693-0_7","volume-title":"Integrated Formal Methods","author":"PR D\u2019Argenio","year":"2016","unstructured":"D\u2019Argenio, P.R., Hartmanns, A., Legay, A., Sedwards, S.: Statistical approximation of optimal schedulers for probabilistic timed automata. In: \u00c1brah\u00e1m, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 99\u2013114. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33693-0_7"},{"issue":"4","key":"3_CR21","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/s10009-014-0361-y","volume":"17","author":"A David","year":"2015","unstructured":"David, A., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B.: Uppaal SMC tutorial. Int. J. Softw. Tools Technol. Transf. 17(4), 397\u2013415 (2015). https:\/\/doi.org\/10.1007\/s10009-014-0361-y","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"2\u20133","key":"3_CR22","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/s10009-003-0118-5","volume":"5","author":"C Daws","year":"2004","unstructured":"Daws, C., Kwiatkowska, M.Z., Norman, G.: Automatic verification of the IEEE 1394 root contention protocol with KRONOS and PRISM. Int. J. Softw. Tools Technol. Transf. 5(2\u20133), 221\u2013236 (2004)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"doi-asserted-by":"crossref","unstructured":"Dombrowski, C., Junges, S., Katoen, J., Gross, J.: Model-checking assisted protocol design for ultra-reliable low-latency wireless networks. In: SRDS, pp. 307\u2013316. IEEE Computer Society (2016)","key":"3_CR23","DOI":"10.1109\/SRDS.2016.048"},{"doi-asserted-by":"crossref","unstructured":"Fruth, M.: Probabilistic model checking of contention resolution in the IEEE 802.15.4 low-rate wireless personal area network protocol. In: ISoLA, pp. 290\u2013297. IEEE Computer Society (2006)","key":"3_CR24","DOI":"10.1109\/ISoLA.2006.34"},{"unstructured":"Gregersen, H., Jensen, H.E.: Formal Design of Reliable Real Time Systems. Master\u2019s thesis, Department of Mathematics and Computer Science, Aalborg University (1995)","key":"3_CR25"},{"issue":"2","key":"3_CR26","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). https:\/\/doi.org\/10.1007\/s10703-012-0167-z","journal-title":"Formal Methods Syst. Des."},{"doi-asserted-by":"crossref","unstructured":"Hartmanns, A., Hermanns, H.: A Modest approach to checking probabilistic timed automata. In: QEST, pp. 187\u2013196. IEEE (2009)","key":"3_CR27","DOI":"10.1109\/QEST.2009.41"},{"key":"3_CR28","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"},{"doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Katoen, J.P., Kohlen, B., Spel, J.: Tweaking the odds in probabilistic timed automata (artifact). 4TU.Centre for Research Data (2021). https:\/\/doi.org\/10.4121\/14910426","key":"3_CR29","DOI":"10.4121\/14910426"},{"key":"3_CR30","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"},{"doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Sedwards, S., D\u2019Argenio, P.R.: Efficient simulation-based verification of probabilistic timed automata. In: WSC, pp. 1419\u20131430. IEEE (2017). https:\/\/doi.org\/10.1109\/WSC.2017.8247885","key":"3_CR31","DOI":"10.1109\/WSC.2017.8247885"},{"key":"3_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/3-540-58085-9_75","volume-title":"Types for Proofs and Programs","author":"L Helmink","year":"1994","unstructured":"Helmink, L., Sellink, M.P.A., Vaandrager, F.W.: Proof-checking a data link protocol. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol. 806, pp. 127\u2013165. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58085-9_75"},{"doi-asserted-by":"crossref","unstructured":"Hensel, C., Junges, S., Katoen, J.P., Quatmann, T., Volk, M.: The probabilistic model checker storm. CoRR abs\/2002.07080 (2020)","key":"3_CR33","DOI":"10.1007\/s10009-021-00633-z"},{"key":"3_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1007\/3-540-55719-9_103","volume-title":"Automata, Languages and Programming","author":"TA Henzinger","year":"1992","unstructured":"Henzinger, T.A., Manna, Z., Pnueli, A.: What good are digital clocks? In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 545\u2013558. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55719-9_103"},{"key":"3_CR35","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/S1567-8326(02)00037-1","volume":"52\u201353","author":"T Hune","year":"2002","unstructured":"Hune, T., Romijn, J., Stoelinga, M., Vaandrager, F.W.: Linear parametric model checking of timed automata. J. Log. Algebraic Methods Program. 52\u201353, 183\u2013220 (2002). https:\/\/doi.org\/10.1016\/S1567-8326(02)00037-1","journal-title":"J. Log. Algebraic Methods Program."},{"doi-asserted-by":"publisher","unstructured":"Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: LICS, pp. 266\u2013277. IEEE Computer Society (1991). https:\/\/doi.org\/10.1109\/LICS.1991.151651","key":"3_CR36","DOI":"10.1109\/LICS.1991.151651"},{"issue":"5","key":"3_CR37","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1109\/TSE.2014.2357445","volume":"41","author":"A Jovanovic","year":"2015","unstructured":"Jovanovic, A., Lime, D., Roux, O.H.: Integer parameter synthesis for real-time systems. IEEE Trans. Softw. Eng. 41(5), 445\u2013461 (2015). https:\/\/doi.org\/10.1109\/TSE.2014.2357445","journal-title":"IEEE Trans. Softw. Eng."},{"key":"3_CR38","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/j.jcss.2021.02.006","volume":"119","author":"S Junges","year":"2021","unstructured":"Junges, S., Katoen, J., P\u00e9rez, G.A., Winkler, T.: The complexity of reachability in parametric Markov decision processes. J. Comput. Syst. Sci. 119, 183\u2013210 (2021)","journal-title":"J. Comput. Syst. Sci."},{"key":"3_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-030-59854-9_6","volume-title":"Quantitative Evaluation of Systems","author":"M Kamali","year":"2020","unstructured":"Kamali, M., Katoen, J.-P.: Probabilistic model checking of AODV. In: Gribaudo, M., Jansen, D.N., Remke, A. (eds.) QEST 2020. LNCS, vol. 12289, pp. 54\u201373. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-59854-9_6"},{"unstructured":"Kohlen, B.: Parameter synthesis in probabilistic timed automata. Master\u2019s thesis, RWTH Aachen University, Aachen (2020). https:\/\/publications.rwth-aachen.de\/record\/811856","key":"3_CR40"},{"doi-asserted-by":"crossref","unstructured":"Krause, C., Giese, H.: Model checking probabilistic real-time properties for service-oriented systems with service level agreements. INFINITY. EPTCS, vol. 73, pp. 64\u201378 (2011)","key":"3_CR41","DOI":"10.4204\/EPTCS.73.8"},{"key":"3_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/978-3-642-04368-0_17","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"M Kwiatkowska","year":"2009","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Stochastic games for verification of probabilistic timed automata. In: Ouaknine, J., Vaandrager, F.W. (eds.) FORMATS 2009. LNCS, vol. 5813, pp. 212\u2013227. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04368-0_17"},{"key":"3_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). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"issue":"1","key":"3_CR44","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/s10703-006-0005-2","volume":"29","author":"MZ Kwiatkowska","year":"2006","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D., Sproston, J.: Performance analysis of probabilistic timed automata using digital clocks. Formal Methods Syst. Des. 29(1), 33\u201378 (2006). https:\/\/doi.org\/10.1007\/s10703-006-0005-2","journal-title":"Formal Methods Syst. Des."},{"issue":"1","key":"3_CR45","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). https:\/\/doi.org\/10.1016\/S0304-3975(01)00046-9","journal-title":"Theor. Comput. Sci."},{"issue":"7","key":"3_CR46","doi-asserted-by":"publisher","first-page":"1027","DOI":"10.1016\/j.ic.2007.01.004","volume":"205","author":"MZ Kwiatkowska","year":"2007","unstructured":"Kwiatkowska, M.Z., Norman, G., Sproston, J., Wang, F.: Symbolic model checking for probabilistic timed automata. Inf. Comput. 205(7), 1027\u20131077 (2007)","journal-title":"Inf. Comput."},{"key":"3_CR47","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"},{"unstructured":"Markowitch, O., Roggeman, Y.: Probabilistic non-repudiation without trusted third party. In: Proceedings 2nd Workshop on Security in Communication Networks (1999)","key":"3_CR48"},{"issue":"2","key":"3_CR49","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/s10703-012-0177-x","volume":"43","author":"G Norman","year":"2013","unstructured":"Norman, G., Parker, D., Sproston, J.: Model checking for probabilistic timed automata. Formal Methods Syst. Des. 43(2), 164\u2013190 (2013)","journal-title":"Formal Methods Syst. Des."},{"key":"3_CR50","series-title":"Wiley Series in Probability and Mathematical Statistics: Applied Probability and Statistics","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 Series in Probability and Mathematical Statistics: Applied Probability and Statistics, John Wiley & Sons Inc., New York (1994)"},{"key":"3_CR51","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, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_4"},{"key":"3_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"620","DOI":"10.1007\/978-3-642-04081-8_41","volume-title":"CONCUR 2009 - Concurrency Theory","author":"J Sproston","year":"2009","unstructured":"Sproston, J.: Strict divergence for probabilistic timed automata. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 620\u2013636. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04081-8_41"},{"issue":"1\u20132","key":"3_CR53","doi-asserted-by":"publisher","first-page":"101","DOI":"10.3233\/FI-2021-2000","volume":"178","author":"J Sproston","year":"2021","unstructured":"Sproston, J.: Probabilistic timed automata with clock-dependent probabilities. Fundam. Informaticae 178(1\u20132), 101\u2013138 (2021)","journal-title":"Fundam. Informaticae"},{"key":"3_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-48778-6_4","volume-title":"Formal Methods for Real-Time and Probabilistic Systems","author":"M Stoelinga","year":"1999","unstructured":"Stoelinga, M., Vaandrager, F.: Root contention in IEEE 1394. In: Katoen, J.-P. (ed.) ARTS 1999. LNCS, vol. 1601, pp. 53\u201374. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48778-6_4"}],"container-title":["Lecture Notes in Computer Science","Quantitative Evaluation of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-85172-9_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,21]],"date-time":"2021-10-21T18:10:01Z","timestamp":1634839801000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-85172-9_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030851712","9783030851729"],"references-count":54,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-85172-9_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"19 August 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"QEST","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Quantitative Evaluation of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 August 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 August 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"qest2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.qest.org\/","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 (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"47","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"21","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"45% - 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 (provided by the conference organizers)"}},{"value":"3.5","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5-6","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"1 keynote paper is also included.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}