Cotygodniowe seminarium badawcze
2020-05-20, godz. 14:15, Online seminar
Vincent Michielini (Uniwersytet Warszawski)
Regular choices and uniformisations for countable domains (joint work with Michał Skrzypczak)
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 f: P(D) -> D such that for all nonempty X subset of D, f(...
2020-05-13, godz. 14:15, Online seminar
Denis Kuperberg (CNRS, LIP, ENS Lyon)
Computational content of circular proof systems (joint work with Laureline Pinault and Damien Pous)
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 branches. The Curry-Howard correspondence allows us to see these cyclic...
2020-05-06, godz. 14:15, Online seminar
Filip Mazowiecki (MPI SWS)
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 is, we consider a dynamic version of the problem, called monitoring problem, where the autom...
2020-04-29, godz. 14:15, Online seminar
Mikołaj Bojańczyk (Uniwersytet Warszawski)
Single use transducers over infinite alphabets (joint work with Rafał Stefański)
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 mso gives yet another...
2020-04-22, godz. 14:15, Online seminar
Wojciech Czerwiński (Uniwersytet Warszawski)
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 the interplay between unambiguity and VASS. ...
2020-04-15, godz. 14:15, Online seminar
Bartek Klin (Uniwersytet Warszawski)
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 also for infinite words, finite or infinite trees, and ...
2020-04-08, godz. 14:15, Online seminar
David Barozzini (Uniwersytet Warszawski)
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 by alternating B-automata, an ex...
2020-04-01, godz. 14:15, Online seminar
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 invariant I in D guaranteeing that program P meets its s...
2020-03-25, godz. 14:15, Online seminar
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 replies immediately with untimed actions. The winning condition is ...
2020-03-18, godz. 14:15, 5050