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

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). …
May 5, 2021, 2:15 p.m.
Mikołaj Bojańczyk (MIM UW)
Star-free expressions for graphs, and an appropriate first-order logic
In the study of word languages, first-order logic is more frequently used with the order predicate x > y, and not the successor predicate x=y+1. (For MSO, there is no difference.) For example, the celebrated …
April 28, 2021, 2:15 p.m.
Nathanaël Fijalkow (LaBRI)
The theory of universal graphs for infinite duration games
2017 was a special year in the world of parity games. Now that the dust has settled, what have we learned from the new quasi polynomial algorithms? In this talk I'll introduce the notion of …
April 21, 2021, 2:15 p.m.
Lorenzo Clemente & Michał Skrzypczak (MIM UW & MIM UW)
Deterministic and game separability of tree languages via games
We show that it is decidable whether two regular languages of infinite trees are separable by a deterministic language, resp., a game language. We consider two variants of separability, depending on whether the set of …