Search Results

Documents authored by Rudolph, Sebastian

Document
DOI: 10.4230/LIPIcs.CSL.2024.33
Decidable (Ac)counting with Parikh and Muller: Adding Presburger Arithmetic to Monadic Second-Order Logic over Tree-Interpretable Structures

Authors: Luisa Herrmann, Vincent Peth, and Sebastian Rudolph

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)

Abstract
We propose ωMSO⋈BAPA , an expressive logic for describing countable structures, which subsumes and transcends both Counting Monadic Second-Order Logic (CMSO) and Boolean Algebra with Presburger Arithmetic (BAPA). We show that satisfiability of ωMSO⋈BAPA is decidable over the class of labeled infinite binary trees, whereas it becomes undecidable even for a rather mild relaxations. The decidability result is established by an elaborate multi-step transformation into a particular normal form, followed by the deployment of Parikh-Muller Tree Automata, a novel kind of automaton for infinite labeled binary trees, integrating and generalizing both Muller and Parikh automata while still exhibiting a decidable (in fact PSpace-complete) emptiness problem. By means of MSO-interpretations, we lift the decidability result to all tree-interpretable classes of structures, including the classes of finite/countable structures of bounded treewidth/cliquewidth/partitionwidth. We generalize the result further by showing that decidability is even preserved when coupling width-restricted ωMSO⋈BAPA with width-unrestricted two-variable logic with advanced counting. A final showcase demonstrates how our results can be leveraged to harvest decidability results for expressive μ-calculi extended by global Presburger constraints.
Cite as

Luisa Herrmann, Vincent Peth, and Sebastian Rudolph. Decidable (Ac)counting with Parikh and Muller: Adding Presburger Arithmetic to Monadic Second-Order Logic over Tree-Interpretable Structures. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 33:1-33:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{herrmann_et_al:LIPIcs.CSL.2024.33,
  author =	{Herrmann, Luisa and Peth, Vincent and Rudolph, Sebastian},
  title =	{{Decidable (Ac)counting with Parikh and Muller: Adding Presburger Arithmetic to Monadic Second-Order Logic over Tree-Interpretable Structures}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{33:1--33:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.33},
  URN =		{urn:nbn:de:0030-drops-196768},
  doi =		{10.4230/LIPIcs.CSL.2024.33},
  annote =	{Keywords: MSO, BAPA, Parikh-Muller tree automata, decidability, MSO-interpretations}
}
Document
DOI: 10.4230/LIPIcs.ICDT.2023.18
Finite-Cliquewidth Sets of Existential Rules: Toward a General Criterion for Decidable yet Highly Expressive Querying

Authors: Thomas Feller, Tim S. Lyon, Piotr Ostropolski-Nalewaja, and Sebastian Rudolph

Published in: LIPIcs, Volume 255, 26th International Conference on Database Theory (ICDT 2023)

Abstract
In our pursuit of generic criteria for decidable ontology-based querying, we introduce finite-cliquewidth sets (fcs) of existential rules, a model-theoretically defined class of rule sets, inspired by the cliquewidth measure from graph theory. By a generic argument, we show that fcs ensures decidability of entailment for a sizable class of queries (dubbed DaMSOQs) subsuming conjunctive queries (CQs). The fcs class properly generalizes the class of finite-expansion sets (fes), and for signatures of arity ≤ 2, the class of bounded-treewidth sets (bts). For higher arities, bts is only indirectly subsumed by fcs by means of reification. Despite the generality of fcs, we provide a rule set with decidable CQ entailment (by virtue of first-order-rewritability) that falls outside fcs, thus demonstrating the incomparability of fcs and the class of finite-unification sets (fus). In spite of this, we show that if we restrict ourselves to single-headed rule sets over signatures of arity ≤ 2, then fcs subsumes fus.
Cite as

Thomas Feller, Tim S. Lyon, Piotr Ostropolski-Nalewaja, and Sebastian Rudolph. Finite-Cliquewidth Sets of Existential Rules: Toward a General Criterion for Decidable yet Highly Expressive Querying. In 26th International Conference on Database Theory (ICDT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 255, pp. 18:1-18:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{feller_et_al:LIPIcs.ICDT.2023.18,
  author =	{Feller, Thomas and Lyon, Tim S. and Ostropolski-Nalewaja, Piotr and Rudolph, Sebastian},
  title =	{{Finite-Cliquewidth Sets of Existential Rules: Toward a General Criterion for Decidable yet Highly Expressive Querying}},
  booktitle =	{26th International Conference on Database Theory (ICDT 2023)},
  pages =	{18:1--18:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-270-9},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{255},
  editor =	{Geerts, Floris and Vandevoort, Brecht},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2023.18},
  URN =		{urn:nbn:de:0030-drops-177602},
  doi =		{10.4230/LIPIcs.ICDT.2023.18},
  annote =	{Keywords: existential rules, TGDs, cliquewidth, treewidth, bounded-treewidth sets, finite-unification sets, first-order rewritability, monadic second-order logic, datalog}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2021.120
Datalog-Expressibility for Monadic and Guarded Second-Order Logic

Authors: Manuel Bodirsky, Simon Knäuer, and Sebastian Rudolph

Published in: LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)

Abstract
We characterise the sentences in Monadic Second-order Logic (MSO) that are over finite structures equivalent to a Datalog program, in terms of an existential pebble game. We also show that for every class C of finite structures that can be expressed in MSO and is closed under homomorphisms, and for all 𝓁,k ∈ , there exists a canonical Datalog program Π of width (𝓁,k), that is, a Datalog program of width (𝓁,k) which is sound for C (i.e., Π only derives the goal predicate on a finite structure 𝔄 if 𝔄 ∈ C) and with the property that Π derives the goal predicate whenever some Datalog program of width (𝓁,k) which is sound for C derives the goal predicate. The same characterisations also hold for Guarded Second-order Logic (GSO), which properly extends MSO. To prove our results, we show that every class C in GSO whose complement is closed under homomorphisms is a finite union of constraint satisfaction problems (CSPs) of ω-categorical structures.
Cite as

Manuel Bodirsky, Simon Knäuer, and Sebastian Rudolph. Datalog-Expressibility for Monadic and Guarded Second-Order Logic. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 120:1-120:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{bodirsky_et_al:LIPIcs.ICALP.2021.120,
  author =	{Bodirsky, Manuel and Kn\"{a}uer, Simon and Rudolph, Sebastian},
  title =	{{Datalog-Expressibility for Monadic and Guarded Second-Order Logic}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{120:1--120:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-195-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{198},
  editor =	{Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.120},
  URN =		{urn:nbn:de:0030-drops-141897},
  doi =		{10.4230/LIPIcs.ICALP.2021.120},
  annote =	{Keywords: Monadic Second-order Logic, Guarded Second-order Logic, Datalog, constraint satisfaction, homomorphism-closed, conjunctive query, primitive positive formula, pebble game, \omega-categoricity}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.ICDT.2019.3
The Power of the Terminating Chase (Invited Talk)

Authors: Markus Krötzsch, Maximilian Marx, and Sebastian Rudolph

Published in: LIPIcs, Volume 127, 22nd International Conference on Database Theory (ICDT 2019)

Abstract
The chase has become a staple of modern database theory with applications in data integration, query optimisation, data exchange, ontology-based query answering, and many other areas. Most application scenarios and implementations require the chase to terminate and produce a finite universal model, and a large arsenal of sufficient termination criteria is available to guarantee this (generally undecidable) condition. In this invited tutorial, we therefore ask about the expressive power of logical theories for which the chase terminates. Specifically, which database properties can be recognised by such theories, i.e., which Boolean queries can they realise? For the skolem (semi-oblivious) chase, and almost any known termination criterion, this expressivity is just that of plain Datalog. Surprisingly, this limitation of most prior research does not apply to the chase in general. Indeed, we show that standard - chase terminating theories can realise queries with data complexities ranging from PTime to non-elementary that are out of reach for the terminating skolem chase. A "Datalog-first" standard chase that prioritises applications of rules without existential quantifiers makes modelling simpler - and we conjecture: computationally more efficient. This is one of the many open questions raised by our insights, and we conclude with an outlook on the research opportunities in this area.
Cite as

Markus Krötzsch, Maximilian Marx, and Sebastian Rudolph. The Power of the Terminating Chase (Invited Talk). In 22nd International Conference on Database Theory (ICDT 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 127, pp. 3:1-3:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{krotzsch_et_al:LIPIcs.ICDT.2019.3,
  author =	{Kr\"{o}tzsch, Markus and Marx, Maximilian and Rudolph, Sebastian},
  title =	{{The Power of the Terminating Chase}},
  booktitle =	{22nd International Conference on Database Theory (ICDT 2019)},
  pages =	{3:1--3:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-101-6},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{127},
  editor =	{Barcelo, Pablo and Calautti, Marco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2019.3},
  URN =		{urn:nbn:de:0030-drops-103057},
  doi =		{10.4230/LIPIcs.ICDT.2019.3},
  annote =	{Keywords: Existential rules, Tuple-generating dependencies, all-instances chase termination, expressive power, data complexity}
}
Document
DOI: 10.4230/LIPIcs.ICDT.2018.12
Preserving Constraints with the Stable Chase

Authors: David Carral, Markus Krötzsch, Maximilian Marx, Ana Ozaki, and Sebastian Rudolph

Published in: LIPIcs, Volume 98, 21st International Conference on Database Theory (ICDT 2018)

Abstract
Conjunctive query answering over databases with constraints – also known as (tuple-generating) dependencies – is considered a central database task. To this end, several versions of a construction called chase have been described. Given a set Sigma of dependencies, it is interesting to ask which constraints not contained in Sigma that are initially satisfied in a given database instance are preserved when computing a chase over Sigma. Such constraints are an example for the more general class of incidental constraints, which when added to Sigma as new dependencies do not affect certain answers and might even speed up query answering. After formally introducing incidental constraints, we show that deciding incidentality is undecidable for tuple-generating dependencies, even in cases for which query entailment is decidable. For dependency sets with a finite universal model, the core chase can be used to decide incidentality. For the infinite case, we propose the stable chase, which generalises the core chase, and study its relation to incidental constraints.
Cite as

David Carral, Markus Krötzsch, Maximilian Marx, Ana Ozaki, and Sebastian Rudolph. Preserving Constraints with the Stable Chase. In 21st International Conference on Database Theory (ICDT 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 98, pp. 12:1-12:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{carral_et_al:LIPIcs.ICDT.2018.12,
  author =	{Carral, David and Kr\"{o}tzsch, Markus and Marx, Maximilian and Ozaki, Ana and Rudolph, Sebastian},
  title =	{{Preserving Constraints with the Stable Chase}},
  booktitle =	{21st International Conference on Database Theory (ICDT 2018)},
  pages =	{12:1--12:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-063-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{98},
  editor =	{Kimelfeld, Benny and Amsterdamer, Yael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2018.12},
  URN =		{urn:nbn:de:0030-drops-86015},
  doi =		{10.4230/LIPIcs.ICDT.2018.12},
  annote =	{Keywords: Incidental constraints, Tuple-generating dependencies, Infinite core chase, Universal Model, BCQ entailment}
}
Document
DOI: 10.4230/DagSemProc.08091.3
Approximate OWL Instance Retrieval with SCREECH

Authors: Pascal Hitzler, Markus Krötzsch, Sebastian Rudolph, and Tuvshintur Tserendorj

Published in: Dagstuhl Seminar Proceedings, Volume 8091, Logic and Probability for Scene Interpretation (2008)

Abstract
With the increasing interest in expressive ontologies for the Semantic Web, it is critical to develop scalable and efficient ontology reasoning techniques that can properly cope with very high data volumes. For certain application domains, approximate reasoning solutions, which trade soundness or completeness for increased reasoning speed, will help to deal with the high computational complexities which state of the art ontology reasoning tools have to face. In this paper, we present a comprehensive overview of the SCREECH approach to approximate instance retrieval with OWL ontologies, which is based on the KAON2 algorithms, facilitating a compilation of OWL DL TBoxes into Datalog, which is tractable in terms of data complexity. We present three different instantiations of the Screech approach, and report on experiments which show that the gain in efficiency outweighs the number of introduced mistakes in the reasoning process.
Cite as

Pascal Hitzler, Markus Krötzsch, Sebastian Rudolph, and Tuvshintur Tserendorj. Approximate OWL Instance Retrieval with SCREECH. In Logic and Probability for Scene Interpretation. Dagstuhl Seminar Proceedings, Volume 8091, pp. 1-8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{hitzler_et_al:DagSemProc.08091.3,
  author =	{Hitzler, Pascal and Kr\"{o}tzsch, Markus and Rudolph, Sebastian and Tserendorj, Tuvshintur},
  title =	{{Approximate OWL Instance Retrieval with SCREECH}},
  booktitle =	{Logic and Probability for Scene Interpretation},
  pages =	{1--8},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8091},
  editor =	{Anthony G. Cohn and David C. Hogg and Ralf M\"{o}ller and Bernd Neumann},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.08091.3},
  URN =		{urn:nbn:de:0030-drops-16157},
  doi =		{10.4230/DagSemProc.08091.3},
  annote =	{Keywords: Description logics, automated reasoning, approximate reasoning, Horn logic}
}
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