Weekly research seminar
Organizers
 prof. dr hab. Mikołaj Bojańczyk
 prof. dr hab. Damian Niwiński
Information
Wednesdays, 2:15 p.m. , room: 5050Research fields
List of talks

Jan. 12, 2022, 2:15 p.m.
Pierre Ohlmann (MIM UW)
Characterising oneplayer positionality for infinite duration games on graphs
I will present a new result, asserting that a winning condition (or, more generally, a valuation) which admits a neutral letter is positional over arbitrary arenas if and only if for all cardinals there exists …

Dec. 22, 2021, 2:15 p.m.
Marcin Przybyłko (University of Bremen)
Answer Counting and Guarded TGDs
Answer Counting is simply the problem of counting the number of solutions to a given query. TupleGenerating Dependencies (TGDs) are a common formalism for formulating database constraints. A TGD states that if certain facts are …

Dec. 15, 2021, 2:15 p.m.
Filip Mazowiecki (Max Planck Institute for Software Systems)
The boundedness and zero isolation problems for weighted automata over nonnegative rationals
We consider linear costregister automata (equivalently, weighted automata) over the semiring of nonnegative rationals, which generalise probabilistic automata. The two problems boundedness and zero isolation ask whether there is a sequence of words that converge …

Dec. 8, 2021, 2:15 p.m.
Arka Ghosh (MIM UW)
Joint work with P.Hofman and S.Lasota
An orbitfinite system of linear equations is a system of linear equations where the equations and the variables used in them are possibly infinite but are finite up to certain symmetries. I will start with …

Dec. 1, 2021, 2:15 p.m.
Ismaël Jecker (MIM UW)
Composite automata
A finite automaton A is called composite if there exist automata A1, A2, . . . , Ak smaller than A such that the language of A is equal to the intersection of the languages …

Nov. 24, 2021, 2:15 p.m.
Krzysztof Ziemiański (MIM UW)
joint work with U. Fahrenberg, C. Johansen, G. Struth
Higher dimensional automata (HDA) are a formalism for modeling concurrent systems introduced by Pratt and van Glabbeek. I will present several ways to define languages of HDA, which are collections of interval pomsets closed under …

Nov. 17, 2021, 2:15 p.m.
Jędrzej Kołodziejski (MIM UW)
un)boundedness  logic, automata and games with countdow
I will present extensions of: the modal fixpoint calculus, parity games, and parity automata  designed to capture (un)boundednessrelated 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 FOtransduction order on classes of graphs (or other structures), defined by the relation: a class C can be obtained by an FOtransduction 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)
HigherOrder Model Checking Step by Step
I will show a new simple algorithm that solves the modelchecking problem for recursion schemes: check whether the tree generated by a given higherorder 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 EhrenfeuchtFraisse 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 SecondOrder logic and nondeterministic automata over infinite trees. The nondeterminism 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 firstorder 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 nonlocal queries in description logics
We study the problem of finite entailment of ontologymediated queries. In particular, we are interested in nonlocal queries. Recent studies show that a vast majority of userissued CRPQs only use Kleene star over unions of …

June 23, 2021, 2:15 p.m.
Andrzej Murawski (University of Oxford)
Verifying higherorder concurrency with data automata
Using a combination of automatatheoretic and gamesemantic techniques, we propose a method for analysing higherorder concurrent programs. Our language of choice is Finitary Idealised Concurrent Algol (FICA) due to its relatively simple fully abstract game …