2 Search Results for "Dvorak, Martin"

Document
DOI: 10.4230/LIPIcs.ITP.2023.15
Closure Properties of General Grammars – Formally Verified

Authors: Martin Dvorak and Jasmin Blanchette

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

Abstract
We formalized general (i.e., type-0) grammars using the Lean 3 proof assistant. We defined basic notions of rewrite rules and of words derived by a grammar, and used grammars to show closure of the class of type-0 languages under four operations: union, reversal, concatenation, and the Kleene star. The literature mostly focuses on Turing machine arguments, which are possibly more difficult to formalize. For the Kleene star, we could not follow the literature and came up with our own grammar-based construction.
Cite as

Martin Dvorak and Jasmin Blanchette. Closure Properties of General Grammars – Formally Verified. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 15:1-15:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{dvorak_et_al:LIPIcs.ITP.2023.15,
  author =	{Dvorak, Martin and Blanchette, Jasmin},
  title =	{{Closure Properties of General Grammars – Formally Verified}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{15:1--15:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.15},
  URN =		{urn:nbn:de:0030-drops-183906},
  doi =		{10.4230/LIPIcs.ITP.2023.15},
  annote =	{Keywords: Lean, type-0 grammars, recursively enumerable languages, Kleene star}
}
Document
DOI: 10.4230/LIPIcs.STACS.2015.90
Welfare Maximization with Friends-of-Friends Network Externalities

Authors: Sayan Bhattacharya, Wolfgang Dvorák, Monika Henzinger, and Martin Starnberger

Published in: LIPIcs, Volume 30, 32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015)

Abstract
Online social networks allow the collection of large amounts of data about the influence between users connected by a friendship-like relationship. When distributing items among agents forming a social network, this information allows us to exploit network externalities that each agent receives from his neighbors that get the same item. In this paper we consider Friends-of-Friends (2-hop) network externalities, i.e., externalities that not only depend on the neighbors that get the same item but also on neighbors of neighbors. For these externalities we study a setting where multiple different items are assigned to unit-demand agents. Specifically, we study the problem of welfare maximization under different types of externality functions. Let n be the number of agents and m be the number of items. Our contributions are the following: (1) We show that welfare maximization is APX-hard; we show that even for step functions with 2-hop (and also with 1-hop) externalities it is NP-hard to approximate social welfare better than (1-1/e). (2) On the positive side we present (i) an O(sqrt n)-approximation algorithm for general concave externality functions, (ii) an O(\log m)-approximation algorithm for linear externality functions, and (iii) an (1-1/e)\frac{1}{6}-approximation algorithm for 2-hop step function externalities. We also improve the result from [6] for 1-hop step function externalities by giving a (1-1/e)/2-approximation algorithm.
Cite as

Sayan Bhattacharya, Wolfgang Dvorák, Monika Henzinger, and Martin Starnberger. Welfare Maximization with Friends-of-Friends Network Externalities. In 32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 30, pp. 90-102, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{bhattacharya_et_al:LIPIcs.STACS.2015.90,
  author =	{Bhattacharya, Sayan and Dvor\'{a}k, Wolfgang and Henzinger, Monika and Starnberger, Martin},
  title =	{{Welfare Maximization with Friends-of-Friends Network Externalities}},
  booktitle =	{32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015)},
  pages =	{90--102},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-78-1},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{30},
  editor =	{Mayr, Ernst W. and Ollinger, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2015.90},
  URN =		{urn:nbn:de:0030-drops-49066},
  doi =		{10.4230/LIPIcs.STACS.2015.90},
  annote =	{Keywords: network externalities, welfare maximization, approximation algorithms}
}
  • Refine by Author
  • 1 Bhattacharya, Sayan
  • 1 Blanchette, Jasmin
  • 1 Dvorak, Martin
  • 1 Dvorák, Wolfgang
  • 1 Henzinger, Monika
  • Show More...

  • Refine by Classification
  • 1 Theory of computation → Rewrite systems

  • Refine by Keyword
  • 1 Kleene star
  • 1 Lean
  • 1 approximation algorithms
  • 1 network externalities
  • 1 recursively enumerable languages
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2015
  • 1 2023

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 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact