{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:13:06Z","timestamp":1784837586352,"version":"3.55.0"},"publisher-location":"Cham","reference-count":52,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031572487","type":"print"},{"value":"9783031572494","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T00:00:00Z","timestamp":1712275200000},"content-version":"vor","delay-in-days":95,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Labeled continuous-time Markov chains (CTMCs) describe processes subject to random timing and partial observability. In applications such as runtime monitoring, we must incorporate past observations. The timing of these observations matters but may be uncertain. Thus, we consider a setting in which we are given a sequence of imprecisely timed labels called the evidence. The problem is to compute reachability probabilities, which we condition on this evidence. Our key contribution is a method that solves this problem by unfolding the CTMC states over all possible timings for the evidence. We formalize this unfolding as a Markov decision process (MDP) in which each timing for the evidence is reflected by a scheduler. This MDP has infinitely many states and actions in general, making a direct analysis infeasible. Thus, we abstract the continuous MDP into a finite interval MDP (iMDP) and develop an iterative refinement scheme to upper-bound conditional probabilities in the CTMC. We show the feasibility of our method on several numerical benchmarks and discuss key challenges to further enhance the performance.<\/jats:p>","DOI":"10.1007\/978-3-031-57249-4_13","type":"book-chapter","created":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T07:02:35Z","timestamp":1712214155000},"page":"258-278","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["CTMCs with Imprecisely Timed Observations"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5235-1967","authenticated-orcid":false,"given":"Thom","family":"Badings","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3810-4185","authenticated-orcid":false,"given":"Matthias","family":"Volk","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0978-8466","authenticated-orcid":false,"given":"Sebastian","family":"Junges","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6793-8165","authenticated-orcid":false,"given":"Marielle","family":"Stoelinga","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1318-8973","authenticated-orcid":false,"given":"Nils","family":"Jansen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,4,5]]},"reference":[{"key":"13_CR1","doi-asserted-by":"publisher","unstructured":"Amparore, E.G., Donatelli, S.: MC4CSLTA: an efficient model checking tool for CSLTA. In: QEST. pp. 153\u2013154. IEEE Computer Society (2010). https:\/\/doi.org\/10.1109\/QEST.2010.26","DOI":"10.1109\/QEST.2010.26"},{"key":"13_CR2","doi-asserted-by":"publisher","unstructured":"Amparore, E.G., Donatelli, S.: Efficient model checking of the stochastic logic CSL$${{}^{\\text{TA}}}$$. Perform. Evaluation 123-124, 1\u201334 (2018). https:\/\/doi.org\/10.1016\/j.peva.2018.03.002","DOI":"10.1016\/j.peva.2018.03.002"},{"key":"13_CR3","doi-asserted-by":"publisher","unstructured":"Andriushchenko, R., Ceska, M., Junges, S., Katoen, J.P., Stupinsk\u00fd, S.: PAYNT: A tool for inductive synthesis of probabilistic programs. In: CAV (1). LNCS, vol. 12759, pp. 856\u2013869. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_40","DOI":"10.1007\/978-3-030-81685-8_40"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Model-checking continuous-time Markov chains. ACM Transactions on Computational Logic 1(1), 162\u2013170 (2000)","DOI":"10.1145\/343369.343402"},{"key":"13_CR5","doi-asserted-by":"publisher","unstructured":"Badings, T.S., Jansen, N., Junges, S., Stoelinga, M., Volk, M.: Sampling-based verification of CTMCs with uncertain rates. In: CAV (2). LNCS, vol. 13372, pp. 26\u201347. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_2","DOI":"10.1007\/978-3-031-13188-2_2"},{"key":"13_CR6","doi-asserted-by":"publisher","unstructured":"Badings, T.S., Romao, L., Abate, A., Jansen, N.: Probabilities are not enough: Formal controller synthesis for stochastic dynamical models with epistemic uncertainty. In: AAAI. pp. 14701\u201314710. AAAI Press (2023). https:\/\/doi.org\/10.1609\/aaai.v37i12.26718","DOI":"10.1609\/aaai.v37i12.26718"},{"key":"13_CR7","doi-asserted-by":"publisher","unstructured":"Badings, T.S., Romao, L., Abate, A., Parker, D., Poonawala, H.A., Stoelinga, M., Jansen, N.: Robust control for dynamical systems with non-Gaussian noise via formal abstractions. J. Artif. Intell. Res. 76, 341\u2013391 (2023). https:\/\/doi.org\/10.1613\/jair.1.14253","DOI":"10.1613\/jair.1.14253"},{"key":"13_CR8","doi-asserted-by":"publisher","unstructured":"Badings, T.S., Volk, M., Junges, S., Stoelinga, M., Jansen, N.: CTMCs with imprecisely timed observations. Tech. rep., CoRR, abs\/2401.06574 (2024). https:\/\/doi.org\/10.48550\/arXiv.2401.06574","DOI":"10.48550\/arXiv.2401.06574"},{"key":"13_CR9","doi-asserted-by":"publisher","unstructured":"Baier, C., Dubslaff, C., Korenciak, L., Kucera, A., Reh\u00e1k, V.: Mean-payoff optimization in continuous-time Markov chains with parametric alarms. ACM Trans. Model. Comput. Simul. 29(4), 28:1\u201328:26 (2019). https:\/\/doi.org\/10.1145\/3310225","DOI":"10.1145\/3310225"},{"key":"13_CR10","doi-asserted-by":"publisher","unstructured":"Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.P.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Software Eng. 29(6), 524\u2013541 (2003). https:\/\/doi.org\/10.1109\/TSE.2003.1205180","DOI":"10.1109\/TSE.2003.1205180"},{"key":"13_CR11","unstructured":"Baier, C., Katoen, J.P.: Principles of model checking. MIT Press (2008)"},{"key":"13_CR12","doi-asserted-by":"publisher","unstructured":"Baier, C., Klein, J., Kl\u00fcppelholz, S., M\u00e4rcker, S.: Computing conditional probabilities in Markovian models efficiently. In: TACAS. LNCS, vol.\u00a08413, pp. 515\u2013530. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_43","DOI":"10.1007\/978-3-642-54862-8_43"},{"key":"13_CR13","doi-asserted-by":"publisher","unstructured":"Bartocci, E., Deshmukh, J.V., Donz\u00e9, A., Fainekos, G., Maler, O., Nickovic, D., Sankaranarayanan, S.: Specification-based monitoring of cyber-physical systems: A survey on theory, tools and applications. In: Lectures on Runtime Verification, LNCS, vol. 10457, pp. 135\u2013175. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-75632-5_5","DOI":"10.1007\/978-3-319-75632-5_5"},{"key":"13_CR14","doi-asserted-by":"publisher","unstructured":"Bortolussi, L., Silvetti, S.: Bayesian statistical parameter synthesis for linear temporal properties of stochastic models. In: TACAS (2). LNCS, vol. 10806, pp. 396\u2013413. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_23","DOI":"10.1007\/978-3-319-89963-3_23"},{"key":"13_CR15","doi-asserted-by":"publisher","unstructured":"Br\u00e1zdil, T., Korenciak, L., Krc\u00e1l, J., Novotn\u00fd, P., Reh\u00e1k, V.: Optimizing performance of continuous-time stochastic systems using timeout synthesis. In: QEST. LNCS, vol.\u00a09259, pp. 141\u2013159. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-22264-6_10","DOI":"10.1007\/978-3-319-22264-6_10"},{"key":"13_CR16","doi-asserted-by":"publisher","unstructured":"Calinescu, R., Ceska, M., Gerasimou, S., Kwiatkowska, M., Paoletti, N.: Efficient synthesis of robust models for stochastic systems. J. Syst. Softw. 143, 140\u2013158 (2018). https:\/\/doi.org\/10.1016\/j.jss.2018.05.013","DOI":"10.1016\/j.jss.2018.05.013"},{"key":"13_CR17","doi-asserted-by":"publisher","unstructured":"Cardelli, L., Grosu, R., Larsen, K.G., Tribastone, M., Tschaikowski, M., Vandin, A.: Lumpability for uncertain continuous-time Markov chains. In: QEST. LNCS, vol. 12846, pp. 391\u2013409. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-85172-9_21","DOI":"10.1007\/978-3-030-85172-9_21"},{"key":"13_CR18","doi-asserted-by":"publisher","unstructured":"Cardelli, L., Grosu, R., Larsen, K.G., Tribastone, M., Tschaikowski, M., Vandin, A.: Algorithmic minimization of uncertain continuous-time Markov chains. IEEE Transactions on Automatic Control pp. 1\u201316 (2023). https:\/\/doi.org\/10.1109\/TAC.2023.3244093","DOI":"10.1109\/TAC.2023.3244093"},{"key":"13_CR19","doi-asserted-by":"publisher","unstructured":"Cauchi, N., Abate, A.: $$\\sf StocHy$$: Automated verification and synthesis of stochastic processes. In: TACAS (2). LNCS, vol. 11428, pp. 247\u2013264. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-17465-1_14","DOI":"10.1007\/978-3-030-17465-1_14"},{"key":"13_CR20","doi-asserted-by":"publisher","unstructured":"Ceska, M., Dannenberg, F., Paoletti, N., Kwiatkowska, M., Brim, L.: Precise parameter synthesis for stochastic biochemical systems. Acta Informatica 54(6), 589\u2013623 (2017). https:\/\/doi.org\/10.1007\/s00236-016-0265-2","DOI":"10.1007\/s00236-016-0265-2"},{"key":"13_CR21","doi-asserted-by":"publisher","unstructured":"Ceska, M., Jansen, N., Junges, S., Katoen, J.P.: Shepherding hordes of Markov chains. In: TACAS (2). LNCS, vol. 11428, pp. 172\u2013190. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-17465-1_10","DOI":"10.1007\/978-3-030-17465-1_10"},{"key":"13_CR22","doi-asserted-by":"publisher","unstructured":"Chen, T., Han, T., Katoen, J.P., Mereacre, A.: Model checking of continuous-time Markov chains against timed automata specifications. Log. Methods Comput. Sci. 7(1) (2011). https:\/\/doi.org\/10.2168\/LMCS-7(1:12)2011","DOI":"10.2168\/LMCS-7(1:12)2011"},{"key":"13_CR23","doi-asserted-by":"publisher","unstructured":"Feng, Y., Katoen, J.P., Li, H., Xia, B., Zhan, N.: Monitoring CTMCs by multi-clock timed automata. In: CAV (1). LNCS, vol. 10981, pp. 507\u2013526. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_27","DOI":"10.1007\/978-3-319-96145-3_27"},{"key":"13_CR24","doi-asserted-by":"publisher","unstructured":"Gales, M.J.F., Young, S.J.: The application of hidden Markov models in speech recognition. Found. Trends Signal Process. 1(3), 195\u2013304 (2007). https:\/\/doi.org\/10.1561\/2000000004","DOI":"10.1561\/2000000004"},{"key":"13_CR25","doi-asserted-by":"publisher","unstructured":"Gao, Y., Hahn, E.M., Zhan, N., Zhang, L.: CCMC: A conditional CSL model checker for continuous-time Markov chains. In: ATVA. LNCS, vol.\u00a08172, pp. 464\u2013468. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-319-02444-8_36","DOI":"10.1007\/978-3-319-02444-8_36"},{"key":"13_CR26","doi-asserted-by":"publisher","unstructured":"Gao, Y., Xu, M., Zhan, N., Zhang, L.: Model checking conditional CSL for continuous-time Markov chains. Inf. Process. Lett. 113(1-2), 44\u201350 (2013). https:\/\/doi.org\/10.1016\/j.ipl.2012.09.009","DOI":"10.1016\/j.ipl.2012.09.009"},{"key":"13_CR27","doi-asserted-by":"publisher","unstructured":"Givan, R., Leach, S.M., Dean, T.L.: Bounded-parameter Markov decision processes. Artif. Intell. 122(1-2), 71\u2013109 (2000). https:\/\/doi.org\/10.1016\/S0004-3702(00)00047-3","DOI":"10.1016\/S0004-3702(00)00047-3"},{"key":"13_CR28","doi-asserted-by":"publisher","unstructured":"Guan, J., Yu, N.: A probabilistic logic for verifying continuous-time Markov chains. In: TACAS (2). LNCS, vol. 13244, pp. 3\u201321. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_1","DOI":"10.1007\/978-3-030-99527-0_1"},{"key":"13_CR29","doi-asserted-by":"publisher","unstructured":"Hahn, E.M., Hermanns, H., Wachter, B., Zhang, L.: PASS: abstraction refinement for infinite probabilistic models. In: TACAS. LNCS, vol.\u00a06015, pp. 353\u2013357. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-12002-2_30","DOI":"10.1007\/978-3-642-12002-2_30"},{"key":"13_CR30","doi-asserted-by":"publisher","unstructured":"Hahn, E.M., Norman, G., Parker, D., Wachter, B., Zhang, L.: Game-based abstraction and controller synthesis for probabilistic hybrid systems. In: QEST. pp. 69\u201378. IEEE Computer Society (2011). https:\/\/doi.org\/10.1109\/QEST.2011.17","DOI":"10.1109\/QEST.2011.17"},{"key":"13_CR31","doi-asserted-by":"publisher","unstructured":"Han, T., Katoen, J.P., Mereacre, A.: Approximate parameter synthesis for probabilistic time-bounded reachability. In: RTSS. pp. 173\u2013182. IEEE Computer Society (2008). https:\/\/doi.org\/10.1109\/RTSS.2008.19","DOI":"10.1109\/RTSS.2008.19"},{"key":"13_CR32","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Junges, S., Quatmann, T., Weininger, M.: A practitioner\u2019s guide to MDP model checking algorithms. In: TACAS (1). LNCS, vol. 13993, pp. 469\u2013488. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_24","DOI":"10.1007\/978-3-031-30823-9_24"},{"key":"13_CR33","doi-asserted-by":"publisher","unstructured":"Haverkort, B.R., Hermanns, H., Katoen, J.P.: On the use of model checking techniques for dependability evaluation. In: SRDS. pp. 228\u2013237. IEEE Computer Society (2000). https:\/\/doi.org\/10.1109\/RELDI.2000.885410","DOI":"10.1109\/RELDI.2000.885410"},{"key":"13_CR34","doi-asserted-by":"publisher","unstructured":"Hensel, C., Junges, S., Katoen, J.P., Quatmann, T., Volk, M.: The probabilistic model checker Storm. Int. J. Softw. Tools Technol. Transf. 24(4), 589\u2013610 (2022). https:\/\/doi.org\/10.1007\/s10009-021-00633-z","DOI":"10.1007\/s10009-021-00633-z"},{"key":"13_CR35","unstructured":"Hermanns, H., Meyer-Kayser, J., Siegle, M.: Multi terminal binary decision diagrams to represent and analyse continuous time Markov chains. In: 3rd Int. Workshop on the Numerical Solution of Markov Chains. pp. 188\u2013207. Citeseer (1999)"},{"key":"13_CR36","doi-asserted-by":"crossref","unstructured":"Hobolth, A., Stone, E.A.: Simulation from endpoint-conditioned, continuous-time Markov chains on a finite state space, with applications to molecular evolution. The annals of applied statistics 3(3), \u00a01204 (2009)","DOI":"10.1214\/09-AOAS247"},{"key":"13_CR37","doi-asserted-by":"publisher","unstructured":"Iyengar, G.N.: Robust dynamic programming. Math. Oper. Res. 30(2), 257\u2013280 (2005). https:\/\/doi.org\/10.1287\/moor.1040.0129","DOI":"10.1287\/moor.1040.0129"},{"key":"13_CR38","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","DOI":"10.1109\/LICS.1991.151651"},{"key":"13_CR39","doi-asserted-by":"publisher","unstructured":"Junges, S., Torfah, H., Seshia, S.A.: Runtime monitors for Markov decision processes. In: CAV (2). LNCS, vol. 12760, pp. 553\u2013576. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_26","DOI":"10.1007\/978-3-030-81688-9_26"},{"key":"13_CR40","doi-asserted-by":"publisher","unstructured":"Katoen, J.P.: The probabilistic model checking landscape. In: LICS. pp. 31\u201345. ACM (2016). https:\/\/doi.org\/10.1145\/2933575.2934574","DOI":"10.1145\/2933575.2934574"},{"key":"13_CR41","doi-asserted-by":"publisher","unstructured":"Kattenbelt, M., Kwiatkowska, M.Z., Norman, G., Parker, D.: A game-based abstraction-refinement framework for Markov decision processes. Formal Methods Syst. Des. 36(3), 246\u2013280 (2010). https:\/\/doi.org\/10.1007\/s10703-010-0097-6","DOI":"10.1007\/s10703-010-0097-6"},{"key":"13_CR42","doi-asserted-by":"publisher","unstructured":"Korenciak, L., Kucera, A., Reh\u00e1k, V.: Efficient timeout synthesis in fixed-delay CTMC using policy iteration. In: MASCOTS. pp. 367\u2013372. IEEE Computer Society (2016). https:\/\/doi.org\/10.1109\/MASCOTS.2016.34","DOI":"10.1109\/MASCOTS.2016.34"},{"key":"13_CR43","doi-asserted-by":"publisher","unstructured":"Lavaei, A., Soudjani, S., Abate, A., Zamani, M.: Automated verification and synthesis of stochastic hybrid systems: A survey. Autom. 146, 110617 (2022). https:\/\/doi.org\/10.1016\/j.automatica.2022.110617","DOI":"10.1016\/j.automatica.2022.110617"},{"key":"13_CR44","doi-asserted-by":"publisher","unstructured":"Nilim, A., Ghaoui, L.E.: Robust control of Markov decision processes with uncertain transition matrices. Oper. Res. 53(5), 780\u2013798 (2005). https:\/\/doi.org\/10.1287\/opre.1050.0216","DOI":"10.1287\/opre.1050.0216"},{"key":"13_CR45","unstructured":"Perkins, T.J.: Maximum likelihood trajectories for continuous-time Markov chains. In: NIPS. pp. 1437\u20131445. Curran Associates, Inc. (2009)"},{"key":"13_CR46","doi-asserted-by":"publisher","unstructured":"Puggelli, A., Li, W., Sangiovanni-Vincentelli, A.L., Seshia, S.A.: Polynomial-time verification of PCTL properties of MDPs with convex uncertainties. In: CAV. LNCS, vol.\u00a08044, pp. 527\u2013542. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_35","DOI":"10.1007\/978-3-642-39799-8_35"},{"key":"13_CR47","doi-asserted-by":"publisher","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley Series in Probability and Statistics, Wiley (1994). https:\/\/doi.org\/10.1002\/9780470316887","DOI":"10.1002\/9780470316887"},{"key":"13_CR48","doi-asserted-by":"publisher","unstructured":"Ruijters, E., Stoelinga, M.: Fault tree analysis: A survey of the state-of-the-art in modeling, analysis and tools. Comput. Sci. Rev. 15, 29\u201362 (2015). https:\/\/doi.org\/10.1016\/j.cosrev.2015.03.001","DOI":"10.1016\/j.cosrev.2015.03.001"},{"key":"13_CR49","doi-asserted-by":"publisher","unstructured":"S\u00e1nchez, C., Schneider, G., Ahrendt, W., Bartocci, E., Bianculli, D., Colombo, C., Falcone, Y., Francalanza, A., Krstic, S., Louren\u00e7o, J.M., Nickovic, D., Pace, G.J., Rufino, J., Signoles, J., Traytel, D., Weiss, A.: A survey of challenges for runtime verification from advanced application domains (beyond software). Formal Methods Syst. Des. 54(3), 279\u2013335 (2019). https:\/\/doi.org\/10.1007\/s10703-019-00337-w","DOI":"10.1007\/s10703-019-00337-w"},{"key":"13_CR50","doi-asserted-by":"publisher","unstructured":"Stoller, S.D., Bartocci, E., Seyster, J., Grosu, R., Havelund, K., Smolka, S.A., Zadok, E.: Runtime verification with state estimation. In: RV. LNCS, vol.\u00a07186, pp. 193\u2013207. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-29860-8_15","DOI":"10.1007\/978-3-642-29860-8_15"},{"key":"13_CR51","doi-asserted-by":"publisher","unstructured":"Winterer, L., Junges, S., Wimmer, R., Jansen, N., Topcu, U., Katoen, J.P., Becker, B.: Strategy synthesis for POMDPs in robot planning via game-based abstractions. IEEE Trans. Autom. Control. 66(3), 1040\u20131054 (2021). https:\/\/doi.org\/10.1109\/TAC.2020.2990140","DOI":"10.1109\/TAC.2020.2990140"},{"key":"13_CR52","doi-asserted-by":"publisher","unstructured":"Wolff, E.M., Topcu, U., Murray, R.M.: Robust control of uncertain Markov decision processes with temporal logic specifications. In: CDC. pp. 3372\u20133379. IEEE (2012). https:\/\/doi.org\/10.1109\/CDC.2012.6426174","DOI":"10.1109\/CDC.2012.6426174"}],"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-031-57249-4_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T07:08:12Z","timestamp":1712214492000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57249-4_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572487","9783031572494"],"references-count":52,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57249-4_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"5 April 2024","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":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2024\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-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":"159","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":"53","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":"16","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":"33% - 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","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":"10","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)"}}]}}