Organizatorzy

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

Informacje

środy, 14:15 , sala: 5440

Dziedziny badań

Lista referatów

30 maja 2018 14:15
Paweł Parys (Uniwersytet Warszawski)
Universal trees grow inside separating automata: Quasi-polynomial lower bounds for parity games (joint work with Wojciech Czerwiński, Laure Daviaud, Nathanael Fijalkow, Marcin Jurdziński, Ranko Lazić)
Several distinct techniques have been proposed to design quasi-polynomial algorithms for solving parity games since the breakthrough result of Calude, Jain, Khoussainov, Li, and Stephan (2017): play summaries, progress measures and universal trees, and register …
23 maja 2018 14:15
Vincent Michielini (Uniwersytet Warszawski)
Uniformization Problem for Variants of First Order Logic over Finite Words
We study the uniformization problem for natural variants of the first order logic over finite words. We show that none of them has the uniformization property, as witnessed by proposed counterexamples.
16 maja 2018 14:15
Samson Abramsky (University of Oxford)
Relating Structure and Power: Comonadic Semantics for Computational Resources
Combinatorial games are widely used in finite model theory, constraint satisfaction, modal logic and concurrency theory to characterize logical equivalences between structures. In particular, Ehrenfeucht-Fraisse games, pebble games, and bisimulation games play a central role. …
9 maja 2018 14:15
Bartosz Klin (Uniwersytet Warszawski)
Mu-calculi with atoms
I will show an extension of modal mu-calculus to sets with atoms, developed jointly with Mateusz Łełyk. Model checking is decidable there, and a correspondence to parity games holds. On the other hand, satisfiability becomes …
25 kwietnia 2018 14:15
Janusz Schmude (Uniwersytet Warszawski)
The “Hilbert Method” for Solving Transducer Equivalence Problems
The "Hilbert Method" applies classical results from algebraic geometry, e.g. Hilbert's Basis Theorem, to prove decidability of equivalence on certain classes of transducers. In the first part, following [1], we will describe the method and …
18 kwietnia 2018 14:15
Wojciech Czerwiński (Uniwersytet Warszawski)
Toolkit for VASSes (joint work with Piotr Hofman and Georg Zetzsche)
There are many natural problems for VASS systems, which are a bit similar in style to the reachability problem, but cannot be directly reduced to reachability. In order to solve them one needs to dig …
11 kwietnia 2018 14:15
Sławomir Lasota (University of Warsaw)
Regular Separability of Well-Structured Transition Systems
We investigate languages recognized by well-structured transition systems (WSTS), i.e., infinite systems with state space ordered by a well quasi-order (WQO). We show that, surprisingly, under very mild assumptions every two disjoint WSTS languages are regularly …
4 kwietnia 2018 14:15
Paweł Parys (Uniwersytet Warszawski)
Recursion Schemes and the WMSO+U Logic
We study the weak MSO logic extended by the unbounding quantifier (WMSO+U), expressing the fact that there exist arbitrarily large finite sets satisfying a given property. We prove that it is decidable whether the tree …
28 marca 2018 14:15
-
No seminar (thursday plan)
21 marca 2018 14:15
Marcin Jurdziński (University of Warwick)
A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games (joint work with Laure Daviaud and Ranko Lazić)
In a mean-payoff parity game, one of the two players aims both to achieve a qualitative parity objective and to minimize a quantitative long-term average of payoffs (aka. mean payoff). The game is zero-sum and …
14 marca 2018 14:15
Bartosz Piotrowski (Uniwersytet Warszawski)
Automated Reasoning in Large Theories and Premise Selection with Machine Learning
In the talk I will briefly overview current state-of-the-art in the fields of Formal Mathematics and Automated Theorem Proving and how Machine Learning techniques can be fruitfully applied in these domains. One of crucial problems …
7 marca 2018 14:15
-
No seminar
28 lutego 2018 14:15
Pierre Pradic (ENS de Lyon)
A Curry-Howard Approach to Church's Synthesis via Linear Logic (Joint work with Colin Riba)
Church synthesis problem asks whether or not one can synthesize a 1-Lipschitz (or synchronous) function according to a specification of the type ∀ X ∃ Y φ(X,Y) expressed in the language of MSO over ω. …
21 lutego 2018 14:15
Mikołaj Bojańczyk (Uniwersytet Warszawski)
Transducers with polynomial size increase (part 2)
For functional string-to-string transductions, one of the most popular models is deterministic two-way automata with output. This model admits many different equivalent characterisations (mso transductions, streaming string transducers), and strictly generalises other transducer models such …
14 lutego 2018 14:15
Mikołaj Bojańczyk (Uniwersytet Warszawski)
Transducers with polynomial size increase
For functional string-to-string transductions, one of the most popular models is deterministic two-way automata with output. This model admits many different equivalent characterisations (mso transductions, streaming string transducers), and strictly generalises other transducer models such …