Organizers

prof. dr hab. Mikołaj Bojańczyk
prof. dr hab. Damian Niwiński

Information

Wednesdays, 2:15 p.m. , room: 5440

Research fields

List of talks

Feb. 19, 2025, 2:15 p.m.
Rafał Stefański (University of Warsaw)
Polyregular model checking (Polyregular model checking)
We reduce the model checking problem for a subset of Python to the satisfiability of a first-order formula over finite words, which is known to be decidable. The reduction is based on the theory of …
Feb. 5, 2025, 2:15 p.m.
Wojciech Czerwiński (University of Warsaw)
Reachability in 3-VASS is Elementary (Reachability in 3-VASS is Elementary)
I will present our recent result (with Ismael Jecker, Sławomir Lasota and Łukasz Orlikowski) about the reachability problem in 3-dimensional Vector Addition Systems with States (VASS). We have shown that the problem is in 2-ExpSpace, …
Jan. 29, 2025, 2:15 p.m.
Andrew Ryzhikov (University of Warsaw)
A guide to tax-free travelling between codes, automata and matrices (A guide to tax-free travelling between codes, automata and matrices)
In this tutorial talk, I will describe a tight and fruitful relationship between variable-length codes (bases of free submonoids of a free monoid), unambiguous finite automata and semigroups of zero-one matrices. I will concentrate on …
Jan. 22, 2025, 2:15 p.m.
Giannos Stamoulis (University of Warsaw)
Low rank MSO (Low rank MSO)
We introduce a new logic for describing properties of graphs, which is called low rank MSO. This is the fragment of monadic second-order logic (MSO), in which set quantification is restricted to sets of bounded …
Jan. 15, 2025, 2:15 p.m.
Mikołaj Bojańczyk (University of Warsaw)
Graphs of unbounded linear cliquewidth. (Graphs of unbounded linear cliquewidth.)
We show that for every class C of graphs, one of the following holds: 1. The class has bounded linear cliquewidth; or 2. There is a surjective MSO transduction from C to the class of …
Dec. 18, 2024, 2:15 p.m.
Lorenzo Clemente (University of Warsaw)
The commutativity problem for varieties of formal series and applications (The commutativity problem for varieties of formal series and applications)
Let Σ be a finite alphabet of noncommuting indeterminates. A *formal series* over the rational numbers is a mapping Σ* → ℚ. We say that it is *commutative* if the output does not depend on …
Dec. 11, 2024, 2:15 p.m.
Martin Grohe (RWTH Aachen University)
Some Thoughts on Graph Similarity (Some Thoughts on Graph Similarity)
We give an overview of different approaches to measuring the similarity of, or the distance between, two graphs, highlighting connections between these approaches. We also discuss the complexity of computing the distances.
Dec. 4, 2024, 2:15 p.m.
Paweł Parys (University of Warsaw)
A Dichotomy Theorem for Ordinal Ranks in MSO (A Dichotomy Theorem for Ordinal Ranks in MSO)
We focus on formulae ∃X.ϕ(Y, X) of monadic second-order logic over the full binary tree, such that the witness X is a well-founded set. The ordinal rank rank(X) < ω_1 of such a set X …
Nov. 27, 2024, 2:15 p.m.
Michał Skrzypczak (University of Warsaw)
Index problem for tree automata - revisited (Index problem for tree automata - revisited)
This talk is mostly "other people's work" type of a talk. However, it is meant to prepare ground for the next week, when Paweł Parys will present our joint results with Damian Niwiński. I want …
Nov. 20, 2024, 2:15 p.m.
Mikołaj Bojańczyk (University of Warsaw)
Transducers and straight line programs (Transducers and straight line programs)
In this talk, a straight line program (SLP) is a context-free grammar that generates a single string. This can be viewed as a compression scheme, with the compressed string being possibly exponentially smaller than the …
Nov. 13, 2024, 2:15 p.m.
Szymon Toruńczyk (University of Warsaw)
Merge-width and First-Order Model Checking (Merge-width and First-Order Model Checking)
We introduce merge-width, a family of graph parameters that unifies several structural graph measures, including treewidth, degeneracy, twin-width, clique-width, and generalized coloring numbers. Graph classes of bounded merge-width – for which the radius-r merge-width parameter …
Nov. 6, 2024, 2:15 p.m.
Mathieu Lehaut (University of Gothenburg)
Synthesis for first order specifications over data words (Synthesis for first order specifications over data words)
We study the reactive synthesis problem for distributed systems with a finite but unbounded number of participants interacting with an uncontrollable environment. Executions of those systems are modelled by data words, and specifications are given …
Oct. 30, 2024, 2:15 p.m.
Piotr Hofman (University of Warsaw)
Soundness for Workflows with Reset Arcs (Soundness for Workflows with Reset Arcs)
Workflows are a subclass of Petri nets designed to model business processes. Various definitions of soundness for workflows have been proposed, with the two most prominent being "soundness" and the stronger "generalized soundness." We begin …
Oct. 23, 2024, 2:15 p.m.
Antoni Puch (University of Warsaw)
Minimising ambiguity of weighted automata (Minimising ambiguity of weighted automata)
By bounding the number of accepting runs of automata we obtain various subclasses of them. We consider: unambiguous automata, finitely-ambiguous automata, and polynomially-ambiguous automata, where the number of runs is bounded by 1, a constant, …
Oct. 16, 2024, 2:15 p.m.
Antonio Casares (University of Warsaw)
An algorithm to rule them all: Fast value iteration for energy games (An algorithm to rule them all: Fast value iteration for energy games)
We introduce a uniform framework for describing, comparing, and proving correctness of algorithms for energy games (which generalise the well known parity games). This framework allows us to provide simple presentations and correctness proofs of …