Document Open Access Logo

Coverage and Vacuity in Network Formation Games

Authors Gili Bielous, Orna Kupferman

PDF
Thumbnail PDF

File

LIPIcs.CSL.2020.10.pdf
  • Filesize: 0.63 MB
  • 18 pages

Document Identifiers

Author Details

Gili Bielous
  • School of Computer Science and Engineering, The Hebrew University, Jerusalem, Israel
Orna Kupferman
  • School of Computer Science and Engineering, The Hebrew University, Jerusalem, Israel

Cite AsGet BibTex

Gili Bielous and Orna Kupferman. Coverage and Vacuity in Network Formation Games. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.CSL.2020.10

Abstract

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Algorithmic game theory
  • Theory of computation → Network games
  • Theory of computation → Network formation
  • Software and its engineering → Formal methods
Keywords
  • Network Formation Games
  • Vacuity
  • Coverage

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. 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. Google Scholar
  2. S. Almagor, U. Boker, and O. Kupferman. Formalizing and Reasoning About Quality. Journal of the ACM, 63(3), 2016. Google Scholar
  3. R. Alur, T.A. Henzinger, and O. Kupferman. Alternating-time temporal logic. Journal of the ACM, 49(5):672-713, 2002. Google Scholar
  4. 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. Google Scholar
  5. 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. Google Scholar
  6. 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. Google Scholar
  7. 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. Google Scholar
  8. 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. Google Scholar
  9. G. Avni, O. Kupferman, and T. Tamir. Network-formation games with regular objectives. Information and Computation, 251:165-178, 2016. Google Scholar
  10. 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. Google Scholar
  11. 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. Google Scholar
  12. D. Braess. Über ein paradoxon aus der verkehrsplanung. Unternehmensforschung, 12(1):258-268, 1968. Google Scholar
  13. K. Chatterjee, T. A. Henzinger, and N. Piterman. Strategy logic. Information and Computation, 208(6):677-693, 2010. Google Scholar
  14. H. Chockler, A. Gurfinkel, and O. Strichman. Beyond vacuity: towards the strongest passing formula. Formal Methods in System Design, 43(3):552-571, 2013. Google Scholar
  15. 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. Google Scholar
  16. 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. Google Scholar
  17. H. Chockler, O. Kupferman, and M.Y. Vardi. Coverage Metrics for Formal Verification. Software Tools for Technology Transfer, 8(4-5):373-386, 2006. Google Scholar
  18. E.M. Clarke, O. Grumberg, D. Kroening, D. Peled, and H. Veith. Model Checking, Second Edition. MIT Press, 2018. Google Scholar
  19. R. Cole, Y. Dodis, and T. Roughgarden. How much can taxes help selfish routing? J. Comput. Syst. Sci., 72(3):444-467, 2006. Google Scholar
  20. J. Correa, A. Schulz, and N. Stier Moses. Selfish Routing in Capacitated Networks. Math. Oper. Res., 29(4):961-976, 2004. Google Scholar
  21. 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. Google Scholar
  22. 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. Google Scholar
  23. 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. Google Scholar
  24. 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. Google Scholar
  25. 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. Google Scholar
  26. M.W. Krentel. The complexity of optimization problems. Journal of Computer and Systems Science, 36:490-509, 1988. Google Scholar
  27. 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. Google Scholar
  28. 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. Google Scholar
  29. 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. Google Scholar
  30. 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. Google Scholar
  31. O. Kupferman and M.Y. Vardi. Vacuity detection in temporal model checking. Software Tools for Technology Transfer, 4(2):224-233, 2003. Google Scholar
  32. 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. Google Scholar
  33. 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. Google Scholar
  34. 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. Google Scholar
  35. 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. Google Scholar
  36. 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. Google Scholar
  37. E. Tardos and T. Wexler. Algorithmic Game Theory. Cambridge University Press, 2007. Chapter 19: Network Formation Games and the Potential Function Method. Google Scholar
  38. 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. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact