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

April 8, 2020, 2:15 p.m.
David Barozzini (Uniwersytet Warszawski)
Higher-order recursion schemes are an expressive formalism used to define languages of possibly infinite ranked trees.
Higher-order recursion schemes are an expressive formalism used to define languages of possibly infinite ranked trees. We prove, under a syntactical constraint called safety, decidability of the model-checking problem for recursion schemes against properties defined …
April 1, 2020, 2:15 p.m.
Engel Lefaucheux (MPI SWS)
Monniaux Problem in Abstract Interpretation
The Monniaux Problem in abstract interpretation asks, roughly speaking, whether the following question is decidable: given a program P, a safety specification φ, and an abstract domain of invariants D, does there exist an inductive …
March 25, 2020, 2:15 p.m.
Radosław Piórkowski (Uniwersytet Warszawski)
Online seminar) Timed games and deterministic separability ()
The presentation is based on my recent joint work with Lorenzo Clemente and Sławomir Lasota. We study a generalisation of Büchi-Landweber games to the timed setting, where Player I plays timed actions and Player II …
March 18, 2020, 2:15 p.m.
-
No seminar
March 11, 2020, 2:15 p.m.
-
No seminar
March 4, 2020, 2:15 p.m.
Gaëtan Douéneau-Tabot (ENS Paris-Saclay)
Optimisation of simple programs using pebble and marble transducers
Several models of automata with outputs (known as transducers) have been defined over the years to describe various classes of “regular-like” functions. Such classes generally have good decidability properties, and they have been shown especially …
Feb. 26, 2020, 2:15 p.m.
Mikołaj Bojańczyk (Uniwersytet Warszawski)
joint work with Amina Doumane (First-order tree-to-tree functions)
We study tree-to-tree transformations that can be defined in logics such as first-order logic or monadic second-order logic.We show that such transformations can be decomposed into certain primitive transformations, such as tree-to-tree homomorphisms or pre-order traversal, by using combinators such …
Feb. 5, 2020, 2:15 p.m.
Nathan Lhote (Uniwersytet Warszawski)
Pebble minimization for polyregular functions
We show that a polyregular word-to-word function is regular if and only its output size is at most linear in its input size. Moreover a polyregular function can be realized by: a transducer with …
Jan. 29, 2020, 2:15 p.m.
Piotr Hofman (Uniwersytet Warszawski)
joint work with Jakub Różycki (Generalized linear equations with unordered data)
Consider a Petri net in which every token carries a k-element set of data, and whenever we fire a transition then data from consumed and produced tokens are compared for equality and disequality. Such an …
Jan. 22, 2020, 2:15 p.m.
Pierre Simon (UC Berkeley)
Model theory of order-like and tree-like homogeneous structure
I will discuss results towards a model-theoretic classification of order-like homogeneous structures, including for instance all structures FO-definable in a dense linear order. I will also mention ongoing work towards extending this classification to include …
Jan. 15, 2020, 2:15 p.m.
Wojciech Czerwiński (Uniwersytet Warszawski)
joint work with Sławomir Lasota, Ranko Lazic, Jerome Leroux and Filip Mazowiecki (Reachability problem for fixed dimensional VASSes)
I will present a few recent results about reachability problem for fixed dimensional VASSes. There results invalidate some previously posed conjectures and show that the problem is harder than previously expected to be.
Jan. 8, 2020, 2:15 p.m.
Paweł Parys (Uniwersytet Warszawski)
joint work with Stefan Göller (Bisimulation Finiteness of Pushdown Systems Is Elementary)
We show that in case a pushdown system is bisimulation equivalent to a finite system, then there is already a bisimulation equivalent finite system whose size is elementarily bounded in the description size of the …
Dec. 18, 2019, 2:15 p.m.
Michał Wrocławski (Uniwersytet Warszawski)
How computability depends on notation?
We study abstract notations for natural numbers, which may differ from standard notations, so that the functions and relations classically uncomputable become computable, and vice versa. This question was raised by a philosopher Stewart Shapiro …
Dec. 11, 2019, 2:15 p.m.
Sławomir Lasota (Uniwersytet Warszawski)
Extremal counter programming
The aim is to present a technical core of a recently obtained TOWER lower bound for the reachability problem of Petri nets, model equivalent to vector addition systems with states or to nondeterministic counter machines …
Dec. 4, 2019, 2:15 p.m.
Michał Skrzypczak (Uniwersytet Warszawski)
Computing measures of weak-MSO definable sets of trees
Michalewski and Mio posed a fundamental question about the possibility of computing standard measures of regular languages of infinite trees. A positive solution (i.e. an algorithm) would allow us to tackle quantitatively a variety of …