Search Results

Documents authored by Benedikt, Michael

Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2024.127
Decidability of Graph Neural Networks via Logical Characterizations

Authors: Michael Benedikt, Chia-Hsuan Lu, Boris Motik, and Tony Tan

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract
We present results concerning the expressiveness and decidability of a popular graph learning formalism, graph neural networks (GNNs), exploiting connections with logic. We use a family of recently-discovered decidable logics involving "Presburger quantifiers". We show how to use these logics to measure the expressiveness of classes of GNNs, in some cases getting exact correspondences between the expressiveness of logics and GNNs. We also employ the logics, and the techniques used to analyze them, to obtain decision procedures for verification problems over GNNs. We complement this with undecidability results for static analysis problems involving the logics, as well as for GNN verification problems.
Cite as

Michael Benedikt, Chia-Hsuan Lu, Boris Motik, and Tony Tan. Decidability of Graph Neural Networks via Logical Characterizations. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 127:1-127:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{benedikt_et_al:LIPIcs.ICALP.2024.127,
  author =	{Benedikt, Michael and Lu, Chia-Hsuan and Motik, Boris and Tan, Tony},
  title =	{{Decidability of Graph Neural Networks via Logical Characterizations}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{127:1--127:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.127},
  URN =		{urn:nbn:de:0030-drops-202708},
  doi =		{10.4230/LIPIcs.ICALP.2024.127},
  annote =	{Keywords: Logic, Graph Neural Networks}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2023.112
The Complexity of Presburger Arithmetic with Power or Powers

Authors: Michael Benedikt, Dmitry Chistikov, and Alessio Mansutti

Published in: LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)

Abstract
We investigate expansions of Presburger arithmetic (Pa), i.e., the theory of the integers with addition and order, with additional structure related to exponentiation: either a function that takes a number to the power of 2, or a predicate 2^ℕ for the powers of 2. The latter theory, denoted Pa(2^ℕ(·)), was introduced by Büchi as a first attempt at characterizing the sets of tuples of numbers that can be expressed using finite automata; Büchi’s method does not give an elementary upper bound, and the complexity of this theory has been open. The former theory, denoted as Pa(λx.2^|x|), was shown decidable by Semenov; while the decision procedure for this theory differs radically from the automata-based method proposed by Büchi, Semenov’s method is also non-elementary. And in fact, the theory with the power function has a non-elementary lower bound. In this paper, we show that while Semenov’s and Büchi’s approaches yield non-elementary blow-ups for Pa(2^ℕ(·)), the theory is in fact decidable in triply exponential time, similarly to the best known quantifier-elimination algorithm for Pa. We also provide a NExpTime upper bound for the existential fragment of Pa(λx.2^|x|), a step towards a finer-grained analysis of its complexity. Both these results are established by analyzing a single parameterized satisfiability algorithm for Pa(λx.2^|x|), which can be specialized to either the setting of Pa(2^ℕ(·)) or the existential theory of Pa(λx.2^|x|). Besides the new upper bounds for the existential theory of Pa(λx.2^|x|) and Pa(2^ℕ(·)), we believe our algorithm provides new intuition for the decidability of these theories, and for the features that lead to non-elementary blow-ups.
Cite as

Michael Benedikt, Dmitry Chistikov, and Alessio Mansutti. The Complexity of Presburger Arithmetic with Power or Powers. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 112:1-112:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{benedikt_et_al:LIPIcs.ICALP.2023.112,
  author =	{Benedikt, Michael and Chistikov, Dmitry and Mansutti, Alessio},
  title =	{{The Complexity of Presburger Arithmetic with Power or Powers}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{112:1--112:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-278-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{261},
  editor =	{Etessami, Kousha and Feige, Uriel and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.112},
  URN =		{urn:nbn:de:0030-drops-181641},
  doi =		{10.4230/LIPIcs.ICALP.2023.112},
  annote =	{Keywords: arithmetic theories, exponentiation, decision procedures}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2020.112
Two Variable Logic with Ultimately Periodic Counting

Authors: Michael Benedikt, Egor V. Kostylev, and Tony Tan

Published in: LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)

Abstract
We consider the extension of FO² with quantifiers that state that the number of elements where a formula holds should belong to a given ultimately periodic set. We show that both satisfiability and finite satisfiability of the logic are decidable. We also show that the spectrum of any sentence is definable in Presburger arithmetic. In the process we present several refinements to the "biregular graph method". In this method, decidability issues concerning two-variable logics are reduced to questions about Presburger definability of integer vectors associated with partitioned graphs, where nodes in a partition satisfy certain constraints on their in- and out-degrees.
Cite as

Michael Benedikt, Egor V. Kostylev, and Tony Tan. Two Variable Logic with Ultimately Periodic Counting. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 112:1-112:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{benedikt_et_al:LIPIcs.ICALP.2020.112,
  author =	{Benedikt, Michael and Kostylev, Egor V. and Tan, Tony},
  title =	{{Two Variable Logic with Ultimately Periodic Counting}},
  booktitle =	{47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
  pages =	{112:1--112:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-138-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{168},
  editor =	{Czumaj, Artur and Dawar, Anuj and Merelli, Emanuela},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.112},
  URN =		{urn:nbn:de:0030-drops-125197},
  doi =		{10.4230/LIPIcs.ICALP.2020.112},
  annote =	{Keywords: Presburger Arithmetic, Two-variable logic}
}
Document
DOI: 10.4230/DagRep.9.9.1
Logic and Learning (Dagstuhl Seminar 19361)

Authors: Michael Benedikt, Kristian Kersting, Phokion G. Kolaitis, and Daniel Neider

Published in: Dagstuhl Reports, Volume 9, Issue 9 (2020)

Abstract
The goal of building truly intelligent systems has forever been a central problem in computer science. While logic-based approaches of yore have had their successes and failures, the era of machine learning, specifically deep learning is also coming upon significant challenges. There is a growing consensus that the inductive reasoning and complex, high-dimensional pattern recognition capabilities of deep learning models need to be combined with symbolic (even programmatic), deductive capabilities traditionally developed in the logic and automated reasoning communities in order to achieve the next step towards building intelligent systems, including making progress at the frontier of hard problems such as explainable AI. However, these communities tend to be quite separate and interact only minimally, often at odds with each other upon the subject of the ``correct approach'' to AI. This report documents the efforts of Dagstuhl Seminar 19361 on ``Logic and Learning'' to bring these communities together in order to: (i) bridge the research efforts between them and foster an exchange of ideas in order to create unified formalisms and approaches that bear the advantages of both research methodologies; (ii) review and analyse the progress made across both communities; (iii) understand the subtleties and difficulties involved in solving hard problems using both perspectives; (iv) make attempts towards a consensus on what the hard problems are and what the elements of good solutions to these problems would be. The three focal points of the seminar were the strands of ``Logic for Machine Learning'', ``Machine Learning for Logic'', and ``Logic vs. Machine Learning''. The seminar format consisted of long and short talks, as well as breakout sessions. We summarise the motivations and proceedings of the seminar, and report on the abstracts of the talks and the results of the breakout sessions.
Cite as

Michael Benedikt, Kristian Kersting, Phokion G. Kolaitis, and Daniel Neider. Logic and Learning (Dagstuhl Seminar 19361). In Dagstuhl Reports, Volume 9, Issue 9, pp. 1-22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@Article{benedikt_et_al:DagRep.9.9.1,
  author =	{Benedikt, Michael and Kersting, Kristian and Kolaitis, Phokion G. and Neider, Daniel},
  title =	{{Logic and Learning (Dagstuhl Seminar 19361)}},
  pages =	{1--22},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2020},
  volume =	{9},
  number =	{9},
  editor =	{Benedikt, Michael and Kersting, Kristian and Kolaitis, Phokion G. and Neider, Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.9.9.1},
  URN =		{urn:nbn:de:0030-drops-118425},
  doi =		{10.4230/DagRep.9.9.1},
  annote =	{Keywords: Artificial Intelligence, Automated reasoning, Databases, Deep Learning, Inductive Logic Programming, Logic, Logic and Learning, Logic for Machine Learning, Logic vs. Machine Learning, Machine Learning, Machine Learning for Logic, Neurosymbolic methods}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2017.107
Characterizing Definability in Decidable Fixpoint Logics

Authors: Michael Benedikt, Pierre Bourhis, and Michael Vanden Boom

Published in: LIPIcs, Volume 80, 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)

Abstract
We look at characterizing which formulas are expressible in rich decidable logics such as guarded fixpoint logic, unary negation fixpoint logic, and guarded negation fixpoint logic. We consider semantic characterizations of definability, as well as effective characterizations. Our algorithms revolve around a finer analysis of the tree-model property and a refinement of the method of moving back-and-forth between relational logics and logics over trees.
Cite as

Michael Benedikt, Pierre Bourhis, and Michael Vanden Boom. Characterizing Definability in Decidable Fixpoint Logics. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 107:1-107:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{benedikt_et_al:LIPIcs.ICALP.2017.107,
  author =	{Benedikt, Michael and Bourhis, Pierre and Vanden Boom, Michael},
  title =	{{Characterizing Definability in Decidable Fixpoint Logics}},
  booktitle =	{44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)},
  pages =	{107:1--107:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-041-5},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{80},
  editor =	{Chatzigiannakis, Ioannis and Indyk, Piotr and Kuhn, Fabian and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2017.107},
  URN =		{urn:nbn:de:0030-drops-74062},
  doi =		{10.4230/LIPIcs.ICALP.2017.107},
  annote =	{Keywords: Guarded logics, bisimulation, definability, automata}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.ICDT.2017
LIPIcs, Volume 68, ICDT'17, Complete Volume

Authors: Michael Benedikt and Giorgio Orsi

Published in: LIPIcs, Volume 68, 20th International Conference on Database Theory (ICDT 2017)

Abstract
LIPIcs, Volume 68, ICDT'17, Complete Volume
Cite as

20th International Conference on Database Theory (ICDT 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 68, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Proceedings{benedikt_et_al:LIPIcs.ICDT.2017,
  title =	{{LIPIcs, Volume 68, ICDT'17, Complete Volume}},
  booktitle =	{20th International Conference on Database Theory (ICDT 2017)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-024-8},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{68},
  editor =	{Benedikt, Michael and Orsi, Giorgio},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2017},
  URN =		{urn:nbn:de:0030-drops-70689},
  doi =		{10.4230/LIPIcs.ICDT.2017},
  annote =	{Keywords: Database Management, Normal Forms, Schema and Subschema, Query Languages, \lbrackSystems\rbrack Query Processing, Relational Databases, Distributed Databases}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.ICDT.2017.0
Front Matter, Table of Contents, Preface, Conference Organization, List of Authors

Authors: Michael Benedikt and Giorgio Orsi

Published in: LIPIcs, Volume 68, 20th International Conference on Database Theory (ICDT 2017)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization, List of Authors
Cite as

20th International Conference on Database Theory (ICDT 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 68, pp. 0:i-0:xii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{benedikt_et_al:LIPIcs.ICDT.2017.0,
  author =	{Benedikt, Michael and Orsi, Giorgio},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization, List of Authors}},
  booktitle =	{20th International Conference on Database Theory (ICDT 2017)},
  pages =	{0:i--0:xii},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-024-8},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{68},
  editor =	{Benedikt, Michael and Orsi, Giorgio},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2017.0},
  URN =		{urn:nbn:de:0030-drops-70446},
  doi =		{10.4230/LIPIcs.ICDT.2017.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization, List of Authors}
}
Document
DOI: 10.4230/DagRep.4.8.1
Querying and Reasoning Under Expressive Constraints (Dagstuhl Seminar 14331)

Authors: Michael Benedikt, Carsten Lutz, and Balder Ten Cate

Published in: Dagstuhl Reports, Volume 4, Issue 8 (2015)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 14331 "Querying and Reasoning Under Expressive Constraints" which took place from August 10th to August 14th, 2014. The seminar aimed to bring together researchers in databases, knowledge representation, decidable fragments of first-order logic, and constraint satisfaction to identify and discuss common themes and technique as well as complementary ones, identify future research issues, and foster cooperation and cross-fertilization between the communities.
Cite as

Michael Benedikt, Carsten Lutz, and Balder Ten Cate. Querying and Reasoning Under Expressive Constraints (Dagstuhl Seminar 14331). In Dagstuhl Reports, Volume 4, Issue 8, pp. 1-20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@Article{benedikt_et_al:DagRep.4.8.1,
  author =	{Benedikt, Michael and Lutz, Carsten and Ten Cate, Balder},
  title =	{{Querying and Reasoning Under Expressive Constraints (Dagstuhl Seminar 14331)}},
  pages =	{1--20},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2014},
  volume =	{4},
  number =	{8},
  editor =	{Benedikt, Michael and Lutz, Carsten and Ten Cate, Balder},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.4.8.1},
  URN =		{urn:nbn:de:0030-drops-47941},
  doi =		{10.4230/DagRep.4.8.1},
  annote =	{Keywords: Integrity constraints, Open-World Query Answering, Ontology-Based Data Access, Knowledge Representation, Automated Reasoning, Decidable Fragments of}
}
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact