Organizatorzy

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

Informacje

środy, 14:15 , sala: 5440

Dziedziny badań

Lista referatów

27 października 2021 14:15
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 …
20 października 2021 14:15
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 …
13 października 2021 14:15
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 …
6 października 2021 14:15
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 …
30 czerwca 2021 14:15
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 …
23 czerwca 2021 14:15
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 …
16 czerwca 2021 14:15
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 …
9 czerwca 2021 14:15
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 …
2 czerwca 2021 14:15
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 …
26 maja 2021 14:15
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 …
19 maja 2021 14:15
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 …
12 maja 2021 14:15
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). …
5 maja 2021 14:15
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 …
28 kwietnia 2021 14:15
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 …
21 kwietnia 2021 14:15
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 …