Coverage and Vacuity in Network Formation Games
The frameworks of coverage and vacuity in formal verification analyze the effect of mutations applied to systems or their specifications. We adopt these notions to network formation games, analyzing the effect of a change in the cost of a resource. We consider two measures to be affected: the cost of the Social Optimum and extremums of costs of Nash Equilibria. Our results offer a formal framework to the effect of mutations in network formation games and include a complexity analysis of related decision problems. They also tighten the relation between algorithmic game theory and formal verification, suggesting refined definitions of coverage and vacuity for the latter.
Network Formation Games
Vacuity
Coverage
Theory of computation~Algorithmic game theory
Theory of computation~Network games
Theory of computation~Network formation
Software and its engineering~Formal methods
10:1-10:18
Regular Paper
A full version of the paper is available at https://www.cs.huji.ac.il/~ornak/publications/csl20.pdf.
Gili
Bielous
Gili Bielous
School of Computer Science and Engineering, The Hebrew University, Jerusalem, Israel
Orna
Kupferman
Orna Kupferman
School of Computer Science and Engineering, The Hebrew University, Jerusalem, Israel
10.4230/LIPIcs.CSL.2020.10
S. Albers, S. Elits, E. Even-Dar, Y. Mansour, and L. Roditty. On Nash Equilibria for a Network Creation Game. In 7th ACM-SIAM Symposium on Discrete Algorithms, 2006.
S. Almagor, U. Boker, and O. Kupferman. Formalizing and Reasoning About Quality. Journal of the ACM, 63(3), 2016.
R. Alur, T.A. Henzinger, and O. Kupferman. Alternating-time temporal logic. Journal of the ACM, 49(5):672-713, 2002.
E. Anshelevich, A. Dasgupta, J. Kleinberg, E. Tardos, T. Wexler, and T. Roughgarden. The Price of Stability for Network Design with Fair Cost Allocation. SIAM J. Comput., 38(4):1602-1623, 2008.
G. Avni, S. Guha, and O. Kupferman. An Abstraction-Refinement Methodology for Reasoning about Network Games. In Proc. 26th Int. Joint Conf. on Artificial Intelligence, pages 70-76, 2017.
G. Avni, S. Guha, and O. Kupferman. Timed Network Games. In 42nd Int. Symp. on Mathematical Foundations of Computer Science, volume 83 of LIPIcs, pages 37:1-37:16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, 2017.
G. Avni, T.A. Henzinger, and O. Kupferman. Dynamic Resource Allocation Games. In Algorithmic Game Theory - 9th International Symposium, volume 9928 of Lecture Notes in Computer Science, pages 153-166. Springer, 2016.
G. Avni and O. Kupferman. Synthesis from Component Libraries with Costs. In Proc. 25th Int. Conf. on Concurrency Theory, volume 8704 of Lecture Notes in Computer Science, pages 156-172. Springer, 2014.
G. Avni, O. Kupferman, and T. Tamir. Network-formation games with regular objectives. Information and Computation, 251:165-178, 2016.
I. Beer, S. Ben-David, C. Eisner, and Y. Rodeh. Efficient detection of vacuity in ACTL formulas. Formal Methods in System Design, 18(2):141-162, 2001.
P. Bouyer-Decitre, O. Kupferman, N. Markey, B. Maubert, A. Murano, and G. Perelli. Reasoning about Quality and Fuzziness of Strategic Behaviours. In Proc. 28th Int. Joint Conf. on Artificial Intelligence, 2019.
D. Braess. Über ein paradoxon aus der verkehrsplanung. Unternehmensforschung, 12(1):258-268, 1968.
K. Chatterjee, T. A. Henzinger, and N. Piterman. Strategy logic. Information and Computation, 208(6):677-693, 2010.
H. Chockler, A. Gurfinkel, and O. Strichman. Beyond vacuity: towards the strongest passing formula. Formal Methods in System Design, 43(3):552-571, 2013.
H. Chockler, O. Kupferman, R.P. Kurshan, and M.Y. Vardi. A Practical Approach to Coverage in Model Checking. In Proc. 13th Int. Conf. on Computer Aided Verification, volume 2102 of Lecture Notes in Computer Science, pages 66-78. Springer, 2001.
H. Chockler, O. Kupferman, and M.Y. Vardi. Coverage Metrics for Temporal Logic Model Checking. In Proc. 7th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, number 2031 in Lecture Notes in Computer Science, pages 528-542. Springer, 2001.
H. Chockler, O. Kupferman, and M.Y. Vardi. Coverage Metrics for Formal Verification. Software Tools for Technology Transfer, 8(4-5):373-386, 2006.
E.M. Clarke, O. Grumberg, D. Kroening, D. Peled, and H. Veith. Model Checking, Second Edition. MIT Press, 2018.
R. Cole, Y. Dodis, and T. Roughgarden. How much can taxes help selfish routing? J. Comput. Syst. Sci., 72(3):444-467, 2006.
J. Correa, A. Schulz, and N. Stier Moses. Selfish Routing in Capacitated Networks. Math. Oper. Res., 29(4):961-976, 2004.
A. Fabrikant, A. Luthra, E. Maneva, C. Papadimitriou, and S. Shenker. On a Network Creation Game. In ACM Symposium on Principles of Distributed Computing, 2003.
D. Fisman, O. Kupferman, and Y. Lustig. Rational Synthesis. In Proc. 16th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, volume 6015 of Lecture Notes in Computer Science, pages 190-204. Springer, 2010.
J.D. Hartline and T. Roughgarden. Optimal mechanism design and money burning. In Proc. 40th ACM Symp. on Theory of Computing, pages 75-84, 2008.
Y. Hoskote, T. Kam, P.-H Ho, and X. Zhao. Coverage estimation for symbolic model checking. In Proc. 36th Design Automation Conf., pages 300-305, 1999.
S. Katz, D. Geist, and O. Grumberg. "Have I written enough properties ?" A method of comparison between specification and implementation. In Proc. 10th Conf. on Correct Hardware Design and Verification Methods, volume 1703 of Lecture Notes in Computer Science, pages 280-297. Springer, 1999.
M.W. Krentel. The complexity of optimization problems. Journal of Computer and Systems Science, 36:490-509, 1988.
O. Kupferman. Sanity Checks in Formal Verification. In Proc. 17th Int. Conf. on Concurrency Theory, volume 4137 of Lecture Notes in Computer Science, pages 37-51. Springer, 2006.
O. Kupferman. Examining classical graph-theory problems from the viewpoint of formal-verification methods. In Proc. 49th ACM Symp. on Theory of Computing, page 6, 2017.
O. Kupferman, W. Li, and S.A. Seshia. A Theory of Mutations with Applications to Vacuity, Coverage, and Fault Tolerance. In Proc. 8th Int. Conf. on Formal Methods in Computer-Aided Design, pages 1-9, 2008.
O. Kupferman and T. Tamir. Hierarchical Network Formation Games. In Proc. 22nd Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, volume 10205 of Lecture Notes in Computer Science, pages 229-246. Springer, 2017.
O. Kupferman and M.Y. Vardi. Vacuity detection in temporal model checking. Software Tools for Technology Transfer, 4(2):224-233, 2003.
F. Mogavero, A. Murano, G. Perelli, and M. Y. Vardi. Reasoning About Strategies: On the Model-Checking Problem. ACM Transactions on Computational Logic, 15(4):34:1-34:47, 2014.
O. Padon, N. Immerman, A. Karbyshev, O. Lahav, M. Sagiv, and S. Shoham. Decentralizing SDN Policies. In Proc. 42nd ACM Symp. on Principles of Programming Languages, pages 663-676, 2015.
A. Panda, K. Argyraki, M. Sagiv, M. Schapira, and S. Shenker. New Directions for Network Verification. In 1st Summit on Advances in Programming Languages, volume 32 of LIPIcs, pages 209-220, 2015.
C.H. Papadimitriou and M. Yannakakis. The complexity of facets (and some facets of complexity). In Proc. 14th ACM Symp. on Theory of Computing, pages 255-260, 1982.
F. Souza and L.C. Rego. Mixed equilibrium in 2 x 2 normal form games: when burning money is rational. Pesquisa Operacional, 36:81-99, April 2016.
E. Tardos and T. Wexler. Algorithmic Game Theory. Cambridge University Press, 2007. Chapter 19: Network Formation Games and the Potential Function Method.
M. Wooldridge, J. Gutierrez, P. Harrenstein, E. Marchioni, G. Perelli, and A. Toumi. Rational Verification: From Model Checking to Equilibrium Checking. In Proc. of 30th National Conf. on Artificial Intelligence, pages 4184-4190, 2016.
Gili Bielous and Orna Kupferman
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode