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

Nov. 17, 2021, 2:15 p.m.
Jędrzej Kołodziejski (MIM UW)
un)boundedness - logic, automata and games with countdow (Taming)
I will present extensions of: the modal fixpoint calculus, parity games, and parity automata - designed to capture (un)boundedness-related phenomena. The extensions lift the classical logic~games~automata correspondence beyond regular properties - in particular the logic …
Nov. 10, 2021, 2:15 p.m.
Szymon Toruńczyk (MIM UW)
Some results and directions in finite model theory
I will discuss the FO-transduction order on classes of graphs (or other structures), defined by the relation: a class C can be obtained by an FO-transduction from a class D. I will focus on the …
Nov. 3, 2021, 2:15 p.m.
Piotr Hofman (MIM UW)
Language inclusion for unambiguous VASSes
During the talk, I will present our unpublished results with Wojciech Czerwiński. I will show the decidability of language inclusion for unambiguous VASSes. The main tool is, up to our knowledge, a new concept of …
Oct. 27, 2021, 2:15 p.m.
Paweł Parys (MIM UW)
Higher-Order Model Checking Step by Step
I will show a new simple algorithm that solves the model-checking problem for recursion schemes: check whether the tree generated by a given higher-order recursion scheme is accepted by a given alternating parity automaton. Recursion …
Oct. 20, 2021, 2:15 p.m.
Jakub Gajarsky (MIM UW)
Differential games, locality, and model checking for FO logic of graphs
We introduce differential games for FO logic of graphs, a variant of Ehrenfeucht-Fraisse games in which the game is played on one graph only and the moves of both players are restricted. We prove that …
Oct. 13, 2021, 2:15 p.m.
Michał Skrzypczak (MIM UW)
Guidable automata and their index problem
Rabin's theorem relies on the equivalence between Monadic Second-Order logic and non-deterministic automata over infinite trees. The non-determinism of the involved model is known to be "inherent", both in terms of descriptive complexity and from …
Oct. 6, 2021, 2:15 p.m.
Szymon Toruńczyk (MIM UW)
Model checking separator logic on graphs that exclude a fixed topological minor.
We consider separator logic on graphs introduced recently by Bojańczyk, and independently by Siebertz, Shrader, and Vigny. This logic extends first-order logic by atomic predicates of arity k+2, for each k, expressing that every path …
June 30, 2021, 2:15 p.m.
Albert Gutowski (MIM UW)
Finite entailment of non-local queries in description logics
We study the problem of finite entailment of ontology-mediated queries. In particular, we are interested in non-local queries. Recent studies show that a vast majority of user-issued CRPQs only use Kleene star over unions of …
June 23, 2021, 2:15 p.m.
Andrzej Murawski (University of Oxford)
Verifying higher-order concurrency with data automata
Using a combination of automata-theoretic and game-semantic techniques, we propose a method for analysing higher-order concurrent programs. Our language of choice is Finitary Idealised Concurrent Algol (FICA) due to its relatively simple fully abstract game …
June 16, 2021, 2:15 p.m.
Lê Thành Dũng (Tito) Nguyễn (LIPN (Paris Nord))
Comparison-free polyregular functions
We introduce a new automata-theoretic class of string-to-string functions with polynomial growth. Several equivalent definitions are provided: a machine model which is a restricted variant of pebble transducers, and a few inductive definitions that close …
June 9, 2021, 2:15 p.m.
Amina Doumane (CNRS-ENS Lyon)
Regular expressions for languages of graphs of tree-width 2
I propose a syntax of regular expressions which capture exactly CMSO definable languages of graphs of tree-width 2. A similar syntax is given for CMSO definable languages of series-parallel graphs and of connected tree-width 2 …
June 2, 2021, 2:15 p.m.
Gaëtan Douéneau (IRIF, Université de Paris)
Pebble transducers with unary output
Bojańczyk recently initiated an intensive study of deterministic pebble transducers, which are two-way automata that can drop marks (named "pebbles") on their input word, and produce an output word. They describe functions from words to …
May 26, 2021, 2:15 p.m.
Sandra Kiefer (MIM UW)
Logarithmic Weisfeiler-Leman Identifies All Planar Graphs
The Weisfeiler-Leman (WL) algorithm is a well-known combinatorial procedure for detecting symmetries in graphs that is widely used in graph-isomorphism tests. It proceeds by iteratively computing vertex colours. The number of iterations needed to obtain …
May 19, 2021, 2:15 p.m.
Jan Dreier (TU Wien, Austria)
Lacon- and Shrub-Decompositions: A New Characterization of First-Order Transductions of Bounded Expansion Classes
The concept of bounded expansion provides a robust way to capture sparse graph classes with interesting algorithmic properties. Most notably, every problem definable in first-order logic can be solved in linear time on bounded expansion …
May 12, 2021, 2:15 p.m.
Wojciech Czerwiński (MIM UW)
Reachability in Vector Addition Systems is Ackermann-complete
Complexity of the reachability problem in Vector Addition Systems (VASes) was a long standing problem for a few decades. Very recently two proofs of Ackermann-hardness were obtained independently (one by Jerome Leroux, one by us). …