Seminar
Theory Seminar
Together with the Theoretical Computer Science / Complex Systems group from Uni Kassel (led by Stefan Göller) we organize the "Theory (Online) Seminar".Generally, the topics of this seminar are related to the areas of computer science logic, automata theory, string combinatorics and algorithms, formal verification, and data-base theory. The seminar started in November 2020, it is organized online, and it uses Zoom as streaming platform.
If you are interested in attending the seminar, please let us know by e-mail (to Florin Manea).
Future Talks
T.B.APast Talks
5.4.2022, 16:00 (s.t.) Thomas Colcombet (IRIF, Paris) -- Asymptotic complexity of tree algebras
I will describe some recent works obtained with Arthur Jaquard.
We study algebras of finite ranked trees. In our case, these algebras are extensions of monoids, in which the product (called in this case substitution) exists in different forms parameterised by the variable in which the operation is performed. This natural definition is infinitely sorted: the set of trees are indexed by the set of variables that may appear in them. Such algebras can be used to describe — formally recognise — languages of trees. For this, an algebra is used which describe the different situation of trees that need be distinguished for being able to recognise the language, yielding a set of elements for each set of variables, called the sort.
We began a study of the expressive power of such recognising algebras depending on the asymptotic size of each sort as a function of the number of variables. It is well known that a language of trees is regular if and only if it is recognised by an algebra that has all its sorts finite. In this case, an algebra of doubly exponential complexity can be constructed. In our case, we characterise the algebras of bounded and of polynomial complexity. The later class displays a surprising relationship with nominal automata (aka register automata/automata with atoms).
22.3.2022, 16:00 (s.t.) Laura Ciobanu (Heriot-Watt, Edinburgh) -- Equations in groups, formal languages and complexity
Solving word equations (in free monoids) is a rich and well-established area in theoretical computer science, In this talk I will introduce equations in groups, and draw parallels to word equations while discussing the challenges presented in the algebraic setting of groups.
I will give a short non-technical survey containing results from both mathematics and computer science about solving equations in (semi)groups, with emphasis on the free ones. In particular, I will explain that the solutions to equations can be beautifully described in terms of EDT0L languages, and that the (non-deterministic) space complexity is remarkably low even for groups arising in deep geometric settings. This is based on work with/of Volker Diekert, Murray Elder, Alex Evetts and Alex Levine.
8.3.2022, 16:00 (s.t.) Benedikt Bollig (Paris) -- Synthesis in Presence of Dynamic Links
In this talk, we consider the problem of distributed synthesis: Given a distributed system architecture and a logical specification, can we generate a distributed algorithm that satisfies the specification independently of the inputs that the system receives from the environment?
While previous work has focused on static architectures with an a priori fixed message size, we assume that the communication network changes dynamically and that processes piggy-pack previously received messages onto current messages.
Specifically, we address a system of two processes communicating in rounds over a dynamic link. Given a network model N, i.e., a set of link directions, an adversary picks, in each round, an arbitrary link from N. We show that the synthesis problem is decidable for N if and only if N does not contain the 'empty' link. We will also discuss some directions for future work.
This is joint work with Béatrice Bérard, Patricia Bouyer, Matthias Függer, and Nathalie Sznajder.
8.2.2022, 16:00 (s.t.) Anthony Lin (Kaiserslautern) -- 100 Facets of String Constraints
Strings crop up frequently and naturally in computer science. This explains the multitude of existing string constraint languages that independently arose in different subareas of computer science. In this talk, I will go through some of these languages that can be found in the SMT community, verification of parameterized systems community, graph database theory community, and if time permits also analysis of access control policies. In addition to going through several basic results on these string constraint languages (naturally unashamedly biased towards the problems I have worked on), I will pinpoint similarities and differences of these languages, and possible opportunities for "cross-fertilization". At the end of the talk, I will describe some challenges to extend these to "sequence constraints", where an element in the sequence could come from an infinite domain.
1.2.2022, 16:00 (s.t.) Amaldev Manuel (Indian Institute of Technology Goa) -- Algebraically characterising first-order logic with neighbour
We give an algebraic characterisation of first-order logic with the neighbour relation, on finite words. For this, we consider languages of finite words over alphabets with an involution on them. The natural algebras for such languages are involution semigroups. To characterise the logic, we define a special kind of semidirect product of involution semigroups, called the locally hermitian product. The characterisation theorem for FO with neighbour states that a language is definable in the logic if and only if it is recognised by a locally hermitian product of an aperiodic commutative involution semigroup, and a locally trivial involution semigroup.
We then define the notion of involution varieties of languages, namely classes of languages closed under Boolean operations, quotients, involution, and inverse images of involutory morphisms. An Eilenberg-type correspondence is established between involution varieties of languages and pseudovarieties of involution semigroups. This is joint work with Dhruv Nevatia.
18.1.2022, 16:00 (s.t.) Sebastian Siebertz (Bremen) -- First-Order Logic with Connectivity Operators: expressiveness and model-checking
Abstract available here.
23.11.2021, 16:00 (s.t.) Moses Ganardi (Kaiserslautern) -- Balancing straight-line programs
In grammar-based compression, a string is represented by a context-free grammar, also called a straight-line program (SLP), that generates only that string. The hierarchical structure of SLPs makes them amenable to algorithms that work directly on the compressed representation, without decompressing the string first. I will present a recent balancing result stating that one can transform an SLP of size g in linear time into an equivalent SLP of size O(g) and height O(log N) where N is the length of the represented string. Furthermore, I will discuss extensions and various applications of the balancing theorem.
This is joint work with Artur Jeż and Markus Lohrey.
9.11.2021, 16:00 (s.t.) Patrick Totzke (Liverpool) -- Some results on strategy complexities for countable MDPs/Games
I will talk mainly about the most recent in a line of papers on strategy complexity for countable MDPs and (turn-based, stochastic) Games. I will motivate this line of research and mention related results and some open questions.
We consider the "Transient" objective, which asks not to visit any state infinitely often. While this is not possible in any finite Markov Decision Process (MDP), it can be satisfied in countably infinite ones, e.g., if the transition graph is acyclic. Transience is not the same as coBuechi nor expressible as Parity condition.
We prove the following properties of this objective in countably infinite MDPs.
1. There exist uniformly $\eps$-optimal MD strategies (memoryless deterministic) for Transient, even in infinitely branching MDPs.
2. Optimal strategies for Transient need not exist, even if the MDP is finitely branching. However, if an optimal strategy exists then there is also an optimal MD strategy.
3. If an MDP is universally transient (i.e., almost surely transient under all strategies) then many other objectives have a lower strategy complexity than in general MDPs. E.g., $\eps$-optimal strategies for Safety and co-B\"uchi and optimal strategies for $\{0,1,2\}$-Parity (where they exist) can be chosen MD, even if the MDP is infinitely branching.
The paper is joint work with Stefan Kiefer, Richard Mayr and Mahsa Shirmohammadi and appeared at CONCUR this year. A very short video teaser is available here: https://stream.liv.ac.uk/xrvdpjs5
29.06.2021, 16:00 (s.t.) Manfred Kufleitner (Stuttgart) -- FO2 quantifier alternation over infinite words
We consider two-variable first-order logic FO^2 over infinite words. Restricting the number of nested negations defines an infinite hierarchy; its levels are often called the half-levels of the FO^2 quantifier alternation hierarchy. The full levels are the Boolean closures of the half-levels. For every level of this hierarchy, we give an effective characterization. For the lower levels, this characterization is a combination of an algebraic and a topological property. For the higher levels, algebraic properties turn out to be sufficient. Within two-variable first-order logic, each algebraic property is a single ordered identity of omega-terms. The topological properties are the same as for the lower half-levels of the quantifier alternation hierarchy without the two-variable restriction (i.e., the Cantor topology and the alphabetic topology). Our result generalizes the corresponding results for finite words.
This is joint work with Aaron Boussidan and Viktor Henriksson.
15.06.2021, 16:00 (s.t.) Dominik Freydenberger (Loughborough) -- Finite models and word equations
This talk is about FC, a new logic on words. Like the theory of concatenation, FC is based word equations; but in contrast to it, the universe of FC is restricted to a single word and all its factors.
In many ways, FC behaves like first-order logic over finite structures. Most importantly, its model checking problem is PSPACE-complete and can be made tractable by restricting the formulas, for example by requiring acyclicity or bounded width.
FC also provides a general framework for logic on words that can be tailored to various applications. For example, by adding regular constraints, FC can be used as a logic for document spanners; and FC with operators for fixed points or transitive closure captures various complexity classes.
This talk is based on "The theory of concatenation over finite models", a joint work with Liat Peterfreund, to be presented at ICALP 2021 (full version https://arxiv.org/abs/1912.06110).
1.06.2021, 16:00 (s.t.) Sylvain Schmitz (Paris) -- Branching in Well-Structured Transition Systems
Abstract:
The framework of well-structured transition systems has been highly successful in providing generic algorithms to show the decidability of verification problems for infinite-state systems. In some of these applications, the executions in the system at hand are actually trees, and need to be "lifted" to executions over sets of configurations in order to fit in the framework. The downside of this approach is that we might lose precision when analysing the computational complexity of the algorithms, compared to reasoning over branching executions.
Talk given at CSL 2021; see here.
18.05.2021, 16:00 (s.t.) -- Karoliina Lehtinen (Aix-Marseille) - Just a little bit of nondetermism can go a long way
Abstract:
Nondeterminism probably makes your favourite automata model more expressive, or at least more succinct, than determinism. However, the cost of nondeterminism is higher algorithmic complexity, especially in algorithms that involve a determinisation step.
Good-for-games automata, also known as history deterministic automata, are nondeterministic automata in which nondeterministic choices can be resolved on the fly, without knowledge of the future of a word. They lie in between deterministic and nondeterministic models, and combine some of the expressivity and succinctness of nondeterminism with some of the nice algorithmic properties of deterministic automata.
In particular, games with winning conditions given by good-for-games automata can be solved without determinisation.
In this talk, I will give an overview of good-for-games automata, explain their relation to the Church synthesis problem and survey recent developments in the area for different classes of automata (regular, pushdown, and perhaps even timed) and point to some of the hard questions that remain unanswered and some areas that remain unexplored.
04.05.2021, 16:00 (s.t.) -- Karin Quaas (Leipzig) - On the universality problem for unambiguous register automata
Abstract:
The talk gives an overview over recent results concerning the universality problem for unambiguous register automata.
27.04.2021, 16:00 (s.t.) -- Igor Potapov (Liverpool) - Various forms of reachability - the question, the tool and the objective
Abstract:
In this presentation I would like to discuss a number of computational problems which are all linked by reachability questions, but appear in quite diverse areas of mathematics and computer science, e.g. computational models, algebraic structures, geometry and topology as well as in other virtual or real systems.
Reachability is one of the fundamental and the most natural question to ask about formal models with any forms of dynamics. It is the question about predicting the dynamics -- for example, whether a particular state or a property could be reached starting from some specific initial state or more parametrised form of initial configurations. On the other hand the reachability properties can characterise the dynamics in formal models and abstractions in respect to diversity, complexity and various structural properties. Moreover the reachability can be seen as a set of desirable or undesired properties in control theory and computational games where the goal is to design a control sequence or a winning strategy.
The number of open problems in this presentation could be on a different level of complexity from some questions which are suitable for immediate exploration by research students upto major unsolved problem in mathematics and computer science.
6.04.2021, 16:00 (s.t.) -- Markus Lohrey (Siegen) - Subgroup membership for GL(2,Z)
Abstract:
The subgroup membership problem for a group G asks whether a given group element g from G belongs to a given finitely generated subgroup H of G. Here, we are mainly interested in the case that G is infinite, where the representation of elements of G becomes relevant. In the case that G is finitely generated, one can represent elements of G by finite words over a generating set. But this representation is often not the most natural one. Consider for instance the group GL(2,Z) of 2-dimensional integer matrices with determinant 1 or -1 (it is a finitely generated group). The most natural representation of an element of GL(2,Z) is certainly a matrix with binary encoded integers. Concerning the subgroup membership problem, it is straightforward to show that it can be solved in polynomial time for GL(2,Z) if elements of GL(2,Z) are represented by finite words over a finite set of generators (the proof uses the fact that GL(2,Z) is virtually-free. On the other hand, if elements of GL(2,Z) are represented by matrices with binary encoded integers, the subgroup membership problem becomes more difficult. Nevertheless, we show that it can be solved in polynomial time. For the proof we extend Stallings folding procedure to graphs where edges are labelled with so called power words (finite words where binary encoded exponents are allowed).
(changed Date!) 23.3.2021, 16:00 -- Jean Jung (Hildesheim) - On the Decidability of Expressive Description Logics with Transitive Closure and Regular Role Expressions.
Abstract:
We consider the extension of the basic description logic ALC with inverses, nominals, functionality, and regular role expressions. The logic can be viewed as a notational variant of propositional dynamic logic PDL extended with converse, constants, and deterministic programs. The complexity of the satisfiability problem of this logic is not known. However, it is known that the extension of ALC with any three of the four mentioned constructs is decidable and ExpTime or NExpTime-complete and that the logic becomes undecidable when regular expressions are replaced by fixpoints. We identify two non-trivial conditions on the regular expressions which still ensure decidability in NExpTime and 2NExpTime, respectively. Notably, both conditions allow for transitive closure and for expressing equivalence relations and linear orders, two semantic relations which are notorious for causing undecidability when added to Two Variable First-Order Logic.
23.2.2021, 16:00 -- Markus Schmid (Berlin) - A Purely Regular Approach to Non-Regular Core Spanners
Abstract:
The regular spanners (characterised by vset-automata) are closed under the algebraic operations of union, join and projection, and have desirable algorithmic properties. The core spanners (introduced by Fagin, Kimelfeld, Reiss, and Vansummeren (PODS 2013, JACM 2015) as a formalisation of the core functionality of the query language AQL used in IBM’s SystemT) additionally need string equality selections and it has been shown by Freydenberger and Holldack (ICDT 2016, Theory of Computing Systems 2018) that this leads to high complexity and even undecidability of the typical problems in static analysis and query evaluation. We propose an alternative approach to core spanners: by incorporating the string-equality selections directly into the regular language that represents the underlying regular spanner (instead of treating it as an algebraic operation on the table extracted by the regular spanner), we obtain a fragment of core spanners that, while having slightly weaker expressive power than the full class of core spanners, arguably still covers the intuitive applications of string equality selections for information extraction and has much better upper complexity bounds of the typical problems in static analysis and query evaluation.
9.2.2021, 16:00 -- Nathanaël Fijalkow (Bordeaux) - Can we extend the quasipolynomial time algorithms of parity games to mean payoff games?
Abstract:
Short answer is ''arguably not". More details below.
We study the computational complexity of solving mean payoff games. This class of games can be seen as an extension of parity games, and they have similar complexity status: in both cases solving them is in NP and in coNP and not known to be in P. In a breakthrough result Calude, Jain, Khoussainov, Li, and Stephan constructed in 2017 a quasipolynomial time algorithm for solving parity games, which was quickly followed by a few other algorithms with the same complexity. Our objective is to investigate how these techniques can be extended to mean payoff games.
The starting point is the combinatorial notion of universal trees: all quasipolynomial time algorithms for parity games have been shown to exploit universal trees. Universal graphs extend universal trees to arbitrary (positionally determined) objectives. We show that they yield a family of value iteration algorithms for solving mean payoff games which includes the value iteration algorithm due to Brim, Chaloupka, Doyen, Gentilini, and Raskin.
The contribution of this paper is to prove tight bounds on the complexity of algorithms for mean payoff games using universal graphs. We consider two parameters: the largest weight N in absolute value and the number k of weights. The dependence in N in the existing value iteration algorithm is linear, we show that this can be improved to N^{1 - 1/n} and obtain a matching lower bound. However, we show that we cannot break the linear dependence in the exponent in the number k of weights implying that universal graphs do not yield a quasipolynomial time algorithm for solving mean payoff games.
Joint work with Pierre Ohlmann and Paweł Gawrychowski,
available here: Value Iteration Using Universal Graphs and the Complexity of Mean Payoff Games
26.1.2021, 16:00 -- Pawel Parys (Warsaw) - A Quasi-Polynomial Black-Box Algorithm for Fixed Point Evaluation
joint work with André Arnold and Damian Niwiński
Abstract:
We consider nested fixed-point expressions like µz.νy.µx.f(x,y,z)
evaluated over a finite lattice, and ask how many queries to a function f
are needed to find the value. Following a recent
development for parity games, we show that a quasi-polynomial number of
queries is sufficient, namely n^{lg(d/lg n)+O(1)} for a monotone function
f of arity d over the lattice {0,1}^n. The algorithm
is an abstract version of several algorithms proposed recently by a number
of authors, which involve (implicitly or explicitly) the structure of a
universal tree. We also show a quasi-polynomial
lower bound for the number of queries used by the algorithms in
consideration.
12.1.2021, 16:00 -- Georg Zetzsche (Kaiserslautern) -
Rational Subsets of Baumslag-Solitar Groups
(Part of the events celebrating the World Logic Day 2021)
Abstract:
We consider the rational subset membership problem for Baumslag-Solitar
groups. These groups form a prominent class in the area of algorithmic
group theory, and they were recently identified as an obstacle for
understanding the rational subsets of GL(2,ℚ). We show that rational
subset membership for Baumslag-Solitar groups BS(1,q) with q ≥ 2 is
decidable and PSPACE-complete. To this end, we introduce a word
representation of the elements of BS(1,q): their pointed expansion (PE),
an annotated q-ary expansion. Seeing subsets of BS(1,q) as word
languages, this leads to a natural notion of PE-regular subsets of
BS(1,q): these are the subsets of BS(1,q) whose sets of PE are regular
languages. Our proof shows that every rational subset of BS(1,q) is
PE-regular. Since the class of PE-regular subsets of BS(1,q) is
well-equipped with closure properties, we obtain further applications of
these results. Our results imply that (i) emptiness of Boolean
combinations of rational subsets is decidable, (ii) membership to each
fixed rational subset of BS(1,q) is decidable in logarithmic space, and
(iii) it is decidable whether a given rational subset is recognizable.
In particular, it is decidable whether a given finitely generated
subgroup of BS(1,q) has finite index.
Related papers:
This is joint work with Michaël Cadilhac and Dmitry Chistikov and has
appeared at ICALP 2020. The full version of the paper is available at
Rational subsets of Baumslag-Solitar groups.
8.12.2020, 16:00 -- Joel Day (Loughborough) -
A closer look at solution-sets to word equations in restricted cases.
Abstract:
Word equations are equations in which each side is a word whose letters are either terminal symbols or variables. Solutions are substitutions of the variables for words over the alphabet of terminal symbols which result in both sides becoming equal. For example, x=bab is a solution to the equation xab = bax where x is a variable and a,b are terminal symbols.
They were originally studied as a possible means of solving Hilbert's 10th problem: since solving word equations can be reduced to solving Diophatine equations, the idea was to use word equations as an intermediate step to encode the computations of Turing machines in Diophantine equations. This endeavour ultimately failed when in 1977 Makanin presented the first general algorithm for deciding whether a given word equation has a solution. They remain an important topic at the intersection of theoretical computer science and algebra.
Prominent open problems include settling the precise complexity of deciding whether a given word equation has a solution, and whether the problem of determining whether a solution exists which satisfies additional conditions of the form "the image of x has the same length as the image of y" for variables x and y.
This talk will focus on restricted classes of word equations for which many questions remain unanswered (including those mentioned above), and recent efforts to describe the structure of their solutions-sets. Investigations into these subclasses offer new insights in the absence of results in the more general case, and are also of practical interest as solving word equations (with additional constraints) is an important part in the verification and analysis of string-heavy programming languages such as javascript.
Related papers:
On the Structure of Solution Sets to Regular Word Equations.
Upper Bounds on the Length of Minimal Solutions to Certain Quadratic Word Equations.
The Hardness of Solving Simple Word Equations.
24.11.2020, 16:00 -- Dirk Nowotka (Kiel) -
Lagrange’s Theorem for Binary Squares
Abstract:
We show how to prove theorems in additive number theory using a decision procedure based on finite automata. Among other things, we obtain the following analogue of Lagrange’s theorem: every natural number > 686 is the sum of at most 4 natural numbers whose canonical base-2 representation is a binary square, that is, a string of the form xx for some block of bits x. While we cannot embed this theorem itself in a decidable theory, we show that stronger lemmas that imply the theorem can be embedded in decidable theories, and show how automated methods can be used to search for these stronger lemmas.
Related papers:
Lagrange's Theorem for Binary Squares.
10.11.2020, 16:00 -- Christoph Haase (University College London) -
The complexity and expressiveness of existential Büchi arithmetic
Abstract:
Büchi arithmetic is an extension of Presburger arithmetic, the
first-order theory of the natural numbers with addition and
equality, that additionally allows for expressing restricted
divisibility predicates. In his seminal work, Büchi showed
decidability of Büchi arithmetic via an automata-theoretic
construction. In particular, a set of natural numbers is
definable in Büchi arithmetic if and only if it is recognizable
by a finite-state automaton under a suitable encoding of numbers
as strings.
In this talk, I will focus on the existential fragment of Büchi
arithmetic for which, until recently, only few results were
known. While it is possible to construct a family of formulas of
existential Büchi arithmetic whose smallest solutions have
exponential bit-size, I will show that existential Büchi
arithmetic is nevertheless NP-complete. I will also show that the
existential fragment of Büchi arithmetic is strictly less
expressive than full Büchi arithmetic. This result is in
contrast to Presburger arithmetic and, in particular, implies
that a quantifier-elimination procedure for Büchi arithmetic
a la Presburger cannot exist.
This talk is based on joint work with Florent Guepin, Jakub
Rozycki and James Worrell.
Related papers:
On the Existential Theories of Büchi Arithmetic and Linear p-adic Fields.
On the Expressiveness of Büchi Arithmetic.