{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T01:37:00Z","timestamp":1742953020334,"version":"3.40.3"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319222639"},{"type":"electronic","value":"9783319222646"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-22264-6_10","type":"book-chapter","created":{"date-parts":[[2015,8,21]],"date-time":"2015-08-21T10:33:29Z","timestamp":1440153209000},"page":"141-159","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Optimizing Performance of Continuous-Time Stochastic Systems Using Timeout Synthesis"],"prefix":"10.1007","author":[{"given":"Tom\u00e1\u0161","family":"Br\u00e1zdil","sequence":"first","affiliation":[]},{"given":"\u013dubo\u0161","family":"Koren\u010diak","sequence":"additional","affiliation":[]},{"given":"Jan","family":"Kr\u010d\u00e1l","sequence":"additional","affiliation":[]},{"given":"Petr","family":"Novotn\u00fd","sequence":"additional","affiliation":[]},{"given":"Vojt\u011bch","family":"\u0158eh\u00e1k","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,8,22]]},"reference":[{"key":"10_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/3-540-54233-7_128","volume-title":"Automata, Languages and Programming","author":"R Alur","year":"1991","unstructured":"Alur, R., Courcoubetis, C., Dill, D.: Model-checking for probabilistic real-time systems. In: Albert, J.L., Monien, B., Artalejo, M.R. (eds.) Automata, Languages and Programming. LNCS, vol. 510, pp. 115\u2013136. Springer, Heidelberg (1991)"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: STOC, pp. 592\u2013601. ACM (1993)","DOI":"10.1145\/167088.167242"},{"issue":"1","key":"10_CR3","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/S0141-9331(97)00020-3","volume":"21","author":"NC Audsley","year":"1997","unstructured":"Audsley, N.C., Grigg, A.: Timing analysis of the ARINC 629 databus for real-time applications. Microprocess. Microsyst. 21(1), 55\u201361 (1997)","journal-title":"Microprocess. Microsyst."},{"key":"10_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-540-77050-3_15","volume-title":"FSTTCS 2007: Foundations of Software Technology and Theoretical Computer Science","author":"C Baier","year":"2007","unstructured":"Baier, C., Bertrand, N., Bouyer, P., Brihaye, T., Gr\u00f6\u00dfer, M.: Probabilistic and topological semantics for timed automata. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol. 4855, pp. 179\u2013191. Springer, Heidelberg (2007)"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Baier, C., Bertrand, N., Bouyer, P., Brihaye, T., Gr\u00f6\u00dfer, M.: Almost-sure model checking of infinite paths in one-clock timed automata. In: LICS, pp. 217\u2013226. IEEE (2008)","DOI":"10.1109\/LICS.2008.25"},{"key":"10_CR6","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1016\/j.ic.2013.01.001","volume":"224","author":"T Br\u00e1zdil","year":"2013","unstructured":"Br\u00e1zdil, T., Forejt, V., Kr\u010d\u00e1l, J., K\u0159et\u00ednsk\u00fd, J., Ku\u010dera, A.: Continuous-time stochastic games with time-bounded reachability. Inf. Comput. 224, 46\u201370 (2013)","journal-title":"Inf. Comput."},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"Br\u00e1zdil, T., Koren\u010diak, \u0139., Kr\u010d\u00e1l, J., Novotn\u00fd, P., \u0158eh\u00e1k, V.: Optimizing performance of continuous-time stochastic systems using timeout synthesis. CoRR, abs\/1407.4777 (2014)","DOI":"10.1007\/978-3-319-22264-6_10"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-642-15375-4_15","volume-title":"CONCUR 2010 - Concurrency Theory","author":"T Br\u00e1zdil","year":"2010","unstructured":"Br\u00e1zdil, T., Kr\u010d\u00e1l, J., K\u0159et\u00ednsk\u00fd, J., Ku\u010dera, A., \u0158eh\u00e1k, V.: Stochastic real-time games with qualitative timed automata objectives. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 207\u2013221. Springer, Heidelberg (2010)"},{"key":"10_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-23217-6_10","volume-title":"CONCUR 2011 \u2013 Concurrency Theory","author":"T Br\u00e1zdil","year":"2011","unstructured":"Br\u00e1zdil, T., Kr\u010d\u00e1l, J., K\u0159et\u00ednsk\u00fd, J., \u0158eh\u00e1k, V.: Fixed-delay events in generalized semi-Markov processes revisited. In: Katoen, J.-P., K\u00f6nig, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 140\u2013155. Springer, Heidelberg (2011)"},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-642-22110-1_19","volume-title":"Computer Aided Verification","author":"P Buchholz","year":"2011","unstructured":"Buchholz, P., Hahn, E.M., Hermanns, H., Zhang, L.: Model checking algorithms for CTMDPs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 225\u2013242. Springer, Heidelberg (2011)"},{"issue":"3","key":"10_CR11","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1109\/TSE.2012.42","volume":"39","author":"L Carnevali","year":"2013","unstructured":"Carnevali, L., Ridi, L., Vicario, E.: A quantitative approach to input generation in real-time testing of stochastic systems. IEEE Trans. Softw. Eng. 39(3), 292\u2013304 (2013)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"Chen, T., Han, T., Katoen, J.-P., Mereacre, A.: Quantitative model checking of continuous-time Markov chains against timed automata specifications. In: LICS, pp. 309\u2013318. IEEE (2009)","DOI":"10.1109\/LICS.2009.21"},{"key":"10_CR13","first-page":"166","volume-title":"Application and Theory of Petri Nets","author":"H Choi","year":"1993","unstructured":"Choi, H., Kulkarni, V.G., Trivedi, K.S.: Transient analysis of deterministic and stochastic Petri nets. In: Marsan, M.A. (ed.) Application and Theory of Petri Nets, vol. 691, pp. 166\u2013185. Springer, Heidelberg (1993)"},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"711","DOI":"10.1007\/978-3-540-70575-8_58","volume-title":"Automata, Languages and Programming","author":"K Etessami","year":"2008","unstructured":"Etessami, K., Wojtczak, D., Yannakakis, M.: Recursive stochastic games with positive rewards. In: Aceto, L., Damg\u00e5rd, I., Goldberg, L.A., Halld\u00f3rsson, M.M., Ing\u00f3lfsd\u00f3ttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part I. LNCS, vol. 5125, pp. 711\u2013723. Springer, Heidelberg (2008)"},{"key":"10_CR15","volume-title":"An Introduction to Probability Theory and Its Applications","author":"W Feller","year":"1968","unstructured":"Feller, W.: An Introduction to Probability Theory and Its Applications, vol. 1. Wiley, New York (1968)"},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-642-31424-7_24","volume-title":"Computer Aided Verification","author":"CC Guet","year":"2012","unstructured":"Guet, C.C., Gupta, A., Henzinger, T.A., Mateescu, M., Sezgin, A.: Delayed continuous-time Markov chains for genetic regulatory circuits. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 294\u2013309. Springer, Heidelberg (2012)"},{"key":"10_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/978-3-642-04081-8_25","volume-title":"CONCUR 2009 - Concurrency Theory","author":"C Haase","year":"2009","unstructured":"Haase, C., Kreutzer, S., Ouaknine, J., Worrell, J.: Reachability in succinct and parametric one-counter automata. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 369\u2013383. Springer, Heidelberg (2009)"},{"issue":"1","key":"10_CR18","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10009-010-0146-x","volume":"13","author":"EM Hahn","year":"2011","unstructured":"Hahn, E.M., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric Markov models. STTT 13(1), 3\u201319 (2011)","journal-title":"STTT"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"Han, T., Katoen, J.P., Mereacre, A.: Approximate parameter synthesis for probabilistic time-bounded reachability. In: Real-Time Systems Symposium, pp. 173\u2013182. IEEE (2008)","DOI":"10.1109\/RTSS.2008.19"},{"key":"10_CR20","unstructured":"Jensen, P.G., Taankvist, J.H.: Learning optimal scheduling for time uncertain settings. Aalborg University, Student project (2014)"},{"issue":"21","key":"10_CR21","doi-asserted-by":"publisher","first-page":"2162","DOI":"10.1016\/j.tcs.2011.01.012","volume":"412","author":"SK Jha","year":"2011","unstructured":"Jha, S.K., Langmead, C.J.: Synthesis and infeasibility analysis for stochastic models of biochemical systems using statistical model checking and abstraction refinement. TCS 412(21), 2162\u20132187 (2011)","journal-title":"TCS"},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"Khaksari, M., Fischione, C.: Performance analysis and optimization of the joining protocol for a platoon of vehicles. In: ISCCSP, pp. 1\u20136. IEEE (2012)","DOI":"10.1109\/ISCCSP.2012.6217873"},{"key":"10_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1007\/978-3-319-10885-8_9","volume-title":"Computer Performance Engineering","author":"\u0139 Koren\u010diak","year":"2014","unstructured":"Koren\u010diak, \u0139., Kr\u010d\u00e1l, J., \u0158eh\u00e1k, V.: Dealing with zero density using piecewise phase-type approximation. In: Horv\u00e1th, A., Wolter, K. (eds.) EPEW 2014. LNCS, vol. 8721, pp. 119\u2013134. Springer, Heidelberg (2014)"},{"key":"10_CR24","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/3-540-44618-4_11","volume-title":"CONCUR 2000","author":"M Kwiatkowska","year":"2000","unstructured":"Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Verifying quantitative properties of continuous probabilistic timed automata. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 123\u2013137. Springer, Heidelberg (2000)"},{"issue":"1","key":"10_CR25","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/0166-5316(93)90028-S","volume":"18","author":"C Lindemann","year":"1993","unstructured":"Lindemann, C.: An improved numerical algorithm for calculating steady-state solutions of deterministic and stochastic Petri net models. Perform. Eval. 18(1), 79\u201395 (1993)","journal-title":"Perform. Eval."},{"key":"10_CR26","first-page":"132","volume-title":"Advances in Petri Nets","author":"MA Marsan","year":"1987","unstructured":"Marsan, M.A., Chiola, G.: On Petri nets with deterministic and exponentially distributed firing times. In: Rozenberg, G. (ed.) Advances in Petri Nets, pp. 132\u2013145. Springer, Heidelberg (1987)"},{"key":"10_CR27","doi-asserted-by":"crossref","unstructured":"Neuh\u00e4usser, M.R., Zhang, L.: Time-bounded reachability probabilities in continuous-time Markov decision processes. In: QEST, pp. 209\u2013218. IEEE (2010)","DOI":"10.1109\/QEST.2010.47"},{"key":"10_CR28","volume-title":"Matrix-geometric Solutions in Stochastic Models: An Algorithmic Approach","author":"MF Neuts","year":"1981","unstructured":"Neuts, M.F.: Matrix-geometric Solutions in Stochastic Models: An Algorithmic Approach. Courier Dover Publications, Mineola (1981)"},{"key":"10_CR29","volume-title":"Markov Chains","author":"JR Norris","year":"1998","unstructured":"Norris, J.R.: Markov Chains. Cambridge University Press, Cambridge (1998)"},{"key":"10_CR30","volume-title":"Time-Triggered Communication","author":"R Obermaisser","year":"2011","unstructured":"Obermaisser, R.: Time-Triggered Communication. CRC Press, Boca Raton (2011)"},{"key":"10_CR31","doi-asserted-by":"publisher","DOI":"10.1002\/9780470316887","volume-title":"Markov Decision Processes","author":"ML Puterman","year":"1994","unstructured":"Puterman, M.L.: Markov Decision Processes. Wiley, Hoboken (1994)"},{"issue":"1","key":"10_CR32","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1109\/5.259426","volume":"82","author":"K Ramamritham","year":"1994","unstructured":"Ramamritham, K., Stankovic, J.A.: Scheduling algorithms and operating systems support for real-time systems. Proc. IEEE 82(1), 55\u201367 (1994)","journal-title":"Proc. IEEE"},{"key":"10_CR33","doi-asserted-by":"crossref","unstructured":"Tiassou, K.B.: Aircraft operational reliability - a model-based approach and case studies. Ph.D. thesis, Universi\u00e9 de Toulouse (2013)","DOI":"10.1016\/j.ress.2013.07.008"},{"key":"10_CR34","doi-asserted-by":"crossref","unstructured":"Wolovick, N., D\u2019Argenio, P.R., Qu, V: Optimizing probabilities of real-time test case execution. In: ICST, pp. 446\u2013455. IEEE (2009)","DOI":"10.1109\/ICST.2009.59"}],"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-319-22264-6_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,21]],"date-time":"2023-02-21T06:17:15Z","timestamp":1676960235000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-22264-6_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319222639","9783319222646"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-22264-6_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"22 August 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}