Organizatorzy

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

Informacje

środy, 14:15 , sala: 5050

Dziedziny badań

Lista referatów

20 maja 2020 14:15
Vincent Michielini (Uniwersytet Warszawski)
Regular choices and uniformisations for countable domains
Considering the following question: given (in a sense which will be clarified in the talk) a countable totally ordered set D, on which condition(s) does there exist a choice function over D (i.e. a function …
13 maja 2020 14:15
Denis Kuperberg (CNRS, LIP, ENS Lyon)
Computational content of circular proof systems
Cyclic proofs are a class of formal proof systems that allow some kind of circular reasoning. Unlike classical proofs, represented by finite trees with axioms as leaves, cyclic proofs are represented by trees containing infinite …
6 maja 2020 14:15
Filip Mazowiecki (MPI SWS)
The monitoring problem for timed automata
We study a variant of the classical membership problem in automata theory, which consists of deciding whether a given input word is accepted by a given automaton. We do so under a different perspective, that …
29 kwietnia 2020 14:15
Mikołaj Bojańczyk (Uniwersytet Warszawski)
Single use transducers over infinite alphabets
Automata for infinite alphabets, despite the undeniable appeal, are a bit of a theoretical mess. Almost all models are non-equivalent as language recognisers: deterministic/nondeterministic/alternating, one-way/two-way, etc. Also monoids give a different class of languages, and …
22 kwietnia 2020 14:15
Wojciech Czerwiński (Uniwersytet Warszawski)
Universality problem for unambiguous Vector Addition Systems with States
I will show that the universality problem is ExpSpace-complete for unambiguous VASS, which is in strong contrast with Ackermann-completeness of the same problem for nondeterministic VASS. I also plan to present some more results concerning …
15 kwietnia 2020 14:15
Bartek Klin (Uniwersytet Warszawski)
Monadic MSO logic
The correspondence of regular languages and monadic second-order logic relies on the fact that the class of regular languages is closed under images of surjective letter-to-letter homomorphisms. This closure property holds for finite words, but …
8 kwietnia 2020 14:15
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 …
1 kwietnia 2020 14:15
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 …
25 marca 2020 14:15
Radosław Piórkowski (Uniwersytet Warszawski)

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 …
18 marca 2020 14:15
-
No seminar
11 marca 2020 14:15
-
No seminar
4 marca 2020 14:15
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 …
26 lutego 2020 14:15
Mikołaj Bojańczyk (Uniwersytet Warszawski)
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 …
5 lutego 2020 14:15
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 …
29 stycznia 2020 14:15
Piotr Hofman (Uniwersytet Warszawski)
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 …