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

Jan. 12, 2022, 2:15 p.m.
Pierre Ohlmann (MIM UW)
Characterising one-player 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. Tuple-Generating 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 cost-register 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 (Orbit-finite System of Linear Equations)
An orbit-finite 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 (Languages of higher dimensional automata and Kleene theorem)
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 (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 …