{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:58:19Z","timestamp":1776333499986,"version":"3.51.2"},"publisher-location":"Cham","reference-count":46,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030309411","type":"print"},{"value":"9783030309428","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-30942-8_19","type":"book-chapter","created":{"date-parts":[[2019,9,22]],"date-time":"2019-09-22T23:03:06Z","timestamp":1569193386000},"page":"298-315","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":18,"title":["Equilibria-Based Probabilistic Model Checking for Concurrent Stochastic Games"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9022-7599","authenticated-orcid":false,"given":"Marta","family":"Kwiatkowska","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9326-4344","authenticated-orcid":false,"given":"Gethin","family":"Norman","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4137-8862","authenticated-orcid":false,"given":"David","family":"Parker","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6570-9737","authenticated-orcid":false,"given":"Gabriel","family":"Santos","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,9,23]]},"reference":[{"key":"19_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/3-540-48320-9_7","volume-title":"CONCUR\u201999 Concurrency Theory","author":"L de Alfaro","year":"1999","unstructured":"de Alfaro, L.: Computing minimum and maximum reachability times in probabilistic systems. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 66\u201381. Springer, Heidelberg (1999). \nhttps:\/\/doi.org\/10.1007\/3-540-48320-9_7"},{"issue":"3","key":"19_CR2","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1016\/j.tcs.2007.07.008","volume":"386","author":"L de Alfaro","year":"2007","unstructured":"de Alfaro, L., Henzinger, T., Kupferman, O.: Concurrent reachability games. Theor. Comput. Sci. 386(3), 188\u2013217 (2007)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"19_CR3","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1016\/j.jcss.2003.07.009","volume":"68","author":"L de Alfaro","year":"2004","unstructured":"de Alfaro, L., Majumdar, R.: Quantitative solution of omega-regular games. J. Comput. Syst. Sci. 68(2), 374\u2013397 (2004)","journal-title":"J. Comput. Syst. Sci."},{"issue":"5","key":"19_CR4","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1145\/585265.585270","volume":"49","author":"R Alur","year":"2002","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672\u2013713 (2002)","journal-title":"J. ACM"},{"key":"19_CR5","doi-asserted-by":"crossref","unstructured":"Arslan, G., Y\u00fcksel, S.: Distributionally consistent price taking equilibria in stochastic dynamic games. In: Proceedings of CDC 2017, pp. 4594\u20134599. IEEE (2017)","DOI":"10.1109\/CDC.2017.8264338"},{"issue":"3","key":"19_CR6","doi-asserted-by":"publisher","first-page":"536","DOI":"10.1016\/j.ic.2017.09.010","volume":"261","author":"N Basset","year":"2018","unstructured":"Basset, N., Kwiatkowska, M., Wiltsche, C.: Compositional strategy synthesis for stochastic games with multiple objectives. Inf. Comput. 261(3), 536\u2013587 (2018)","journal-title":"Inf. Comput."},{"key":"19_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1007\/3-540-60692-0_70","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"A Bianco","year":"1995","unstructured":"Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, pp. 499\u2013513. Springer, Heidelberg (1995). \nhttps:\/\/doi.org\/10.1007\/3-540-60692-0_70"},{"key":"19_CR8","unstructured":"Bouyer, P., Markey, N., Stan, D.: Mixed Nash equilibria in concurrent games. In: Proceedings of FSTTCS 2014, LIPICS, vol. 29, pp. 351\u2013363. Leibniz-Zentrum f\u00fcr Informatik (2014)"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"Bouyer, P., Markey, N., Stan, D.: Stochastic equilibria under imprecise deviations in terminal-reward concurrent games. In: Proceedings of GandALF 2016, EPTCS, vol. 226, pp. 61\u201375. Open Publishing Association (2016)","DOI":"10.4204\/EPTCS.226.5"},{"key":"19_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"890","DOI":"10.1007\/978-3-642-39799-8_63","volume-title":"Computer Aided Verification","author":"R Brenguier","year":"2013","unstructured":"Brenguier, R.: PRALINE: a tool for computing nash equilibria in concurrent games. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 890\u2013895. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-39799-8_63"},{"key":"19_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"525","DOI":"10.1007\/978-3-319-08867-9_34","volume-title":"Computer Aided Verification","author":"P \u010cerm\u00e1k","year":"2014","unstructured":"\u010cerm\u00e1k, P., Lomuscio, A., Mogavero, F., Murano, A.: MCMAS-SLK: a model checker for the verification of strategy logic specifications. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 525\u2013532. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-08867-9_34"},{"key":"19_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/11874683_18","volume-title":"Computer Science Logic","author":"K Chatterjee","year":"2006","unstructured":"Chatterjee, K.: Nash equilibrium for upward-closed objectives. In: \u00c9sik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 271\u2013286. Springer, Heidelberg (2006). \nhttps:\/\/doi.org\/10.1007\/11874683_18"},{"key":"19_CR13","unstructured":"Chatterjee, K.: Stochastic $$\\omega $$-regular games. Ph.D. thesis, University of California at Berkeley (2007)"},{"issue":"5","key":"19_CR14","doi-asserted-by":"publisher","first-page":"640","DOI":"10.1016\/j.jcss.2012.12.001","volume":"79","author":"K Chatterjee","year":"2013","unstructured":"Chatterjee, K., de Alfaro, L., Henzinger, T.: Strategy improvement for concurrent reachability and turn-based stochastic safety games. J. Comput. Syst. Sci. 79(5), 640\u2013657 (2013)","journal-title":"J. Comput. Syst. Sci."},{"key":"19_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-540-69850-0_7","volume-title":"25 Years of Model Checking","author":"K Chatterjee","year":"2008","unstructured":"Chatterjee, K., Henzinger, T.A.: Value iteration. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 107\u2013138. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-69850-0_7"},{"key":"19_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/978-3-540-30124-0_6","volume-title":"Computer Science Logic","author":"K Chatterjee","year":"2004","unstructured":"Chatterjee, K., Majumdar, R., Jurdzi\u0144ski, M.: On Nash equilibria in stochastic games. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 26\u201340. Springer, Heidelberg (2004). \nhttps:\/\/doi.org\/10.1007\/978-3-540-30124-0_6"},{"issue":"1","key":"19_CR17","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/s10703-013-0183-7","volume":"43","author":"T Chen","year":"2013","unstructured":"Chen, T., Forejt, V., Kwiatkowska, M., Parker, D., Simaitis, A.: Automatic verification of competitive stochastic systems. Formal Methods Syst. Des. 43(1), 61\u201392 (2013)","journal-title":"Formal Methods Syst. Des."},{"key":"19_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/978-3-642-40313-2_25","volume-title":"Mathematical Foundations of Computer Science 2013","author":"T Chen","year":"2013","unstructured":"Chen, T., Forejt, V., Kwiatkowska, M., Simaitis, A., Wiltsche, C.: On stochastic games with multiple objectives. In: Chatterjee, K., Sgall, J. (eds.) MFCS 2013. LNCS, vol. 8087, pp. 266\u2013277. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-40313-2_25"},{"key":"19_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"19_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"592","DOI":"10.1007\/978-3-319-63390-9_31","volume-title":"Computer Aided Verification","author":"C Dehnert","year":"2017","unstructured":"Dehnert, C., Junges, S., Katoen, J.-P., Volk, M.: A Storm is coming: a modern probabilistic model checker. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 592\u2013600. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-63390-9_31"},{"key":"19_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1007\/978-3-030-02450-5_7","volume-title":"Formal Methods and Software Engineering","author":"D Fernando","year":"2018","unstructured":"Fernando, D., Dong, N., Jegourel, C., Dong, J.S.: Verification of strong Nash-equilibrium for probabilistic BAR systems. In: Sun, J., Sun, M. (eds.) ICFEM 2018. LNCS, vol. 11232, pp. 106\u2013123. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-030-02450-5_7"},{"key":"19_CR22","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1016\/j.tcs.2016.12.003","volume":"735","author":"S Haddad","year":"2018","unstructured":"Haddad, S., Monmege, B.: Interval iteration algorithm for MDPs and IMDPs. Theor. Comput. Sci. 735, 111\u2013131 (2018)","journal-title":"Theor. Comput. Sci."},{"issue":"5","key":"19_CR23","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects Comput. 6(5), 512\u2013535 (1994)","journal-title":"Formal Aspects Comput."},{"key":"19_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"551","DOI":"10.1007\/978-3-030-01090-4_35","volume-title":"Automated Technology for Verification and Analysis","author":"J Gutierrez","year":"2018","unstructured":"Gutierrez, J., Najib, M., Perelli, G., Wooldridge, M.: EVE: a tool for temporal equilibrium analysis. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 551\u2013557. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-030-01090-4_35"},{"key":"19_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"623","DOI":"10.1007\/978-3-319-96145-3_36","volume-title":"Computer Aided Verification","author":"E Kelmendi","year":"2018","unstructured":"Kelmendi, E., Kr\u00e4mer, J., K\u0159et\u00ednsk\u00fd, J., Weininger, M.: Value iteration for simple stochastic games: stopping criterion and learning algorithm. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 623\u2013642. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-96145-3_36"},{"key":"19_CR26","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-9455-6","volume-title":"Denumerable Markov Chains","author":"J Kemeny","year":"1976","unstructured":"Kemeny, J., Snell, J., Knapp, A.: Denumerable Markov Chains. Springer, New York (1976). \nhttps:\/\/doi.org\/10.1007\/978-1-4684-9455-6"},{"key":"19_CR27","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). \nhttps:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"key":"19_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-319-99154-2_14","volume-title":"Quantitative Evaluation of Systems","author":"M Kwiatkowska","year":"2018","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: Automated verification of concurrent stochastic games. In: McIver, A., Horvath, A. (eds.) QEST 2018. LNCS, vol. 11024, pp. 223\u2013239. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-99154-2_14"},{"key":"19_CR29","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: Equilibria-based probabilistic model checking for concurrent stochastic games (2018). \nhttp:\/\/arxiv.org\/abs\/1811.07145"},{"key":"19_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-319-02444-8_2","volume-title":"Automated Technology for Verification and Analysis","author":"M Kwiatkowska","year":"2013","unstructured":"Kwiatkowska, M., Parker, D.: Automated verification and strategy synthesis for probabilistic systems. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 5\u201322. Springer, Cham (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-319-02444-8_2"},{"issue":"2","key":"19_CR31","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/s10009-017-0476-z","volume":"20","author":"M Kwiatkowska","year":"2018","unstructured":"Kwiatkowska, M., Parker, D., Wiltsche, C.: PRISM-games: verification and strategy synthesis for stochastic multi-player games with multiple objectives. Softw. Tools Technol. Transf. 20(2), 195\u2013210 (2018)","journal-title":"Softw. Tools Technol. Transf."},{"issue":"2","key":"19_CR32","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1137\/0112033","volume":"12","author":"C Lemke","year":"1964","unstructured":"Lemke, C., Howson Jr., J.: Equilibrium points of bimatrix games. J. Soc. Ind. Appl. Math. 12(2), 413\u2013423 (1964)","journal-title":"J. Soc. Ind. Appl. Math."},{"key":"19_CR33","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/978-3-319-67504-6_24","volume-title":"Algorithmic Decision Theory","author":"D Lozovanu","year":"2017","unstructured":"Lozovanu, D., Pickl, S.: Determining Nash equilibria for stochastic positional games with discounted payoffs. In: Rothe, J. (ed.) ADT 2017. LNCS (LNAI), vol. 10576, pp. 339\u2013343. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-67504-6_24"},{"key":"19_CR34","unstructured":"McKelvey, R., McLennan, A., Turocy, T.: Gambit: software tools for game theory, version 16.0.1 (2016). \ngambit-project.org"},{"key":"19_CR35","volume-title":"Theory of Games and Economic Behavior","author":"J von Neumann","year":"1944","unstructured":"von Neumann, J., Morgenstern, O., Kuhn, H., Rubinstein, A.: Theory of Games and Economic Behavior. Princeton University Press, Princeton (1944)"},{"key":"19_CR36","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511800481","volume-title":"Algorithmic Game Theory","author":"N Nisan","year":"2007","unstructured":"Nisan, N., Roughgarden, T., Tardos, E., Vazirani, V.: Algorithmic Game Theory. Cambridge University Press, Cambridge (2007)"},{"key":"19_CR37","volume-title":"An Introduction to Game Theory","author":"M Osborne","year":"2004","unstructured":"Osborne, M., Rubinstein, A.: An Introduction to Game Theory. Oxford University Press, Oxford (2004)"},{"key":"19_CR38","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-3-0348-0122-5_7","volume-title":"The Mathematics of Darwin\u2019s Legacy","author":"J Pacheco","year":"2011","unstructured":"Pacheco, J., Santos, F., Souza, M., Skyrms, B.: Evolutionary dynamics of collective action. In: Chalub, F., Rodrigues, J. (eds.) The Mathematics of Darwin\u2019s Legacy, pp. 119\u2013138. Springer, Basel (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-0348-0122-5_7"},{"key":"19_CR39","unstructured":"Porter, R., Nudelman, E., Shoham, Y.: Simple search methods for finding a Nash equilibrium. In: Proceedings of AAAI 2004, pp. 664\u2013669. AAAI Press (2004)"},{"key":"19_CR40","unstructured":"Prasad, H., Prashanth, L., Bhatnagar, S.: Two-timescale algorithms for learning Nash equilibria in general-sum stochastic games. In: Proceedings of AAMAS 2015, pp. 1371\u20131379. IFAAMAS (2015)"},{"key":"19_CR41","unstructured":"Sandholm, T., Gilpin, A., Conitzer, V.: Mixed-integer programming methods for finding Nash equilibria. In: Proceedings of AAAI 2005, pp. 495\u2013501. AAAI Press (2005)"},{"issue":"1","key":"19_CR42","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1006\/game.2000.0794","volume":"34","author":"U Schwalbe","year":"2001","unstructured":"Schwalbe, U., Walker, P.: Zermelo and the early history of game theory. Games Econ. Behav. 34(1), 123\u2013137 (2001)","journal-title":"Games Econ. Behav."},{"key":"19_CR43","series-title":"Mathematical Programming Studies","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/BFb0121248","volume-title":"Pivoting and Extension","author":"L Shapley","year":"1974","unstructured":"Shapley, L.: A note on the Lemke-Howson algorithm. In: Balinski, M.L. (ed.) Pivoting and Extension. Mathematical Programming Studies, vol. 1, pp. 175\u2013189. Springer, Heidelberg (1974). In Honor of A.W. Tucker"},{"key":"19_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1007\/978-3-319-25150-9_34","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2015","author":"A Toumi","year":"2015","unstructured":"Toumi, A., Gutierrez, J., Wooldridge, M.: A tool for the automated verification of nash equilibria in concurrent games. In: Leucker, M., Rueda, C., Valencia, F.D. (eds.) ICTAC 2015. LNCS, vol. 9399, pp. 583\u2013594. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-25150-9_34"},{"key":"19_CR45","doi-asserted-by":"crossref","unstructured":"Ummels, M.: Stochastic multiplayer games: theory and algorithms. Ph.D. thesis, RWTH Aachen University (2010)","DOI":"10.5117\/9789085550402"},{"key":"19_CR46","unstructured":"Supporting material. \nprismmodelchecker.org\/files\/fm19nash\/"}],"container-title":["Lecture Notes in Computer Science","Formal Methods \u2013 The Next 30 Years"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-30942-8_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,5]],"date-time":"2020-05-05T06:07:58Z","timestamp":1588658878000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-30942-8_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030309411","9783030309428"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-30942-8_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"23 September 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Porto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 October 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 October 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/formalmethods2019.inesctec.pt\/","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":"129","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":"44","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":"7","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":"34% - 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":"4","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,5","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":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}