# 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

12.1.2021, 16:00 -- Georg Zetzsche (Kaiserslautern) -

Rational Subsets of Baumslag-Solitar Groups

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.

____________________________________________________________________________

26.1.2021, 16:00 -- Pawel Parys (Warsaw) - TBA

26.1.2021, 16:00 -- Pawel Parys (Warsaw) - TBA

____________________________________________________________________________

9.2.2021, 16:00 -- Nathanaël Fijalkow (Bordeaux) - Can we extend the quasipolynomial time algorithms of parity games to mean payoff games?

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

____________________________________________________________________________

23.2.2021, 16:00 -- Markus Schmid (Berlin) - TBA

23.2.2021, 16:00 -- Markus Schmid (Berlin) - TBA

## Past Talks

10.11.2020, 16:00 -- Christoph Haase (University College London) -

The complexity and expressiveness of existential Büchi arithmetic

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.

____________________________________________________________________________

24.11.2020, 16:00 -- Dirk Nowotka (Kiel) -

Lagrange’s Theorem for Binary Squares

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.

____________________________________________________________________________

8.12.2020, 16:00 -- Joel Day (Loughborough) -

A closer look at solution-sets to word equations in restricted cases.

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.