Search Results

Documents authored by Zeume, Thomas

Document
DOI: 10.4230/LIPIcs.MFCS.2024.46
Query Maintenance Under Batch Changes with Small-Depth Circuits

Authors: Samir Datta, Asif Khan, Anish Mukherjee, Felix Tschirbs, Nils Vortmeier, and Thomas Zeume

Published in: LIPIcs, Volume 306, 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)

Abstract
Which dynamic queries can be maintained efficiently? For constant-size changes, it is known that constant-depth circuits or, equivalently, first-order updates suffice for maintaining many important queries, among them reachability, tree isomorphism, and the word problem for context-free languages. In other words, these queries are in the dynamic complexity class DynFO. We show that most of the existing results for constant-size changes can be recovered for batch changes of polylogarithmic size if one allows circuits of depth 𝒪(log log n) or, equivalently, first-order updates that are iterated 𝒪(log log n) times.
Cite as

Samir Datta, Asif Khan, Anish Mukherjee, Felix Tschirbs, Nils Vortmeier, and Thomas Zeume. Query Maintenance Under Batch Changes with Small-Depth Circuits. In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 306, pp. 46:1-46:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{datta_et_al:LIPIcs.MFCS.2024.46,
  author =	{Datta, Samir and Khan, Asif and Mukherjee, Anish and Tschirbs, Felix and Vortmeier, Nils and Zeume, Thomas},
  title =	{{Query Maintenance Under Batch Changes with Small-Depth Circuits}},
  booktitle =	{49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)},
  pages =	{46:1--46:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-335-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{306},
  editor =	{Kr\'{a}lovi\v{c}, Rastislav and Ku\v{c}era, Anton{\'\i}n},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2024.46},
  URN =		{urn:nbn:de:0030-drops-206027},
  doi =		{10.4230/LIPIcs.MFCS.2024.46},
  annote =	{Keywords: Dynamic complexity theory, parallel computation, dynamic algorithms}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2024.56
Specification and Automatic Verification of Computational Reductions

Authors: Julien Grange, Fabian Vehlken, Nils Vortmeier, and Thomas Zeume

Published in: LIPIcs, Volume 306, 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)

Abstract
We are interested in the following validation problem for computational reductions: for algorithmic problems P and P^⋆, is a given candidate reduction indeed a reduction from P to P^⋆? Unsurprisingly, this problem is undecidable even for very restricted classes of reductions. This leads to the question: Is there a natural, expressive class of reductions for which the validation problem can be attacked algorithmically? We answer this question positively by introducing an easy-to-use graphical specification mechanism for computational reductions, called cookbook reductions. We show that cookbook reductions are sufficiently expressive to cover many classical graph reductions and expressive enough so that SAT remains NP-complete (in the presence of a linear order). Surprisingly, the validation problem is decidable for natural and expressive subclasses of cookbook reductions.
Cite as

Julien Grange, Fabian Vehlken, Nils Vortmeier, and Thomas Zeume. Specification and Automatic Verification of Computational Reductions. In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 306, pp. 56:1-56:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{grange_et_al:LIPIcs.MFCS.2024.56,
  author =	{Grange, Julien and Vehlken, Fabian and Vortmeier, Nils and Zeume, Thomas},
  title =	{{Specification and Automatic Verification of Computational Reductions}},
  booktitle =	{49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)},
  pages =	{56:1--56:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-335-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{306},
  editor =	{Kr\'{a}lovi\v{c}, Rastislav and Ku\v{c}era, Anton{\'\i}n},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2024.56},
  URN =		{urn:nbn:de:0030-drops-206122},
  doi =		{10.4230/LIPIcs.MFCS.2024.56},
  annote =	{Keywords: Computational reductions, automatic verification, decidability}
}
Document
DOI: 10.4230/LIPIcs.CSL.2023.35
Dynamic Complexity of Regular Languages: Big Changes, Small Work

Authors: Felix Tschirbs, Nils Vortmeier, and Thomas Zeume

Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)

Abstract
Whether a changing string is member of a certain regular language can be maintained in the DynFO framework of Patnaik and Immerman: after changing the symbol at one position of the string, a first-order update formula can express - using additionally stored information - whether the resulting string is in the regular language. We extend this and further known results by considering changes of many positions at once. We also investigate to which degree the obtained update formulas imply work-efficient parallel dynamic algorithms.
Cite as

Felix Tschirbs, Nils Vortmeier, and Thomas Zeume. Dynamic Complexity of Regular Languages: Big Changes, Small Work. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 35:1-35:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{tschirbs_et_al:LIPIcs.CSL.2023.35,
  author =	{Tschirbs, Felix and Vortmeier, Nils and Zeume, Thomas},
  title =	{{Dynamic Complexity of Regular Languages: Big Changes, Small Work}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{35:1--35:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.35},
  URN =		{urn:nbn:de:0030-drops-174963},
  doi =		{10.4230/LIPIcs.CSL.2023.35},
  annote =	{Keywords: dynamic descriptive complexity, regular languages, batch changes, work}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2020.122
Dynamic Complexity of Reachability: How Many Changes Can We Handle?

Authors: Samir Datta, Pankaj Kumar, Anish Mukherjee, Anuj Tawari, Nils Vortmeier, and Thomas Zeume

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

Abstract
In 2015, it was shown that reachability for arbitrary directed graphs can be updated by first-order formulas after inserting or deleting single edges. Later, in 2018, this was extended for changes of size (log n)/(log log n), where n is the size of the graph. Changes of polylogarithmic size can be handled when also majority quantifiers may be used. In this paper we extend these results by showing that, for changes of polylogarithmic size, first-order update formulas suffice for maintaining (1) undirected reachability, and (2) directed reachability under insertions. For classes of directed graphs for which efficient parallel algorithms can compute non-zero circulation weights, reachability can be maintained with update formulas that may use "modulo 2" quantifiers under changes of polylogarithmic size. Examples for these classes include the class of planar graphs and graphs with bounded treewidth. The latter is shown here. As the logics we consider cannot maintain reachability under changes of larger sizes, our results are optimal with respect to the size of the changes.
Cite as

Samir Datta, Pankaj Kumar, Anish Mukherjee, Anuj Tawari, Nils Vortmeier, and Thomas Zeume. Dynamic Complexity of Reachability: How Many Changes Can We Handle?. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 122:1-122:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{datta_et_al:LIPIcs.ICALP.2020.122,
  author =	{Datta, Samir and Kumar, Pankaj and Mukherjee, Anish and Tawari, Anuj and Vortmeier, Nils and Zeume, Thomas},
  title =	{{Dynamic Complexity of Reachability: How Many Changes Can We Handle?}},
  booktitle =	{47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
  pages =	{122:1--122:19},
  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.122},
  URN =		{urn:nbn:de:0030-drops-125291},
  doi =		{10.4230/LIPIcs.ICALP.2020.122},
  annote =	{Keywords: Dynamic complexity, reachability, complex changes}
}
Document
DOI: 10.4230/LIPIcs.CSL.2020.36
Dynamic Complexity Meets Parameterised Algorithms

Authors: Jonas Schmidt, Thomas Schwentick, Nils Vortmeier, Thomas Zeume, and Ioannis Kokkinis

Published in: LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)

Abstract
Dynamic Complexity studies the maintainability of queries with logical formulas in a setting where the underlying structure or database changes over time. Most often, these formulas are from first-order logic, giving rise to the dynamic complexity class DynFO. This paper investigates extensions of DynFO in the spirit of parameterised algorithms. In this setting structures come with a parameter k and the extensions allow additional "space" of size f(k) (in the form of an additional structure of this size) or additional time f(k) (in the form of iterations of formulas) or both. The resulting classes are compared with their non-dynamic counterparts and other classes. The main part of the paper explores the applicability of methods for parameterised algorithms to this setting through case studies for various well-known parameterised problems.
Cite as

Jonas Schmidt, Thomas Schwentick, Nils Vortmeier, Thomas Zeume, and Ioannis Kokkinis. Dynamic Complexity Meets Parameterised Algorithms. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 36:1-36:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{schmidt_et_al:LIPIcs.CSL.2020.36,
  author =	{Schmidt, Jonas and Schwentick, Thomas and Vortmeier, Nils and Zeume, Thomas and Kokkinis, Ioannis},
  title =	{{Dynamic Complexity Meets Parameterised Algorithms}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{36:1--36:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-132-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{152},
  editor =	{Fern\'{a}ndez, Maribel 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.CSL.2020.36},
  URN =		{urn:nbn:de:0030-drops-116792},
  doi =		{10.4230/LIPIcs.CSL.2020.36},
  annote =	{Keywords: Dynamic complexity, parameterised complexity}
}
Document
DOI: 10.4230/LIPIcs.CSL.2020.37
Dynamic Complexity of Parity Exists Queries

Authors: Nils Vortmeier and Thomas Zeume

Published in: LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)

Abstract
Given a graph whose nodes may be coloured red, the parity of the number of red nodes can easily be maintained with first-order update rules in the dynamic complexity framework DynFO of Patnaik and Immerman. Can this be generalised to other or even all queries that are definable in first-order logic extended by parity quantifiers? We consider the query that asks whether the number of nodes that have an edge to a red node is odd. Already this simple query of quantifier structure parity-exists is a major roadblock for dynamically capturing extensions of first-order logic. We show that this query cannot be maintained with quantifier-free first-order update rules, and that variants induce a hierarchy for such update rules with respect to the arity of the maintained auxiliary relations. Towards maintaining the query with full first-order update rules, it is shown that degree-restricted variants can be maintained.
Cite as

Nils Vortmeier and Thomas Zeume. Dynamic Complexity of Parity Exists Queries. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 37:1-37:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{vortmeier_et_al:LIPIcs.CSL.2020.37,
  author =	{Vortmeier, Nils and Zeume, Thomas},
  title =	{{Dynamic Complexity of Parity Exists Queries}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{37:1--37:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-132-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{152},
  editor =	{Fern\'{a}ndez, Maribel 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.CSL.2020.37},
  URN =		{urn:nbn:de:0030-drops-116805},
  doi =		{10.4230/LIPIcs.CSL.2020.37},
  annote =	{Keywords: Dynamic complexity, parity quantifier, arity hierarchy}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2018.120
Reachability and Distances under Multiple Changes

Authors: Samir Datta, Anish Mukherjee, Nils Vortmeier, and Thomas Zeume

Published in: LIPIcs, Volume 107, 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)

Abstract
Recently it was shown that the transitive closure of a directed graph can be updated using first-order formulas after insertions and deletions of single edges in the dynamic descriptive complexity framework by Dong, Su, and Topor, and Patnaik and Immerman. In other words, Reachability is in DynFO. In this article we extend the framework to changes of multiple edges at a time, and study the Reachability and Distance queries under these changes. We show that the former problem can be maintained in DynFO(+, x) under changes affecting O({log n}/{log log n}) nodes, for graphs with n nodes. If the update formulas may use a majority quantifier then both Reachability and Distance can be maintained under changes that affect O(log^c n) nodes, for fixed c in N. Some preliminary results towards showing that distances are in DynFO are discussed.
Cite as

Samir Datta, Anish Mukherjee, Nils Vortmeier, and Thomas Zeume. Reachability and Distances under Multiple Changes. In 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 107, pp. 120:1-120:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{datta_et_al:LIPIcs.ICALP.2018.120,
  author =	{Datta, Samir and Mukherjee, Anish and Vortmeier, Nils and Zeume, Thomas},
  title =	{{Reachability and Distances under Multiple Changes}},
  booktitle =	{45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)},
  pages =	{120:1--120:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-076-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{107},
  editor =	{Chatzigiannakis, Ioannis and Kaklamanis, Christos and Marx, D\'{a}niel and Sannella, Donald},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2018.120},
  URN =		{urn:nbn:de:0030-drops-91245},
  doi =		{10.4230/LIPIcs.ICALP.2018.120},
  annote =	{Keywords: dynamic complexity, reachability, distances, complex changes}
}
Document
DOI: 10.4230/LIPIcs.ICDT.2018.3
An Update on Dynamic Complexity Theory

Authors: Thomas Zeume

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

Abstract
In many modern data management scenarios, data is subject to frequent changes. In order to avoid costly re-computing query answers from scratch after each small update, one can try to use auxiliary relations that have been computed before. Of course, the auxiliary relations need to be updated dynamically whenever the data changes. Dynamic complexity theory studies which queries and auxiliary relations can be updated in a highly parallel fashion, that is, by constant-depth circuits or, equivalently, by first-order formulas or the relational algebra. After gently introducing dynamic complexity theory, I will discuss recent results of the area with a focus on the dynamic complexity of the reachability query.
Cite as

Thomas Zeume. An Update on Dynamic Complexity Theory. In 21st International Conference on Database Theory (ICDT 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 98, p. 3:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{zeume:LIPIcs.ICDT.2018.3,
  author =	{Zeume, Thomas},
  title =	{{An Update on Dynamic Complexity Theory}},
  booktitle =	{21st International Conference on Database Theory (ICDT 2018)},
  pages =	{3:1--3:1},
  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.3},
  URN =		{urn:nbn:de:0030-drops-86117},
  doi =		{10.4230/LIPIcs.ICDT.2018.3},
  annote =	{Keywords: Dynamic descriptive complexity, SQL updates, Reachability}
}
Document
DOI: 10.4230/LIPIcs.ICDT.2018.7
A More General Theory of Static Approximations for Conjunctive Queries

Authors: Pablo Barceló, Miguel Romero, and Thomas Zeume

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

Abstract
Conjunctive query (CQ) evaluation is NP-complete, but becomes tractable for fragments of bounded hypertreewidth. If a CQ is hard to evaluate, it is thus useful to evaluate an approximation of it in such fragments. While underapproximations (i.e., those that return correct answers only) are well-understood, the dual notion of overapproximations that return complete (but not necessarily sound) answers, and also a more general notion of approximation based on the symmetric difference of query results, are almost unexplored. In fact, the decidability of the basic problems of evaluation, identification, and existence of those approximations, is open. We develop a connection with existential pebble game tools that allows the systematic study of such problems. In particular, we show that the evaluation and identification of overapproximations can be solved in polynomial time. We also make progress in the problem of existence of overapproximations, showing it to be decidable in 2EXPTIME over the class of acyclic CQs. Furthermore, we look at when overapproximations do not exist, suggesting that this can be alleviated by using a more liberal notion of overapproximation. We also show how to extend our tools to study symmetric difference approximations. We observe that such approximations properly extend under- and over-approximations, settle the complexity of its associated identification problem, and provide several results on existence and evaluation.
Cite as

Pablo Barceló, Miguel Romero, and Thomas Zeume. A More General Theory of Static Approximations for Conjunctive Queries. In 21st International Conference on Database Theory (ICDT 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 98, pp. 7:1-7:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{barcelo_et_al:LIPIcs.ICDT.2018.7,
  author =	{Barcel\'{o}, Pablo and Romero, Miguel and Zeume, Thomas},
  title =	{{A More General Theory of Static Approximations for Conjunctive Queries}},
  booktitle =	{21st International Conference on Database Theory (ICDT 2018)},
  pages =	{7:1--7:22},
  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.7},
  URN =		{urn:nbn:de:0030-drops-86021},
  doi =		{10.4230/LIPIcs.ICDT.2018.7},
  annote =	{Keywords: conjunctive queries, hypertreewidth, approximations, pebble games}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2017.98
A Strategy for Dynamic Programs: Start over and Muddle Through

Authors: Samir Datta, Anish Mukherjee, Thomas Schwentick, Nils Vortmeier, and Thomas Zeume

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

Abstract
A strategy for constructing dynamic programs is introduced that utilises periodic computation of auxiliary data from scratch and the ability to maintain a query for a limited number of change steps. It is established that if some program can maintain a query for log n change steps after an AC^1-computable initialisation, it can be maintained by a first-order dynamic program as well, i.e., in DynFO. As an application, it is shown that decision and optimisation problems defined by monadic second-order (MSO) and guarded second-order logic (GSO) formulas are in DynFO, if only change sequences that produce graphs of bounded treewidth are allowed. To establish this result, Feferman-Vaught-type composition theorems for MSO and GSO are established that might be useful in their own right.
Cite as

Samir Datta, Anish Mukherjee, Thomas Schwentick, Nils Vortmeier, and Thomas Zeume. A Strategy for Dynamic Programs: Start over and Muddle Through. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 98:1-98:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{datta_et_al:LIPIcs.ICALP.2017.98,
  author =	{Datta, Samir and Mukherjee, Anish and Schwentick, Thomas and Vortmeier, Nils and Zeume, Thomas},
  title =	{{A Strategy for Dynamic Programs: Start over and Muddle Through}},
  booktitle =	{44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)},
  pages =	{98:1--98: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.98},
  URN =		{urn:nbn:de:0030-drops-74470},
  doi =		{10.4230/LIPIcs.ICALP.2017.98},
  annote =	{Keywords: dynamic complexity, treewidth, monadic second order logic}
}
Document
DOI: 10.4230/LIPIcs.ICDT.2017.19
Dynamic Complexity under Definable Changes

Authors: Thomas Schwentick, Nils Vortmeier, and Thomas Zeume

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

Abstract
This paper studies dynamic complexity under definable change operations in the DynFO framework by Patnaik and Immerman. It is shown that for changes definable by parameter-free first-order formulas, all (uniform) AC1 queries can be maintained by first-order dynamic programs. Furthermore, many maintenance results for single-tuple changes are extended to more powerful change operations: (1) The reachability query for undirected graphs is first-order maintainable under single tuple changes and first-order defined insertions, likewise the reachability query for directed acyclic graphs under quantifier-free insertions. (2) Context-free languages are first-order maintainable under \EFO-defined changes. These results are complemented by several inexpressibility results, for example, that the reachability query cannot be maintained by quantifier-free programs under definable, quantifier-free deletions.
Cite as

Thomas Schwentick, Nils Vortmeier, and Thomas Zeume. Dynamic Complexity under Definable Changes. In 20th International Conference on Database Theory (ICDT 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 68, pp. 19:1-19:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{schwentick_et_al:LIPIcs.ICDT.2017.19,
  author =	{Schwentick, Thomas and Vortmeier, Nils and Zeume, Thomas},
  title =	{{Dynamic Complexity under Definable Changes}},
  booktitle =	{20th International Conference on Database Theory (ICDT 2017)},
  pages =	{19:1--19:18},
  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.19},
  URN =		{urn:nbn:de:0030-drops-70596},
  doi =		{10.4230/LIPIcs.ICDT.2017.19},
  annote =	{Keywords: dynamic descriptive complexity, SQL updates, dynamic programs}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.ICDT.2016
LIPIcs, Volume 48, ICDT'16, Complete Volume

Authors: Wim Martens and Thomas Zeume

Published in: LIPIcs, Volume 48, 19th International Conference on Database Theory (ICDT 2016)

Abstract
LIPIcs, Volume 48, ICDT'16, Complete Volume
Cite as

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

Copy BibTex To Clipboard

@Proceedings{martens_et_al:LIPIcs.ICDT.2016,
  title =	{{LIPIcs, Volume 48, ICDT'16, Complete Volume}},
  booktitle =	{19th International Conference on Database Theory (ICDT 2016)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-002-6},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{48},
  editor =	{Martens, Wim and Zeume, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2016},
  URN =		{urn:nbn:de:0030-drops-57991},
  doi =		{10.4230/LIPIcs.ICDT.2016},
  annote =	{Keywords: Database Management, Normal forms, Schema and subschema, Query languages, Query processing, Relational databases, Distributed databases, Heterogeneous Databases, Online Information Services,Miscellaneous – Privacy, Office Automation: Workflow management}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.ICDT.2016.0
Front Matter, Table of Contents, Preface, Conference Organization, External Reviewers, List of Authors

Authors: Wim Martens and Thomas Zeume

Published in: LIPIcs, Volume 48, 19th International Conference on Database Theory (ICDT 2016)

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

19th International Conference on Database Theory (ICDT 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 48, pp. 0:i-0:xvi, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{martens_et_al:LIPIcs.ICDT.2016.0,
  author =	{Martens, Wim and Zeume, Thomas},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization, External Reviewers, List of Authors}},
  booktitle =	{19th International Conference on Database Theory (ICDT 2016)},
  pages =	{0:i--0:xvi},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-002-6},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{48},
  editor =	{Martens, Wim and Zeume, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2016.0},
  URN =		{urn:nbn:de:0030-drops-57940},
  doi =		{10.4230/LIPIcs.ICDT.2016.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization, External Reviewers, List of Authors}
}
Document
DOI: 10.4230/LIPIcs.ICDT.2016.14
Dynamic Graph Queries

Authors: Pablo Muñoz, Nils Vortmeier, and Thomas Zeume

Published in: LIPIcs, Volume 48, 19th International Conference on Database Theory (ICDT 2016)

Abstract
Graph databases in many applications - semantic web, transport or biological networks among others - are not only large, but also frequently modified. Evaluating graph queries in this dynamic context is a challenging task, as those queries often combine first-order and navigational features. Motivated by recent results on maintaining dynamic reachability, we study the dynamic evaluation of traditional query languages for graphs in the descriptive complexity framework. Our focus is on maintaining regular path queries, and extensions thereof, by first-order formulas. In particular we are interested in path queries defined by non-regular languages and in extended conjunctive regular path queries (which allow to compare labels of paths based on word relations). Further we study the closely related problems of maintaining distances in graphs and reachability in product graphs. In this preliminary study we obtain upper bounds for those problems in restricted settings, such as undirected and acyclic graphs, or under insertions only, and negative results regarding quantifier-free update formulas. In addition we point out interesting directions for further research.
Cite as

Pablo Muñoz, Nils Vortmeier, and Thomas Zeume. Dynamic Graph Queries. In 19th International Conference on Database Theory (ICDT 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 48, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{munoz_et_al:LIPIcs.ICDT.2016.14,
  author =	{Mu\~{n}oz, Pablo and Vortmeier, Nils and Zeume, Thomas},
  title =	{{Dynamic Graph Queries}},
  booktitle =	{19th International Conference on Database Theory (ICDT 2016)},
  pages =	{14:1--14:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-002-6},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{48},
  editor =	{Martens, Wim and Zeume, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2016.14},
  URN =		{urn:nbn:de:0030-drops-57830},
  doi =		{10.4230/LIPIcs.ICDT.2016.14},
  annote =	{Keywords: Dynamic descriptive complexity, graph databases, graph products, reachability, path queries}
}
Document
DOI: 10.4230/LIPIcs.CSL.2015.308
Static Analysis for Logic-based Dynamic Programs

Authors: Thomas Schwentick, Nils Vortmeier, and Thomas Zeume

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

Abstract
The goal of dynamic programs as introduced by Patnaik and Immerman (1994) is to maintain the result of a fixed query for an input database which is subject to tuple insertions and deletions. To this end such programs store an auxiliary database whose relations are updated via first-order formulas upon modifications of the input database. One of those auxiliary relations is supposed to store the answer to the query. Several static analysis problems can be associated to such dynamic programs. Is the answer relation of a given dynamic program always empty? Does a program actually maintain a query? That is, is the answer given of the program the same when an input database was reached by two different modification sequences? Even more, is the content of auxiliary relations independent of the modification sequence that lead to an input database? We study the algorithmic properties of those and similar static analysis problems. Since all these problems can easily be seen to be undecidable for full first-order programs, we examine the exact borderline for decidability for restricted programs. Our focus is on restricting the arity of the input databases as well as the auxiliary databases, and to restrict the use of quantifiers.
Cite as

Thomas Schwentick, Nils Vortmeier, and Thomas Zeume. Static Analysis for Logic-based Dynamic Programs. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 308-324, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{schwentick_et_al:LIPIcs.CSL.2015.308,
  author =	{Schwentick, Thomas and Vortmeier, Nils and Zeume, Thomas},
  title =	{{Static Analysis for Logic-based Dynamic Programs}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{308--324},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.308},
  URN =		{urn:nbn:de:0030-drops-54221},
  doi =		{10.4230/LIPIcs.CSL.2015.308},
  annote =	{Keywords: Dynamic descriptive complexity, algorithmic problems, emptiness, history independence, consistency}
}
Document
DOI: 10.4230/LIPIcs.CSL.2013.484
Two-Variable Logic on 2-Dimensional Structures

Authors: Amaldev Manuel and Thomas Zeume

Published in: LIPIcs, Volume 23, Computer Science Logic 2013 (CSL 2013)

Abstract
This paper continues the study of the two-variable fragment of first-order logic (FO^2) over two- dimensional structures, more precisely structures with two orders, their induced successor relations and arbitrarily many unary relations. Our main focus is on ordered data words which are finite sequences from the set \Sigma x D where \Sigma is a finite alphabet and D is an ordered domain. These are naturally represented as labelled finite sets with a linear order <=_l and a total preorder <=_p. We introduce ordered data automata, an automaton model for ordered data words. An ordered data automaton is a composition of a finite state transducer and a finite state automaton over the product Boolean algebra of finite and cofinite subsets of N. We show that ordered data automata are equivalent to the closure of FO^2(+1_l,<=_p,+1_p) under existential quantification of unary relations. Using this automaton model we prove that the finite satisfiability problem for this logic is decidable on structures where the <=_p-equivalence classes are of bounded size. As a corollary, we obtain that finite satisfiability of FO^2 is decidable (and it is equivalent to the reachability problem of vector addition systems) on structures with two linear order successors and a linear order corresponding to one of the successors. Further we prove undecidability of FO^2 on several other two-dimensional structures.
Cite as

Amaldev Manuel and Thomas Zeume. Two-Variable Logic on 2-Dimensional Structures. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 484-499, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{manuel_et_al:LIPIcs.CSL.2013.484,
  author =	{Manuel, Amaldev and Zeume, Thomas},
  title =	{{Two-Variable Logic on 2-Dimensional Structures}},
  booktitle =	{Computer Science Logic 2013 (CSL 2013)},
  pages =	{484--499},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Ronchi Della Rocca, Simona},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.484},
  URN =		{urn:nbn:de:0030-drops-42159},
  doi =		{10.4230/LIPIcs.CSL.2013.484},
  annote =	{Keywords: FO2, Data words, Satisfiability, Decidability, Automata}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2010.481
Temporal Logics on Words with Multiple Data Values

Authors: Ahmet Kara, Thomas Schwentick, and Thomas Zeume

Published in: LIPIcs, Volume 8, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)

Abstract
The paper proposes and studies temporal logics for attributed words, that is, data words with a (finite) set of (attribute,value)-pairs at each position. It considers a basic logic which is a semantical fragment of the logic $\LTL^\downarrow_1$ of Demri and Lazic with operators for navigation into the future and the past. By reduction to the emptiness problem for data automata it is shown that this basic logic is decidable. Whereas the basic logic only allows navigation to positions where a fixed data value occurs, extensions are studied that also allow navigation to positions with different data values. Besides some undecidable results it is shown that the extension by a certain UNTIL-operator with an inequality target condition remains decidable.
Cite as

Ahmet Kara, Thomas Schwentick, and Thomas Zeume. Temporal Logics on Words with Multiple Data Values. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 481-492, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{kara_et_al:LIPIcs.FSTTCS.2010.481,
  author =	{Kara, Ahmet and Schwentick, Thomas and Zeume, Thomas},
  title =	{{Temporal Logics on Words with Multiple Data Values}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{481--492},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-23-1},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{8},
  editor =	{Lodaya, Kamal and Mahajan, Meena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2010.481},
  URN =		{urn:nbn:de:0030-drops-28883},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.481},
  annote =	{Keywords: Expressiveness, Decidability, Temporal Logic, Data words}
}
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