{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,11,19]],"date-time":"2024-11-19T18:42:30Z","timestamp":1732041750111},"publisher-location":"Cham","reference-count":67,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031131875"},{"type":"electronic","value":"9783031131882"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,8,6]],"date-time":"2022-08-06T00:00:00Z","timestamp":1659744000000},"content-version":"vor","delay-in-days":217,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,8,6]],"date-time":"2022-08-06T00:00:00Z","timestamp":1659744000000},"content-version":"vor","delay-in-days":217,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"Abstract<\/jats:title>Mo<\/jats:sc>Gym<\/jats:sc>, is an integrated toolbox enabling the training and verification of machine-learned decision-making agents based on formal models, for the purpose of sound use in the real world. Given a formal representation of a decision-making problem in the JANI format and a reach-avoid objective, Mo<\/jats:sc>Gym<\/jats:sc>(a) enables training a decision-making agent with respect to that objective directly on the model using reinforcement learning (RL) techniques, and (b) it supports rigorous assessment of the quality of the induced decision-making agent by means of deep statistical model checking (DSMC). Mo<\/jats:sc>Gym<\/jats:sc>implements the standard interface for training environments established by OpenAI Gym, thereby connecting to the vast body of existing work in the RL community. In return, it makes accessible the large set of existing JANI model checking benchmarks to machine learning research. It thereby contributes an efficient feedback mechanism for improving in particular reinforcement learning algorithms. The connective part is implemented on top of Momba. For the DSMC quality assurance of the learned decision-making agents, a variant of the statistical model checkermodes<\/jats:sc>of the Modest<\/jats:sc>Toolset<\/jats:sc>is leveraged, which has been extended by two new resolution strategies for non-determinism when encountered during statistical evaluation.<\/jats:p>","DOI":"10.1007\/978-3-031-13188-2_21","type":"book-chapter","created":{"date-parts":[[2022,8,5]],"date-time":"2022-08-05T08:16:57Z","timestamp":1659687417000},"page":"430-443","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["MoGym: Using Formal Models for Training and Verifying Decision-making Agents"],"prefix":"10.1007","author":[{"ORCID":"http:\/\/orcid.org\/0000-0002-1100-1952","authenticated-orcid":false,"given":"Timo P.","family":"Gros","sequence":"first","affiliation":[]},{"ORCID":"http:\/\/orcid.org\/0000-0002-2766-9615","authenticated-orcid":false,"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[]},{"ORCID":"http:\/\/orcid.org\/0000-0003-1590-5876","authenticated-orcid":false,"given":"J\u00f6rg","family":"Hoffmann","sequence":"additional","affiliation":[]},{"ORCID":"http:\/\/orcid.org\/0000-0002-6353-227X","authenticated-orcid":false,"given":"Michaela","family":"Klauck","sequence":"additional","affiliation":[]},{"ORCID":"http:\/\/orcid.org\/0000-0003-2551-2814","authenticated-orcid":false,"given":"Maximilian A.","family":"K\u00f6hl","sequence":"additional","affiliation":[]},{"ORCID":"http:\/\/orcid.org\/0000-0001-8460-6007","authenticated-orcid":false,"given":"Verena","family":"Wolf","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,8,6]]},"reference":[{"key":"21_CR1","doi-asserted-by":"crossref","unstructured":"Agostinelli, F., McAleer, S., Shmakov, A., Baldi, P.: Solving the Rubik\u2019s Cube with Deep Reinforcement Learning and Search. Nature M. Intel. pp. 356\u2013363 (2019)","DOI":"10.1038\/s42256-019-0070-z"},{"key":"21_CR2","doi-asserted-by":"crossref","unstructured":"Baier, C., Christakis, M., Gros, T.P., Gro\u00df, D., Gumhold, S., Hermanns, H., Hoffmann, J., Klauck, M.: Lab conditions for research on explainable automated decisions. In: TAILOR 2020. pp. 83\u201390 (2020)","DOI":"10.1007\/978-3-030-73959-1_8"},{"key":"21_CR3","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2019.103216","volume":"280","author":"N Bard","year":"2020","unstructured":"Bard, N., et al.: The hanabi challenge: A new frontier for ai research. Artificial Intelligence 280, 103216 (2020)","journal-title":"Artificial Intelligence"},{"issue":"1","key":"21_CR4","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1016\/0004-3702(94)00011-O","volume":"72","author":"AG Barto","year":"1995","unstructured":"Barto, A.G., Bradtke, S.J., Singh, S.P.: Learning to act using real-time dynamic programming. Artificial Intelligence 72(1), 81\u2013138 (1995)","journal-title":"Artificial Intelligence"},{"key":"21_CR5","doi-asserted-by":"crossref","unstructured":"Basu, A., Bensalem, S., Bozga, M., Caillaud, B., Delahaye, B., Legay, A.: Statistical Abstraction and Model-Checking of Large Heterogeneous Systems. In: FORTE 2010. vol.\u00a06117, pp. 32\u201346. Springer (2010)","DOI":"10.1007\/978-3-642-13464-7_4"},{"key":"21_CR6","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1613\/jair.3912","volume":"47","author":"MG Bellemare","year":"2013","unstructured":"Bellemare, M.G., Naddaf, Y., Veness, J., Bowling, M.: The arcade learning environment: An evaluation platform for general agents. JAIR 47, 253\u2013279 (2013)","journal-title":"JAIR"},{"key":"21_CR7","doi-asserted-by":"crossref","unstructured":"Bogdoll, J., Fioriti, L.M.F., Hartmanns, A., Hermanns, H.: Partial order methods for statistical model checking and simulation. In: FORTE 2011. vol.\u00a06722, pp. 59\u201374. Springer (2011)","DOI":"10.1007\/978-3-642-21461-5_4"},{"key":"21_CR8","doi-asserted-by":"crossref","unstructured":"Bogdoll, J., Hartmanns, A., Hermanns, H.: Simulation and Statistical Model Checking for Modestly Nondeterministic Models. In: GI\/ITG Conf. Measurement, Modelling, and Eval. Comp. Sys. Depend. Fault Tol. pp. 249\u2013252. Springer (2012)","DOI":"10.1007\/978-3-642-28540-0_20"},{"key":"21_CR9","unstructured":"Bonet, B., Geffner, H.: Labeled RTDP: improving the convergence of real-time dynamic programming. In: ICAPS. pp. 12\u201321 (2003)"},{"key":"21_CR10","unstructured":"Bonet, B., Givan, B.: Non-Deterministic Planning Track of the 2006 IPC. http:\/\/idm-lab.org\/wiki\/icaps\/ipc2006\/probabilistic\/ (2006), acc. Oct., 13, 2021"},{"key":"21_CR11","unstructured":"Brockman, G., Cheung, V., Pettersson, L., Schneider, J., Schulman, J., Tang, J., Zaremba, W.: Openai gym. CoRR abs\/1606.01540 (2016)"},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"Browne, C.B., et\u00a0al.: A survey of monte carlo tree search methods. IEEE Trans. Comp. Intel. and AI in Games 4(1), 1\u201343 (2012)","DOI":"10.1109\/TCIAIG.2012.2186810"},{"key":"21_CR13","doi-asserted-by":"crossref","unstructured":"Budde, C.E., D\u2019Argenio, P.R., Hartmanns, A., Sedwards, S.: A statistical model checker for nondeterminism and rare events. In: TACAS. pp. 340\u2013358 (2018)","DOI":"10.1007\/978-3-319-89963-3_20"},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"Budde, C.E., Dehnert, C., Hahn, E.M., Hartmanns, A., Junges, S., Turrini, A.: JANI: Quantitative model and tool interaction. In: TACAS. pp. 151\u2013168 (2017)","DOI":"10.1007\/978-3-662-54580-5_9"},{"key":"21_CR15","doi-asserted-by":"crossref","unstructured":"C\u00f4t\u00e9, M.A., et\u00a0al.: Textworld: A learning environment for text-based games. In: Workshop on Computer Games. pp. 41\u201375. Springer (2018)","DOI":"10.1007\/978-3-030-24337-1_3"},{"key":"21_CR16","unstructured":"Doshi-Velez, F., Kim, B.: Towards a rigorous science of interpretable machine learning. arXiv preprint arXiv:1702.08608 (2017)"},{"key":"21_CR17","unstructured":"Dulac-Arnold, G., et\u00a0al.: Deep reinforcement learning in large discrete action spaces. arXiv preprint arXiv:1512.07679 (2015)"},{"key":"21_CR18","unstructured":"Fan, L., Zhu, Y., Zhu, J., Liu, Z., Zeng, O., Gupta, A., Creus-Costa, J., Savarese, S., Fei-Fei, L.: Surreal: Open-source reinforcement learning framework and robot manipulation benchmark. In: Conf. Robot Learning. pp. 767\u2013782. PMLR (2018)"},{"key":"21_CR19","doi-asserted-by":"crossref","unstructured":"Gros, T.P., Gro\u00df, D., Gumhold, S., Hoffmann, J., Klauck, M., Steinmetz, M.: TraceVis: Towards Visualization for Deep Statistical Model Checking. In: Int. Symp. Leveraging Applications of Formal Methods, Verification and Validation (2020)","DOI":"10.1007\/978-3-030-83723-5_3"},{"key":"21_CR20","doi-asserted-by":"crossref","unstructured":"Gros, T.P., Hermanns, H., Hoffmann, J., Klauck, M., Steinmetz, M.: Deep statistical model checking. In: FORTE 2020. pp. 96\u2013114 (2020)","DOI":"10.1007\/978-3-030-50086-3_6"},{"key":"21_CR21","doi-asserted-by":"crossref","unstructured":"Gros, T.P., H\u00f6ller, D., Hoffmann, J., Klauck, M., Meerkamp, H., Wolf, V.: DSMC evaluation stages: Fostering robust and safe behavior in deep reinforcement learning. In: QEST. pp. 197\u2013216 (2021)","DOI":"10.1007\/978-3-030-85172-9_11"},{"key":"21_CR22","doi-asserted-by":"crossref","unstructured":"Gros, T.P., H\u00f6ller, D., Hoffmann, J., Wolf, V.: Tracking the race between deep reinforcement learning and imitation learning. In: QEST 2020. vol. 12289, pp. 11\u201317. Springer (2020)","DOI":"10.1007\/978-3-030-59854-9_2"},{"key":"21_CR23","doi-asserted-by":"crossref","unstructured":"Gu, S., Holly, E., Lillicrap, T., Levine, S.: Deep Reinforcement Learning for Robotic Manipulation with Asynchronous Off-policy Updates. In: 2017 IEEE Int. Conf. robotics and automation (ICRA). pp. 3389\u20133396. IEEE (2017)","DOI":"10.1109\/ICRA.2017.7989385"},{"key":"21_CR24","unstructured":"Guo, X., Singh, S., Lee, H., Lewis, R.L., Wang, X.: Deep learning for real-time atari game play using offline monte-carlo tree search planning. In: Advances in neural information processing systems. pp. 3338\u20133346 (2014)"},{"key":"21_CR25","unstructured":"Gustafsson, N., et\u00a0al.: TorchSharp. https:\/\/github.com\/dotnet\/TorchSharp (2021), accessed on Sept., 22, 2021"},{"key":"21_CR26","unstructured":"Haarnoja, T., Zhou, A., Abbeel, P., Levine, S.: Soft actor-critic: Off-policy maximum entropy deep reinforcement learning with a stochastic actor. In: Int. conf. ML. pp. 1861\u20131870. PMLR (2018)"},{"key":"21_CR27","doi-asserted-by":"crossref","unstructured":"Hahn, E.M., Hartmanns, A.: A comparison of time- and reward-bounded probabilistic model checking techniques. In: SETTA 2016. pp. 85\u2013100 (2016)","DOI":"10.1007\/978-3-319-47677-3_6"},{"issue":"2","key":"21_CR28","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.: A compositional modelling and analysis framework for stochastic hybrid systems. Formal Methods Syst. Des. 43(2), 191\u2013232 (2013)","journal-title":"Formal Methods Syst. Des."},{"key":"21_CR29","doi-asserted-by":"crossref","unstructured":"Hahn, E.M., Li, Y., Schewe, S., Turrini, A., Zhang, L.: iscasmc: A web-based probabilistic model checker. In: FM 2014. pp. 312\u2013317 (2014)","DOI":"10.1007\/978-3-319-06410-9_22"},{"key":"21_CR30","doi-asserted-by":"crossref","unstructured":"Hartmanns, A., Hermanns, H.: The Modest Toolset: An integrated environment for quantitative modelling and verification. In: TACAS 2014. pp. 593\u2013598 (2014)","DOI":"10.1007\/978-3-642-54862-8_51"},{"key":"21_CR31","doi-asserted-by":"crossref","unstructured":"Hartmanns, A., Klauck, M., Parker, D., Quatmann, T., Ruijters, E.: The Quantitative Verification Benchmark Set. In: TACAS 2019. pp. 344\u2013350 (2019)","DOI":"10.1007\/978-3-030-17462-0_20"},{"key":"21_CR32","doi-asserted-by":"crossref","unstructured":"Hartmanns, A., Timmer, M.: On-the-Fly Confluence Detection for Statistical Model Checking. In: NFM 2013","DOI":"10.1007\/978-3-642-38088-4_23"},{"key":"21_CR33","doi-asserted-by":"crossref","unstructured":"Hensel, C., Junges, S., Katoen, J.P., Quatmann, T., Volk, M.: The probabilistic model checker storm. Int. Jour. on Software Tools for Technology Transfer (2021)","DOI":"10.1007\/s10009-021-00633-z"},{"key":"21_CR34","doi-asserted-by":"crossref","unstructured":"H\u00e9rault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: VMCAI 2004. vol.\u00a02937, pp. 73\u201384. Springer (2004)","DOI":"10.1007\/978-3-540-24622-0_8"},{"key":"21_CR35","first-page":"4565","volume":"29","author":"J Ho","year":"2016","unstructured":"Ho, J., Ermon, S.: Generative adversarial imitation learning. Advances in neural information processing systems 29, 4565\u20134573 (2016)","journal-title":"Advances in neural information processing systems"},{"key":"21_CR36","doi-asserted-by":"crossref","unstructured":"Hoffmann, J., Hermanns, H., Klauck, M., Steinmetz, M., Karpas, E., Magazzeni, D.: Let\u2019s learn their language? A case for planning with automata-network languages from model checking. In: AAAI 2020. pp. 13569\u201313575 (2020)","DOI":"10.1609\/aaai.v34i09.7083"},{"key":"21_CR37","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1613\/jair.1.11595","volume":"68","author":"M Klauck","year":"2020","unstructured":"Klauck, M., Steinmetz, M., Hoffmann, J., Hermanns, H.: Bridging the gap between probabilistic model checking and probabilistic planning: Survey, compilations, and empirical comparison. J. Artif. Intell. Res. 68, 247\u2013310 (2020)","journal-title":"J. Artif. Intell. Res."},{"key":"21_CR38","unstructured":"Koehler, J., Schuster, K.: Elevator control as a planning problem. In: 5. Int. Conf. Art. Intel. Planning Sys. pp. 331\u2013338. AAAI (2000)"},{"key":"21_CR39","doi-asserted-by":"crossref","unstructured":"K\u00f6hl, M.A., Klauck, M., Hermanns, H.: Momba: JANI meets python. In: TACAS. pp. 389\u2013398 (2021)","DOI":"10.1007\/978-3-030-72013-1_23"},{"key":"21_CR40","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: Stochastic model checking. In: SFM 2007, Advanced Lectures. pp. 220\u2013270. LNCS 4486 (2007)","DOI":"10.1007\/978-3-540-72522-0_6"},{"key":"21_CR41","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: 23. CAV 2011. pp. 585\u2013591 (2011)","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"21_CR42","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: The PRISM benchmark suite. In: 9. QEST 2012. pp. 203\u2013204 (2012)","DOI":"10.1109\/QEST.2012.14"},{"issue":"3","key":"21_CR43","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/s001650300007","volume":"14","author":"MZ Kwiatkowska","year":"2003","unstructured":"Kwiatkowska, M.Z., Norman, G., Sproston, J.: Probabilistic model checking of deadline properties in the IEEE 1394 firewire root contention protocol. Formal Aspects Comput. 14(3), 295\u2013318 (2003)","journal-title":"Formal Aspects Comput."},{"key":"21_CR44","doi-asserted-by":"crossref","unstructured":"Legay, A., Delahaye, B., Bensalem, S.: Statistical Model Checking: An Overview. In: Runtime Verification - 1. RV 2010. vol.\u00a06418, pp. 122\u2013135. Springer (2010)","DOI":"10.1007\/978-3-642-16612-9_11"},{"key":"21_CR45","doi-asserted-by":"crossref","unstructured":"Liessner, R., Schmitt, J., Dietermann, A., B\u00e4ker, B.: Hyperparameter optimization for deep reinforcement learning in vehicle energy management. In: ICAART (2). pp. 134\u2013144 (2019)","DOI":"10.5220\/0007364701340144"},{"key":"21_CR46","unstructured":"McMahan, H.B., Gordon, G.J.: Fast exact planning in Markov decision processes. In: ICAPS. pp. 151\u2013160 (2005)"},{"key":"21_CR47","doi-asserted-by":"publisher","first-page":"529","DOI":"10.1038\/nature14236","volume":"518","author":"V Mnih","year":"2015","unstructured":"Mnih, V., et al.: Human-level Control through Deep Reinforcement Learning. Nature 518, 529\u2013533 (2015)","journal-title":"Nature"},{"key":"21_CR48","unstructured":"Mnih, V., et\u00a0al.: Asynchronous methods for deep reinforcement learning. In: Int. conf. machine learning. pp. 1928\u20131937. PMLR (2016)"},{"key":"21_CR49","unstructured":"Nazari, M., Oroojlooy, A., Snyder, L., Takac, M.: Reinforcement learning for solving the vehicle routing problem. In: Advances in Neural Inf. Proc. Sys. 31, pp. 9839\u20139849. Curran Associates, Inc. (2018)"},{"key":"21_CR50","doi-asserted-by":"crossref","unstructured":"Pathak, D., Agrawal, P., Efros, A.A., Darrell, T.: Curiosity-driven exploration by self-supervised prediction. In: Int. conf. ML. pp. 2778\u20132787. PMLR (2017)","DOI":"10.1109\/CVPRW.2017.70"},{"key":"21_CR51","unstructured":"Pineda, L.E., Lu, Y., Zilberstein, S., Goldman, C.V.: Fault-tolerant planning under uncertainty. In: IJCAI. pp. 2350\u20132356 (2013)"},{"key":"21_CR52","doi-asserted-by":"crossref","unstructured":"Pineda, L.E., Zilberstein, S.: Planning under uncertainty using reduced models: Revisiting determinization. In: ICAPS 2014 (2014)","DOI":"10.1609\/icaps.v24i1.13636"},{"key":"21_CR53","doi-asserted-by":"crossref","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley (1994)","DOI":"10.1002\/9780470316887"},{"issue":"19","key":"21_CR54","doi-asserted-by":"publisher","first-page":"70","DOI":"10.2352\/ISSN.2470-1173.2017.19.AVM-023","volume":"2017","author":"AE Sallab","year":"2017","unstructured":"Sallab, A.E., Abdou, M., Perot, E., Yogamani, S.: Deep Reinforcement Learning Framework for Autonomous Driving. Electronic Imaging 2017(19), 70\u201376 (2017)","journal-title":"Electronic Imaging"},{"key":"21_CR55","unstructured":"Schulman, J., Wolski, F., Dhariwal, P., Radford, A., Klimov, O.: Proximal policy optimization algorithms. arXiv preprint arXiv:1707.06347 (2017)"},{"key":"21_CR56","doi-asserted-by":"crossref","unstructured":"Sen, K., Viswanathan, M., Agha, G.: On Statistical Model Checking of Stochastic Systems. In: CAV. pp. 266\u2013280 (2005)","DOI":"10.1007\/11513988_26"},{"issue":"7676","key":"21_CR57","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1038\/nature24270","volume":"550","author":"D Silver","year":"2017","unstructured":"Silver, D., et al.: Mastering the Game of Go Without Human Knowledge. Nature 550(7676), 354\u2013359 (2017)","journal-title":"Nature"},{"issue":"6419","key":"21_CR58","doi-asserted-by":"publisher","first-page":"1140","DOI":"10.1126\/science.aar6404","volume":"362","author":"D Silver","year":"2018","unstructured":"Silver, D., et al.: A General Reinforcement Learning Algorithm That Masters Chess, Shogi, and Go Through Self-play. Science 362(6419), 1140\u20131144 (2018)","journal-title":"Science"},{"key":"21_CR59","doi-asserted-by":"crossref","unstructured":"Stoelinga, M., Vaandrager, F.W.: Root contention in IEEE 1394. In: 5. AMAST Workshop, ARTS\u201999. vol.\u00a01601, pp. 53\u201374. Springer (1999)","DOI":"10.1007\/3-540-48778-6_4"},{"key":"21_CR60","unstructured":"Sutton, R.S., Barto, A.G.: Reinforcement Learning: An Introduction. Adaptive computation and machine learning, The MIT Press, second edn. (2018)"},{"key":"21_CR61","unstructured":"Verma, A., Murali, V., Singh, R., Kohli, P., Chaudhuri, S.: Programmatically interpretable reinforcement learning. In: Int. Conf. on ML. PMLR (2018)"},{"key":"21_CR62","doi-asserted-by":"publisher","first-page":"1264","DOI":"10.1016\/j.procir.2018.03.212","volume":"72","author":"B Waschneck","year":"2018","unstructured":"Waschneck, B., Reichstaller, A., Belzner, L., Altenm\u00fcller, T., Bauernhansl, T., Knapp, A., Kyek, A.: Optimization of global production scheduling with deep reinforcement learning. Procedia Cirp 72, 1264\u20131269 (2018)","journal-title":"Procedia Cirp"},{"key":"21_CR63","doi-asserted-by":"crossref","unstructured":"Xia, F., Zamir, A.R., He, Z., Sax, A., Malik, J., Savarese, S.: Gibson env: Real-world perception for embodied agents. In: IEEE Conf. Computer Vision and Pattern Recognition. pp. 9068\u20139079 (2018)","DOI":"10.1109\/CVPR.2018.00945"},{"key":"21_CR64","doi-asserted-by":"crossref","unstructured":"Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: CAV 2002. vol.\u00a02404, pp. 223\u2013235. Springer (2002)","DOI":"10.1007\/3-540-45657-0_17"},{"key":"21_CR65","doi-asserted-by":"crossref","unstructured":"Younes, H.L., Kwiatkowska, M., Norman, G., Parker, D.: Numerical vs. Statistical Probabilistic Model Checking: An Empirical Study. In: TACAS. pp. 46\u201360. Springer (2004)","DOI":"10.1007\/978-3-540-24730-2_4"},{"key":"21_CR66","unstructured":"Yu, T., Quillen, D., He, Z., Julian, R., Hausman, K., Finn, C., Levine, S.: Meta-world: A benchmark and evaluation for multi-task and meta reinforcement learning. In: Conf. Robot Learning. pp. 1094\u20131100. PMLR (2020)"},{"issue":"2","key":"21_CR67","first-page":"338","volume":"43","author":"P Zuliani","year":"2013","unstructured":"Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to Stateflow\/Simulink verification. FM Sys. Des. 43(2), 338\u2013367 (2013)","journal-title":"FM Sys. Des."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-13188-2_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,13]],"date-time":"2023-02-13T19:26:34Z","timestamp":1676316394000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-13188-2_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031131875","9783031131882"],"references-count":67,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-13188-2_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"6 August 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Haifa","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Israel","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 August 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 August 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2022\/","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":"209","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":"40","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":"11","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":"19% - 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.9","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":"9.7","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)"}}]}}