{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T03:24:43Z","timestamp":1777519483280,"version":"3.51.4"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2019,10,31]],"date-time":"2019-10-31T00:00:00Z","timestamp":1572480000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Model. Comput. Simul."],"published-print":{"date-parts":[[2019,10,31]]},"abstract":"<jats:p>\n            Continuous-time Markov chains with alarms (ACTMCs) allow for alarm events that can be non-exponentially distributed. Within\n            <jats:italic>parametric<\/jats:italic>\n            ACTMCs, the parameters of alarm-event distributions are not given explicitly and can be the subject of parameter synthesis. In this line, an algorithm is presented that solves the \u03b5-optimal parameter synthesis problem for parametric ACTMCs with long-run average optimization objectives. The approach provided in this article is based on a reduction of the problem to finding long-run average optimal policies in semi-Markov decision processes\u00a0(semi-MDPs) and sufficient discretization of the parameter (i.e., action) space. Since the set of actions in the discretized semi-MDP can be very large, a straightforward approach based on an explicit action-space construction fails to solve even simple instances of the problem. The presented algorithm uses an enhanced policy iteration on\n            <jats:italic>symbolic<\/jats:italic>\n            representations of the action space. Soundness of the algorithm is established for parametric ACTMCs with alarm-event distributions that satisfy four mild assumptions, fulfilled by many kinds of distributions. Exemplifying proofs for the satisfaction of these requirements are provided for Dirac, uniform, exponential, Erlang, and Weibull distributions in particular. An experimental implementation shows that the symbolic technique substantially improves the efficiency of the synthesis algorithm and allows us to solve instances of realistic size.\n          <\/jats:p>","DOI":"10.1145\/3310225","type":"journal-article","created":{"date-parts":[[2019,12,11]],"date-time":"2019-12-11T13:27:18Z","timestamp":1576070838000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Mean-payoff Optimization in Continuous-time Markov Chains with Parametric Alarms"],"prefix":"10.1145","volume":"29","author":[{"given":"Christel","family":"Baier","sequence":"first","affiliation":[{"name":"Faculty of Computer Science, TU Dresden, Dresden, Saxony, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5718-8276","authenticated-orcid":false,"given":"Clemens","family":"Dubslaff","sequence":"additional","affiliation":[{"name":"Faculty of Computer Science, TU Dresden, Dresden, Saxony, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"L'ubo\u0161","family":"Koren\u010diak","sequence":"additional","affiliation":[{"name":"Faculty of Informatics, Masaryk University, Brno, Czech Republic"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anton\u00edn","family":"ku\u010dera","sequence":"additional","affiliation":[{"name":"Faculty of Informatics, Masaryk University, Brno, Czech Republic"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vojt\u011bch","family":"\u0158eh\u00e1k","sequence":"additional","affiliation":[{"name":"Faculty of Informatics, Masaryk University, Brno, Czech Republic"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,12,10]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-0871-9"},{"key":"e_1_2_1_2_1","volume-title":"Proceedings of STOC. ACM Press","author":"Alur R.","unstructured":"R. Alur , T. A. Henzinger , and M. Y. Vardi . 1993. Parametric real-time reasoning . In Proceedings of STOC. ACM Press , New York, NY, 592--601. DOI:https:\/\/doi.org\/10.1145\/167088.167242 R. Alur, T. A. Henzinger, and M. Y. Vardi. 1993. Parametric real-time reasoning. In Proceedings of STOC. ACM Press, New York, NY, 592--601. DOI:https:\/\/doi.org\/10.1145\/167088.167242"},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of QEST (LNCS)","volume":"8657","author":"Amparore E. G.","unstructured":"E. G. Amparore , P. Buchholz , and S. Donatelli . 2014. A structured solution approach for Markov regenerative processes . In Proceedings of QEST (LNCS) , Vol. 8657 . Springer, Cham, 9--24. DOI:https:\/\/doi.org\/10.1007\/978-3-319-10696-0 E. G. Amparore, P. Buchholz, and S. Donatelli. 2014. A structured solution approach for Markov regenerative processes. In Proceedings of QEST (LNCS), Vol. 8657. Springer, Cham, 9--24. DOI:https:\/\/doi.org\/10.1007\/978-3-319-10696-0"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66335-7_12"},{"key":"e_1_2_1_5_1","doi-asserted-by":"crossref","unstructured":"C. Baier C. Dubslaff \u013d. Koren\u010diak A. Ku\u010dera and V. \u0158eh\u00e1k. 2017. Mean-payoff optimization in continuous-time Markov chains with parametric alarms. Retrieved from arxiv:cs.PF\/1706.06486.  C. Baier C. Dubslaff \u013d. Koren\u010diak A. Ku\u010dera and V. \u0158eh\u00e1k. 2017. Mean-payoff optimization in continuous-time Markov chains with parametric alarms. Retrieved from arxiv:cs.PF\/1706.06486.","DOI":"10.1007\/978-3-319-66335-7_12"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1093\/imanum\/8.1.141"},{"key":"e_1_2_1_7_1","unstructured":"L. Bernardin et al. 2012. Maple 16 Programming Guide. Maplesoft Waterloo.  L. Bernardin et al. 2012. Maple 16 Programming Guide. Maplesoft Waterloo."},{"key":"e_1_2_1_8_1","unstructured":"D. P. Bertsekas and R. G. Gallager. 1992. Data Networks (2nd ed.). Prentice-Hall Englewood Cliffs NJ.  D. P. Bertsekas and R. G. Gallager. 1992. Data Networks (2nd ed.). Prentice-Hall Englewood Cliffs NJ."},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of QEST (LNCS)","author":"Br\u00e1zdil T.","unstructured":"T. Br\u00e1zdil , \u013d. Koren\u010diak, J. Kr\u010d\u00e1l , P. Novotn\u00fd , and V. \u0158eh\u00e1k . 2015. Optimizing performance of continuous-time stochastic systems using timeout synthesis . In Proceedings of QEST (LNCS) , Vol. 9259 . Springer , Cham , 141--159. DOI:https:\/\/doi.org\/10.1007\/978-3-319-22264-6 T. Br\u00e1zdil, \u013d. Koren\u010diak, J. Kr\u010d\u00e1l, P. Novotn\u00fd, and V. \u0158eh\u00e1k. 2015. Optimizing performance of continuous-time stochastic systems using timeout synthesis. In Proceedings of QEST (LNCS), Vol. 9259. Springer, Cham, 141--159. DOI:https:\/\/doi.org\/10.1007\/978-3-319-22264-6"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23217-6_10"},{"key":"e_1_2_1_11_1","volume-title":"Proceedings of CDC","volume":"3","author":"Cao X.-R.","year":"2002","unstructured":"X.-R. Cao and H.-T. Fang . 2002 . Gradient-based policy iteration: An example . In Proceedings of CDC , Vol. 3 . IEEE, Piscataway, NJ, 3367--3371. DOI:https:\/\/doi.org\/10.1109\/CDC. 2002.1184395 X.-R. Cao and H.-T. Fang. 2002. Gradient-based policy iteration: An example. In Proceedings of CDC, Vol. 3. IEEE, Piscataway, NJ, 3367--3371. DOI:https:\/\/doi.org\/10.1109\/CDC.2002.1184395"},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of CMSB (LNCS)","volume":"8859","author":"\u010ce\u0161ka M.","unstructured":"M. \u010ce\u0161ka , F. Dannenberg , M. Kwiatkowska , and N. Paoletti . 2014. Precise parameter synthesis for stochastic biochemical systems . In Proceedings of CMSB (LNCS) , Vol. 8859 . Springer, Cham, 86--98. DOI:https:\/\/doi.org\/10.1007\/978-3-319-12982-2_7 M. \u010ce\u0161ka, F. Dannenberg, M. Kwiatkowska, and N. Paoletti. 2014. Precise parameter synthesis for stochastic biochemical systems. In Proceedings of CMSB (LNCS), Vol. 8859. Springer, Cham, 86--98. DOI:https:\/\/doi.org\/10.1007\/978-3-319-12982-2_7"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/0166-5316(94)90021-3"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055639"},{"key":"e_1_2_1_15_1","volume-title":"Proceedings of EMSOFT. ACM Press","author":"Diciolla M.","unstructured":"M. Diciolla , C. H. P. Kim , M. Kwiatkowska , and A. Mereacre . 2014. Synthesising optimal timing delays for timed I\/O automata . In Proceedings of EMSOFT. ACM Press , New York, NY. DOI:https:\/\/doi.org\/10.1145\/2656045.2656073 M. Diciolla, C. H. P. Kim, M. Kwiatkowska, and A. Mereacre. 2014. Synthesising optimal timing delays for timed I\/O automata. In Proceedings of EMSOFT. ACM Press, New York, NY. DOI:https:\/\/doi.org\/10.1145\/2656045.2656073"},{"key":"e_1_2_1_16_1","volume-title":"Modeling with Non-Markovian Stochastic Petri Nets","author":"German R.","unstructured":"R. German . 2000. Performance Analysis of Communication Systems , Modeling with Non-Markovian Stochastic Petri Nets . Wiley , Chichester . R. German. 2000. Performance Analysis of Communication Systems, Modeling with Non-Markovian Stochastic Petri Nets. Wiley, Chichester."},{"key":"e_1_2_1_17_1","volume-title":"Stability, Simulation","author":"Haas P. J.","unstructured":"P. J. Haas . 2002. Stochastic Petri Nets: Modelling , Stability, Simulation . Springer , New York, NY . P. J. Haas. 2002. Stochastic Petri Nets: Modelling, Stability, Simulation. Springer, New York, NY."},{"key":"e_1_2_1_18_1","volume-title":"Proceedings of CONCUR (LNCS)","volume":"5710","author":"Haase C.","unstructured":"C. Haase , S. Kreutzer , J. Ouaknine , and J. Worrell . 2009. Reachability in succinct and parametric one-counter automata . In Proceedings of CONCUR (LNCS) , Vol. 5710 . Springer, Heidelberg, 369--383. DOI:https:\/\/doi.org\/10.1007\/978-3-642-04081-8_25 C. Haase, S. Kreutzer, J. Ouaknine, and J. Worrell. 2009. Reachability in succinct and parametric one-counter automata. In Proceedings of CONCUR (LNCS), Vol. 5710. Springer, Heidelberg, 369--383. DOI:https:\/\/doi.org\/10.1007\/978-3-642-04081-8_25"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-010-0146-x"},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of RTSS. IEEE","author":"Han T.","year":"2008","unstructured":"T. Han , J.-P. Katoen , and A. Mereacre . 2008. Approximate parameter synthesis for probabilistic time-bounded reachability . In Proceedings of RTSS. IEEE , Piscataway, NJ, 173--182. DOI:https:\/\/doi.org\/10.1109\/RTSS. 2008 .19 T. Han, J.-P. Katoen, and A. Mereacre. 2008. Approximate parameter synthesis for probabilistic time-bounded reachability. In Proceedings of RTSS. IEEE, Piscataway, NJ, 173--182. DOI:https:\/\/doi.org\/10.1109\/RTSS.2008.19"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.01.012"},{"key":"e_1_2_1_22_1","volume-title":"Proceedings of RP (LNCS)","volume":"8762","author":"Jovanovi\u0107 A.","unstructured":"A. Jovanovi\u0107 and M. Kwiatkowska . 2014. Parameter synthesis for probabilistic timed automata using stochastic game abstractions . In Proceedings of RP (LNCS) , Vol. 8762 . Springer, Cham, 176--189. DOI:https:\/\/doi.org\/10.1007\/978-3-319-11439-2_14 A. Jovanovi\u0107 and M. Kwiatkowska. 2014. Parameter synthesis for probabilistic timed automata using stochastic game abstractions. In Proceedings of RP (LNCS), Vol. 8762. Springer, Cham, 176--189. DOI:https:\/\/doi.org\/10.1007\/978-3-319-11439-2_14"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2014.2357445"},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of MASCOTS. IEEE","author":"Ku\u010dera A.","year":"2016","unstructured":"\u013d. Koren\u010diak, A. Ku\u010dera , and V. \u0158eh\u00e1k . 2016 . Efficient timeout synthesis in fixed-delay CTMC using policy iteration . In Proceedings of MASCOTS. IEEE , Piscataway, NJ, 367--372. DOI:https:\/\/doi.org\/10.1109\/MASCOTS. 2016.34 \u013d. Koren\u010diak, A. Ku\u010dera, and V. \u0158eh\u00e1k. 2016. Efficient timeout synthesis in fixed-delay CTMC using policy iteration. In Proceedings of MASCOTS. IEEE, Piscataway, NJ, 367--372. DOI:https:\/\/doi.org\/10.1109\/MASCOTS.2016.34"},{"key":"e_1_2_1_25_1","volume-title":"Proceedings of iFM (LNCS)","volume":"9681","author":"\u0158eh\u00e1k V.","unstructured":"\u013d. Koren\u010diak, V. \u0158eh\u00e1k , and A. Farmadin . 2016. Extension of PRISM by synthesis of optimal timeouts in fixed-delay CTMC . In Proceedings of iFM (LNCS) , Vol. 9681 . Springer, Cham, 130--138. DOI:https:\/\/doi.org\/10.1007\/978-3-319-33693-0_9 \u013d. Koren\u010diak, V. \u0158eh\u00e1k, and A. Farmadin. 2016. Extension of PRISM by synthesis of optimal timeouts in fixed-delay CTMC. In Proceedings of iFM (LNCS), Vol. 9681. Springer, Cham, 130--138. DOI:https:\/\/doi.org\/10.1007\/978-3-319-33693-0_9"},{"key":"e_1_2_1_26_1","unstructured":"\u013d. Koren\u010diak. 2017.\n  Parameter Synthesis in Continuous-Time Stochastic Systems\n  . Ph.D. Dissertation. \n  Faculty of Informatics Masaryk University Brno.  \u013d. Koren\u010diak. 2017. Parameter Synthesis in Continuous-Time Stochastic Systems. Ph.D. Dissertation. Faculty of Informatics Masaryk University Brno."},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of CAV (LNCS)","volume":"6806","author":"Kwiatkowska M.","unstructured":"M. Kwiatkowska , G. Norman , and D. Parker . 2011. PRISM 4.0: Verification of probabilistic real-time systems . In Proceedings of CAV (LNCS) , Vol. 6806 . Springer, Heidelberg, 585--591. DOI:https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47 M. Kwiatkowska, G. Norman, and D. Parker. 2011. PRISM 4.0: Verification of probabilistic real-time systems. In Proceedings of CAV (LNCS), Vol. 6806. Springer, Heidelberg, 585--591. DOI:https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ejor.2010.12.014"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/0166-5316(93)90028-S"},{"key":"e_1_2_1_30_1","volume-title":"Simulation of Adaptive Behavior","author":"Littman M. L.","year":"1898","unstructured":"M. L. Littman . 1994. Memoryless policies: Theoretical limitations and practical results . In Simulation of Adaptive Behavior , Vol. 3 . MIT Press , Cambridge, MA , 238--245. Retrieved from http:\/\/dl.acm.org\/citation.cfm?id&equals; 1898 29.189893 M. L. Littman. 1994. Memoryless policies: Theoretical limitations and practical results. In Simulation of Adaptive Behavior, Vol. 3. MIT Press, Cambridge, MA, 238--245. Retrieved from http:\/\/dl.acm.org\/citation.cfm?id&equals;189829.189893"},{"key":"e_1_2_1_31_1","volume-title":"Proceedings of MASCOTS. IEEE","author":"Martina S.","year":"2016","unstructured":"S. Martina , M. Paolieri , T. Papini , and E. Vicario . 2016. Performance evaluation of Fischer\u2019s protocol through steady-state analysis of Markov regenerative processes . In Proceedings of MASCOTS. IEEE , Piscataway, NJ, 355--360. DOI:https:\/\/doi.org\/10.1109\/MASCOTS. 2016 .72 S. Martina, M. Paolieri, T. Papini, and E. Vicario. 2016. Performance evaluation of Fischer\u2019s protocol through steady-state analysis of Markov regenerative processes. In Proceedings of MASCOTS. IEEE, Piscataway, NJ, 355--360. DOI:https:\/\/doi.org\/10.1109\/MASCOTS.2016.72"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1080\/03610918.2011.615433"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1080\/00224065.1985.11978953"},{"key":"e_1_2_1_34_1","volume-title":"Cambridge University Press","author":"Norris J. R.","unstructured":"J. R. Norris . 1998. Markov Chains . Cambridge University Press , New York, NY . J. R. Norris. 1998. Markov Chains. Cambridge University Press, New York, NY."},{"key":"e_1_2_1_35_1","volume-title":"Markov Decision Processes","author":"Puterman M. L.","unstructured":"M. L. Puterman . 1994. Markov Decision Processes . Wiley , Hoboken, NJ . M. L. Puterman. 1994. Markov Decision Processes. Wiley, Hoboken, NJ."},{"key":"e_1_2_1_36_1","volume-title":"Proceedings of ISLPED. IEEE","author":"Qiu Q.","year":"1999","unstructured":"Q. Qiu , Q. Wu , and M. Pedram . 1999. Stochastic modeling of a power-managed system: Construction and optimization . In Proceedings of ISLPED. IEEE , New York, NY, 194--199. DOI:https:\/\/doi.org\/10.1109\/LPE. 1999 .799438 Q. Qiu, Q. Wu, and M. Pedram. 1999. Stochastic modeling of a power-managed system: Construction and optimization. In Proceedings of ISLPED. IEEE, New York, NY, 194--199. DOI:https:\/\/doi.org\/10.1109\/LPE.1999.799438"},{"key":"e_1_2_1_37_1","volume-title":"Proceedings of FORMATS (LNCS)","volume":"5215","author":"Traonouez L.-M.","unstructured":"L.-M. Traonouez , D. Lime , and O. H. Roux . 2008. Parametric model-checking of time Petri nets with stopwatches using the state-class graph . In Proceedings of FORMATS (LNCS) , Vol. 5215 . Springer, Heidelberg, 280--294. DOI:https:\/\/doi.org\/10.1007\/978-3-540-85778-5_20 L.-M. Traonouez, D. Lime, and O. H. Roux. 2008. Parametric model-checking of time Petri nets with stopwatches using the state-class graph. In Proceedings of FORMATS (LNCS), Vol. 5215. Springer, Heidelberg, 280--294. DOI:https:\/\/doi.org\/10.1007\/978-3-540-85778-5_20"},{"key":"e_1_2_1_38_1","first-page":"4","article-title":"A performance gradient perspective on gradient-based policy iteration and a modified value iteration","volume":"1","author":"Yang L.","year":"2008","unstructured":"L. Yang , J. Dankert , and J. Si . 2008 . A performance gradient perspective on gradient-based policy iteration and a modified value iteration . Int. J. Innovat. Creat. Change 1 , 4 (Oct. 2008), 509--520. DOI:https:\/\/doi.org\/10.1108\/17563780810919096 L. Yang, J. Dankert, and J. Si. 2008. A performance gradient perspective on gradient-based policy iteration and a modified value iteration. Int. J. Innovat. Creat. Change 1, 4 (Oct. 2008), 509--520. DOI:https:\/\/doi.org\/10.1108\/17563780810919096","journal-title":"Int. J. Innovat. Creat. Change"}],"container-title":["ACM Transactions on Modeling and Computer Simulation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3310225","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3310225","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:13:16Z","timestamp":1750212796000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3310225"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,31]]},"references-count":38,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2019,10,31]]}},"alternative-id":["10.1145\/3310225"],"URL":"https:\/\/doi.org\/10.1145\/3310225","relation":{},"ISSN":["1049-3301","1558-1195"],"issn-type":[{"value":"1049-3301","type":"print"},{"value":"1558-1195","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,10,31]]},"assertion":[{"value":"2018-01-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-12-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}