{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:50:47Z","timestamp":1740099047580,"version":"3.37.3"},"publisher-location":"Cham","reference-count":43,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319898834"},{"type":"electronic","value":"9783319898841"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-89884-1_20","type":"book-chapter","created":{"date-parts":[[2018,4,14]],"date-time":"2018-04-14T01:02:32Z","timestamp":1523667752000},"page":"561-588","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Verified Learning Without Regret"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8763-0053","authenticated-orcid":false,"given":"Samuel","family":"Merten","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6593-0661","authenticated-orcid":false,"given":"Alexander","family":"Bagnall","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0244-2980","authenticated-orcid":false,"given":"Gordon","family":"Stewart","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,4,14]]},"reference":[{"issue":"1","key":"20_CR1","doi-asserted-by":"publisher","first-page":"121","DOI":"10.4086\/toc.2012.v008a006","volume":"8","author":"S Arora","year":"2012","unstructured":"Arora, S., Hazan, E., Kale, S.: The multiplicative weights update method: a meta-algorithm and applications. Theor. Comput. 8(1), 121\u2013164 (2012)","journal-title":"Theor. Comput."},{"key":"20_CR2","doi-asserted-by":"crossref","unstructured":"Awerbuch, B., Azar, Y., Epstein, A.: The price of routing unsplittable flow. In: Proceedings of the thirty-seventh annual ACM Symposium on Theory of Computing, pp. 57\u201366. ACM (2005)","DOI":"10.1145\/1060590.1060599"},{"key":"20_CR3","doi-asserted-by":"publisher","first-page":"143","DOI":"10.24033\/asens.493","volume":"18","author":"L Bachelier","year":"1901","unstructured":"Bachelier, L.: Th\u00e9orie math\u00e9matique du jeu. Annales Scientifiques de l\u2019Ecole Normale Sup\u00e9rieure 18, 143\u2013209 (1901)","journal-title":"Annales Scientifiques de l\u2019Ecole Normale Sup\u00e9rieure"},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"Bagnall, A., Merten, S., Stewart, G.: Brief announcement: certified multiplicative weights update: verified learning without regret. In: Proceedings of the ACM Symposium on Principles of Distributed Computing, PODC 2017. ACM (2017)","DOI":"10.1145\/3087801.3087852"},{"key":"20_CR5","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y Bertot","year":"2013","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2013)"},{"key":"20_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-642-15781-3_2","volume-title":"Algorithms \u2013 ESA 2010","author":"K Bhawalkar","year":"2010","unstructured":"Bhawalkar, K., Gairing, M., Roughgarden, T.: Weighted congestion games: price of anarchy, universal worst-case examples, and tightness. In: de Berg, M., Meyer, U. (eds.) ESA 2010, Part II. LNCS, vol. 6347, pp. 17\u201328. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15781-3_2"},{"key":"20_CR7","volume-title":"Algorithmic Game Theory","author":"A Blum","year":"2007","unstructured":"Blum, A., Monsour, Y.: Learning, regret minimization, and equilibria. In: Nisan, N., Roughgarden, T., Tardos, E., Vazirani, V.V. (eds.) Algorithmic Game Theory. Cambridge University Press, Cambridge (2007). Chapter 4"},{"issue":"1304\u20131308","key":"20_CR8","first-page":"58","volume":"173","author":"E Borel","year":"1921","unstructured":"Borel, E.: La th\u00e9orie du jeu et les \u00e9quations int\u00e9grales \u00e0 noyau sym\u00e9trique. Comptes rendus de l\u2019Acad\u00e9mie des Sci. 173(1304\u20131308), 58 (1921)","journal-title":"Comptes rendus de l\u2019Acad\u00e9mie des Sci."},{"key":"20_CR9","doi-asserted-by":"crossref","unstructured":"Borowski, H., Marden, J.R., Shamma, J.: Learning efficient correlated equilibrium. Submitted for journal publication (2015)","DOI":"10.1109\/CDC.2014.7040463"},{"key":"20_CR10","doi-asserted-by":"crossref","unstructured":"Christodoulou, G., Koutsoupias, E.: The price of anarchy of finite congestion games. In: Proceedings of the 37th Annual ACM Symposium on Theory of Computing, pp. 67\u201373. ACM (2005)","DOI":"10.1145\/1060590.1060600"},{"key":"20_CR11","doi-asserted-by":"crossref","unstructured":"Demaine, E.D., Hajiaghayi, M., Mahini, H., Zadimoghaddam, M.: The price of anarchy in network creation games. In: Proceedings of the Twenty-sixth Annual ACM Symposium on Principles of Distributed Computing, pp. 292\u2013298. ACM (2007)","DOI":"10.1145\/1281100.1281142"},{"key":"20_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1007\/978-3-642-32589-2_33","volume-title":"Mathematical Foundations of Computer Science 2012","author":"A Fanelli","year":"2012","unstructured":"Fanelli, A., Moscardelli, L., Skopalik, A.: On the impact of fair best response dynamics. In: Rovan, B., Sassone, V., Widmayer, P. (eds.) MFCS 2012. LNCS, vol. 7464, pp. 360\u2013371. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32589-2_33"},{"issue":"1","key":"20_CR13","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1006\/game.1997.0595","volume":"21","author":"DP Foster","year":"1997","unstructured":"Foster, D.P., Vohra, R.V.: Calibrated learning and correlated equilibrium. Games Econ. Behav. 21(1), 40\u201355 (1997)","journal-title":"Games Econ. Behav."},{"key":"20_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/3-540-59119-2_166","volume-title":"Computational Learning Theory","author":"Y Freund","year":"1995","unstructured":"Freund, Y., Schapire, R.E.: A desicion-theoretic generalization of on-line learning and an application to boosting. In: Vit\u00e1nyi, P. (ed.) EuroCOLT 1995. LNCS, vol. 904, pp. 23\u201337. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-59119-2_166"},{"issue":"2","key":"20_CR15","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1111\/j.2517-6161.1979.tb01068.x","volume":"41","author":"JC Gittins","year":"1979","unstructured":"Gittins, J.C.: Bandit processes and dynamic allocation indices. J. R. Stat. Soc. Ser. B (Methodol.) 41(2), 148\u2013177 (1979)","journal-title":"J. R. Stat. Soc. Ser. B (Methodol.)"},{"key":"20_CR16","unstructured":"Gonthier, G., Mahboubi, A., Tassi, E.: A small scale reflection extension for the Coq system. Technical report, INRIA (2015)"},{"issue":"5","key":"20_CR17","doi-asserted-by":"publisher","first-page":"1127","DOI":"10.1111\/1468-0262.00153","volume":"68","author":"S Hart","year":"2000","unstructured":"Hart, S., Mas-Colell, A.: A simple adaptive procedure leading to correlated equilibrium. Econometrica 68(5), 1127\u20131150 (2000)","journal-title":"Econometrica"},{"key":"20_CR18","doi-asserted-by":"crossref","unstructured":"Hawblitzel, C., Howell, J., Kapritsos, M., Lorch, J.R., Parno, B., Roberts, M.L., Setty, S., Zill, B.: IronFleet: proving practical distributed systems correct. In: Proceedings of the 25th Symposium on Operating Systems Principles, pp. 1\u201317. ACM (2015)","DOI":"10.1145\/2815400.2815428"},{"key":"20_CR19","unstructured":"Hu, J., Wellman, M.P., et al.: Multiagent reinforcement learning: theoretical framework and an algorithm. In: ICML, vol. 98, pp. 242\u2013250. Citeseer (1998)"},{"key":"20_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-642-33475-7_15","volume-title":"Theoretical Computer Science","author":"P K\u00fcfner","year":"2012","unstructured":"K\u00fcfner, P., Nestmann, U., Rickmann, C.: Formal verification of distributed algorithms. In: Baeten, J.C.M., Ball, T., de Boer, F.S. (eds.) TCS 2012. LNCS, vol. 7604, pp. 209\u2013224. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33475-7_15"},{"key":"20_CR21","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"L Lamport","year":"2002","unstructured":"Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc., Boston (2002)"},{"key":"20_CR22","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"issue":"1","key":"20_CR23","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1145\/2914770.2837622","volume":"51","author":"Mohsen Lesani","year":"2016","unstructured":"Lesani, M., Bell, C.J., Chlipala, A.: Chapar: certified causally consistent distributed key-value stores. In: ACM SIGPLAN Notices, vol. 51. ACM (2016)","journal-title":"ACM SIGPLAN Notices"},{"key":"20_CR24","unstructured":"Lin, H., Yang, M., Long, F., Zhang, L., Zhou, L.: MODIST: transparent model checking of unmodified distributed systems. In: Proceedings of the 6th USENIX Symposium on Networked Systems Design and Implementation (2009)"},{"key":"20_CR25","doi-asserted-by":"crossref","unstructured":"Littlestone, N., Warmuth, M.K.: The weighted majority algorithm. In: Proceedings of the 30th Annual Symposium on Foundations of Computer Science. IEEE (1989)","DOI":"10.1109\/SFCS.1989.63487"},{"issue":"1","key":"20_CR26","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1006\/game.1996.0044","volume":"14","author":"D Monderer","year":"1996","unstructured":"Monderer, D., Shapley, L.S.: Potential games. Games Econ. Behav. 14(1), 124\u2013143 (1996)","journal-title":"Games Econ. Behav."},{"issue":"2","key":"20_CR27","doi-asserted-by":"publisher","first-page":"286","DOI":"10.2307\/1969529","volume":"54","author":"J Nash","year":"1951","unstructured":"Nash, J.: Non-cooperative games. Ann. Math. 54(2), 286\u2013295 (1951)","journal-title":"Ann. Math."},{"issue":"1","key":"20_CR28","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1073\/pnas.36.1.48","volume":"36","author":"JF Nash","year":"1950","unstructured":"Nash, J.F.: Equilibrium in n-player games. Proc. Natl. Acad. Sci. (PNAS) 36(1), 48\u201349 (1950)","journal-title":"Proc. Natl. Acad. Sci. (PNAS)"},{"key":"20_CR29","volume-title":"Theory of Games and Economic Behavior","author":"J Neumann von","year":"1944","unstructured":"von Neumann, J., Morgenstern, O.: Theory of Games and Economic Behavior, vol. 60. Princeton University Press, New Jersey (1944)"},{"key":"20_CR30","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.V.: Algorithmic Game Theory, vol. 1. Cambridge University Press, New York (2007)"},{"issue":"6","key":"20_CR31","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2813885.2737959","volume":"50","author":"P Panchekha","year":"2015","unstructured":"Panchekha, P., et al.: Automatically improving accuracy for floating point expressions. ACM SIGPLAN Not. 50(6), 1\u201311 (2015)","journal-title":"ACM SIGPLAN Not."},{"issue":"8","key":"20_CR32","doi-asserted-by":"publisher","first-page":"1249","DOI":"10.1287\/mnsc.1060.0656","volume":"53","author":"G Perakis","year":"2007","unstructured":"Perakis, G., Roels, G.: The price of anarchy in supply chains: quantifying the efficiency of price-only contracts. Manag. Sci. 53(8), 1249\u20131268 (2007)","journal-title":"Manag. Sci."},{"key":"20_CR33","unstructured":"Rahli, V.: Interfacing with proof assistants for domain specific programming using EventML. In: Proceedings of the 10th International Workshop on User Interfaces for Theorem Provers, Bremen, Germany (2012)"},{"key":"20_CR34","doi-asserted-by":"crossref","unstructured":"Ramananandro, T., et al.: A unified Coq framework for verifying C programs with floating-point computations. In: Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs. ACM (2016)","DOI":"10.1145\/2854065.2854066"},{"key":"20_CR35","doi-asserted-by":"crossref","unstructured":"Roughgarden, T.: Intrinsic robustness of the price of anarchy. In: Proceedings of the 41st Annual ACM Symposium on Theory of Computing, pp. 513\u2013522. ACM (2009)","DOI":"10.1145\/1536414.1536485"},{"key":"20_CR36","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781316779309","volume-title":"Twenty Lectures on Algorithmic Game Theory","author":"T Roughgarden","year":"2016","unstructured":"Roughgarden, T.: Twenty Lectures on Algorithmic Game Theory. Cambridge University Press, New York (2016)"},{"key":"20_CR37","doi-asserted-by":"crossref","unstructured":"Sergey, I., Wilcox, J.R., Tatlock, Z.: Programming and proving with distributed protocols. In: Proceedings of the ACM on Programming Languages, vol. 2 (POPL), Article 28 (2018)","DOI":"10.1145\/3158116"},{"issue":"04","key":"20_CR38","doi-asserted-by":"publisher","first-page":"795","DOI":"10.1017\/S0960129511000119","volume":"21","author":"B Spitters","year":"2011","unstructured":"Spitters, B., Van der Weegen, E.: Type classes for mathematics in type theory. Math. Struct. Comput. Sci. 21(04), 795\u2013825 (2011)","journal-title":"Math. Struct. Comput. Sci."},{"key":"20_CR39","volume-title":"Reinforcement Learning: An Introduction","author":"RS Sutton","year":"1998","unstructured":"Sutton, R.S., Barto, A.G.: Reinforcement Learning: An Introduction, vol. 1. MIT press, Cambridge (1998)"},{"key":"20_CR40","doi-asserted-by":"crossref","unstructured":"Vetta, A.: Nash equilibria in competitive societies, with applications to facility location, traffic routing and auctions. In: Proceedings of the 43rd Annual IEEE Symposium on Foundations of Computer Science, pp. 416\u2013425. IEEE (2002)","DOI":"10.1109\/SFCS.2002.1181966"},{"issue":"3\u20134","key":"20_CR41","first-page":"279","volume":"8","author":"CJ Watkins","year":"1992","unstructured":"Watkins, C.J., Dayan, P.: Q-learning. Mach. Learn. 8(3\u20134), 279\u2013292 (1992)","journal-title":"Mach. Learn."},{"issue":"6","key":"20_CR42","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1145\/2813885.2737958","volume":"50","author":"James R. Wilcox","year":"2015","unstructured":"Wilcox, J.R., Woos, D., Panchekha, P., Tatlock, Z., Wang, X., Ernst, M.D., Anderson, T.: Verdi: a framework for implementing and formally verifying distributed systems. In: ACM SIGPLAN Notices, vol. 50, pp. 357\u2013368. ACM (2015)","journal-title":"ACM SIGPLAN Notices"},{"key":"20_CR43","unstructured":"Zermelo, E.: \u00dcber eine anwendung der mengenlehre auf die theorie des schachspiels. In: Proceedings of the Fifth International Congress of Mathematicians, vol. 2, pp. 501\u2013504. II, Cambridge University Press, Cambridge (1913)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-89884-1_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,6]],"date-time":"2024-07-06T00:58:08Z","timestamp":1720227488000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-89884-1_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319898834","9783319898841"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-89884-1_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}