Thomas Zeume

Highlights Conference 2025 Conference Abstract

Learning Formal Foundations of Computer Science with Iltis

• Thomas Zeume

MFCS Conference 2024 Conference Paper

Query Maintenance Under Batch Changes with Small-Depth Circuits

• Samir Datta
• Asif Khan 0009
• Anish Mukherjee 0001
• Felix Tschirbs
• Nils Vortmeier
• Thomas Zeume

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.

MFCS Conference 2024 Conference Paper

Specification and Automatic Verification of Computational Reductions

• Julien Grange
• Fabian Vehlken
• Nils Vortmeier
• Thomas Zeume

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.

CSL Conference 2023 Conference Paper

Dynamic Complexity of Regular Languages: Big Changes, Small Work

• Felix Tschirbs
• Nils Vortmeier
• Thomas Zeume

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.

CSL Conference 2020 Conference Paper

Dynamic Complexity Meets Parameterised Algorithms

• Jonas Schmidt 0001
• Thomas Schwentick
• Nils Vortmeier
• Thomas Zeume
• Ioannis Kokkinis

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.

CSL Conference 2020 Conference Paper

Dynamic Complexity of Parity Exists Queries

• Nils Vortmeier
• Thomas Zeume

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.

KR Conference 2020 Conference Paper

On the Decidability of Expressive Description Logics with Transitive Closure and Regular Role Expressions

• Jean Christoph Jung
• Carsten Lutz
• Thomas Zeume

We consider fragments of the description logic SHOIF extended with regular expressions on roles. Our main result is that satisfiability and finite satisfiability are decidable in two fragments SHOIF^1 and SHOIF^2, NExpTime-complete for the former and in 2NExpTime for the more expressive latter fragment. Both fragments impose restrictions on regular role expressions of the form r*. SHOIF^1 encompasses the extension of SHOIF with transitive closure of roles (when functional roles have no subroles) and the modal logic of linear orders and successor, with converse. Consequently, these logics are also decidable and NExpTime-complete.

Highlights Conference 2020 Conference Abstract

Teaching Logic with Iltis: an Interactive, Web-Based System

• Thomas Zeume

The Iltis project provides an interactive, web-based system for teaching logic, which is designed to provide immediate and comprehensive feedback for exercises covering various aspects of the reasoning workflow of propositional logic, modal logic, and first-order logic. In this talk I will provide an update on the status of the project.

Highlights Conference 2018 Conference Abstract

Introduction to Iltis: An Interactive, Web-Based System for Teaching Logic

• Thomas Zeume

ABSTRACT. The Iltis project aims at providing a web-based, interactive system that supports teaching logical methods. In particular the system shall (a) support to learn to model knowledge and to infer new knowledge using propositional logic, modal logic and first-order logic, and (b) provide immediate feedback and support to students. The current prototype supports the above tasks for propositional logic. In this talk I will present the status of the project, outline arising theoretical questions, and report on first impressions on using the prototype in a second year logic course for computer science students. The talk is based on joined work with Gaetano Geck, Artur Ljulin, Sebastian Peter, Jonas Schmidt, and Fabian Vehlken.

I&C Journal 2017 Journal Article

The dynamic descriptive complexity of k -clique

• Thomas Zeume

In this work the dynamic descriptive complexity of the k-clique query is studied. It is shown that when edges may only be inserted then k-clique can be maintained by a quantifier-free update program of arity k − 1, but it cannot be maintained by a quantifier-free update program of arity k − 2 (even in the presence of unary auxiliary functions). This establishes an arity hierarchy for graph queries for quantifier-free update programs under insertions. The proof of the lower bound uses upper and lower bounds for Ramsey numbers.

Highlights Conference 2016 Conference Abstract

Dynamic descriptive complexity of FO-definable modifications

• Thomas Schwentick
• Nils Vortmeier
• Thomas Zeume

A dynamic program, as introduced by Dong, Su and Topor and Patnaik and Immerman, maintains the result of a fixed query for an input database which is subject to modifications. It can use an auxiliary database whose relations are updated via first-order formulas upon modifications of the input database. In the original setting, only insertions and deletions of single tuples are considered. In this talk, which is based on joint work with Thomas Schwentick and Thomas Zeume, we will allow modifications defined by (restricted) first-order formulas and review which queries can still be maintained. This talk is based on so far unpublished work.

I&C Journal 2015 Journal Article

On the quantifier-free dynamic complexity of Reachability

• Thomas Zeume
• Thomas Schwentick

The dynamic complexity of the reachability query is studied in the dynamic complexity framework of Patnaik and Immerman, restricted to quantifier-free update formulas. It is shown that, with this restriction, the reachability query cannot be dynamically maintained, neither with binary auxiliary relations nor with unary auxiliary functions, and that ternary auxiliary relations are more powerful with respect to graph queries than binary auxiliary relations. Further inexpressibility results are given for the reachability query in a different setting as well as for a syntactical restriction of quantifier-free update formulas. Moreover inexpressibility results for some other queries are presented.

Highlights Conference 2015 Conference Abstract

Reachability is in DynFO

• Thomas Zeume

A dynamic program, as introduced by Dong, Su Topor (1993) and Pat- naik and Immerman (1994), maintains a fixed query for an input database which is subject to tuple insertions and deletions. It can use an auxiliary database whose relations are updated via first-order formulas upon modi- fications of the input database. In this talk I will present how Reachability in directed graphs can be maintained in this fashion. This result confirms a two decade old conjecture of Patnaik and Immerman (1997). The talk is based on joint work with Samir Datta, Raghav Kulkarni, Anish Mukherjee and Thomas Schwentick.

CSL Conference 2015 Conference Paper

Static Analysis for Logic-based Dynamic Programs

• Thomas Schwentick
• Nils Vortmeier
• Thomas Zeume

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.

MFCS Conference 2013 Conference Paper

On the Quantifier-Free Dynamic Complexity of Reachability

• Thomas Zeume
• Thomas Schwentick

Abstract The dynamic complexity of the reachability query is studied in the dynamic complexity framework of Patnaik and Immerman, restricted to quantifier-free update formulas. It is shown that, with this restriction, the reachability query cannot be dynamically maintained, neither with binary auxiliary relations nor with unary auxiliary functions, and that ternary auxiliary relations are more powerful with respect to graph queries than binary auxiliary relations. Further results are obtained including more inexpressibility results for reachability in a different setting, inexpressibility results for some other queries and normal forms for quantifier-free update programs.

CSL Conference 2013 Conference Paper

Two-Variable Logic on 2-Dimensional Structures

• Amaldev Manuel
• Thomas Zeume

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.

CSL Conference 2010 Conference Paper

Two-Variable Logic with Two Order Relations - (Extended Abstract)

• Thomas Schwentick
• Thomas Zeume

Abstract The finite satisfiability problem for two-variable logic over structures with unary relations and two order relations is investigated. Firstly, decidability is shown for structures with one total preorder relation and one linear order relation. More specifically, we show that this problem is complete for EXPSPACE. As a consequence, the same upper bound applies to the case of two linear orders. Secondly, we prove undecidability for structures with two total preorder relations as well as for structures with one total preorder and two linear order relations. Further, we point out connections to other logics. Decidability is shown for two-variable logic on data words with orders on both positions and data values, but without a successor relation. We also study ”partial models” of compass and interval temporal logic and prove decidability for some of their fragments.

MFCS Conference 2009 Conference Paper

Bounds on Non-surjective Cellular Automata

• Jarkko Kari 0001
• Pascal Vanier
• Thomas Zeume

Abstract Cellular automata (CA) are discrete, homogeneous dynamical systems. Non-surjective one-dimensional CA have finite words with no preimage (called orphans ), pairs of different words starting and ending identically and having the same image ( diamonds ) and words with more/ fewer preimages than the average number ( unbalanced words). Using a linear algebra approach, we obtain new upper bounds on the lengths of the shortest such objects. In the case of an n -state, non-surjective CA with neighborhood range 2 our bounds are of the orders O ( n 2 ), O ( n 3/2 ) and O ( n ) for the shortest orphan, diamond and unbalanced word, respectively.