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

May 30, 2018, 2:15 p.m.
Paweł Parys (Uniwersytet Warszawski)
joint work with Wojciech Czerwiński, Laure Daviaud, Nathanael Fijalkow, Marcin Jurdziński, Ranko Lazić (Universal trees grow inside separating automata: Quasi-polynomial lower bounds for parity games)
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 …
May 23, 2018, 2:15 p.m.
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.
May 16, 2018, 2:15 p.m.
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. …
May 9, 2018, 2:15 p.m.
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 …
April 25, 2018, 2:15 p.m.
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 …
April 18, 2018, 2:15 p.m.
Wojciech Czerwiński (Uniwersytet Warszawski)
joint work with Piotr Hofman and Georg Zetzsche (Toolkit for VASSes)
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 …
April 11, 2018, 2:15 p.m.
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 …
April 4, 2018, 2:15 p.m.
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 …
March 28, 2018, 2:15 p.m.
-
thursday plan (No seminar)
March 21, 2018, 2:15 p.m.
Marcin Jurdziński (University of Warwick)
joint work with Laure Daviaud and Ranko Lazić (A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games)
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 …
March 14, 2018, 2:15 p.m.
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 …
March 7, 2018, 2:15 p.m.
-
No seminar
Feb. 28, 2018, 2:15 p.m.
Pierre Pradic (ENS de Lyon)
Joint work with Colin Riba (A Curry-Howard Approach to Church's Synthesis via Linear Logic)
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 ω. …
Feb. 21, 2018, 2:15 p.m.
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 …
Feb. 14, 2018, 2:15 p.m.
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 …