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

Jan. 10, 2018, 2:15 p.m.
Lorenzo Clemente (Uniwersytet Warszawski)
Computing the binary reachability relation of Timed Pushdown Automata
The reachability problem asks, for a fixed initial and final configuration, whether there is a run of the system going from the former to the latter. The binary reachability problem generalises the reachability problem: The …
Dec. 20, 2017, 2:15 p.m.
Michał Skrzypczak (Uniwersytet Warszawski)
index) bounds for unambiguous languages (No)
The talk is about the class of regular languages of infinite trees that can be recognised by unambiguous automata. Although the class is very natural, its properties are usually non-trivial with many basic questions unanswered …
Dec. 13, 2017, 2:15 p.m.
Adrien Boiret (Uniwersytet Warszawski)
Equivalence of Deterministic Top-Down Tree Transducers is ExpTime-Complete
The class of Deterministic Top-Down Tree Transducers (DTOP) has been studied for a long time, but while its equivalence problem was known to be ExpTime-Hard, the best known algorithms were coNExpTime (search of counter-example) or …
Dec. 6, 2017, 2:15 p.m.
Juliusz Straszyński (Uniwersytet Warszawski)
PSPACE-complexity of reachability and coverability problems for acyclic Grammar VASes
I will show a reduction of reachablity problem for Grammar VASes to a Subset Sum Game, which is PSPACE-complete.
Nov. 29, 2017, 2:15 p.m.
Petr Novotny (IST Austria)
Checking and Classifying Fast Termination in VASS
Vector Addition Systems with States (VASS) consists of a finite state machine equipped with d positive integer-valued counters, where in each transition every counter is incremented, decremented, or left unchanged. In this talk, I will …
Nov. 22, 2017, 2:15 p.m.
Tomasz Gogacz (Uniwersytet Warszawski)
Nominals, Inverses, Counting, and Conjunctive Queries or: Why Infinity is your Friend!
I will present a nice result in Knowledge Representation. It is a proof of decidability of query entailment for a certain extension of modal logic. The procedure consists of two semi-recursive procedures. The first is …
Nov. 15, 2017, 2:15 p.m.
Ranko Lazic (University of Warwick)
Succinct progress measures for solving parity games
The recent breakthrough paper by Calude et al. has given the first algorithm for solving parity games in quasi-polynomial time, where previously the best algorithms were mildly subexponential. We devise an alternative quasi-polynomial time algorithm …
Nov. 8, 2017, 2:15 p.m.
Radosław Piórkowski (Uniwersytet Warszawski)
WQO dichotomy conjecture — proof of a special case, part 2
The conjecture claims that there exists a simple criterion for decidability for Petri nets with homogeneous data. We prove a special case of this conjecture for data being 2-edge-coloured graphs. I will outline the overall …
Oct. 25, 2017, 2:15 p.m.
Radosław Piórkowski (Uniwersytet Warszawski)
WQO dichotomy conjecture — proof of a special case
Decidability of many standard decision problems for Petri nets becomes an open problem once we extend the model with data. If we restrict only to homogeneous data domains, according to the WQO Dichotomy Conjecture there …
Oct. 18, 2017, 2:15 p.m.
Nathanael Fijalkow (University College London)
Timed comparisons of semi-Markov processes
A semi-Markov process is like a Markov process, but each transition takes some time to get fired, and this time is determined by a probabilistic distribution over the non-negative reals. In this talk I will …
Oct. 11, 2017, 2:15 p.m.
Bartek Klin (Uniwersytet Warszawski)
mu-calculus with atoms
True to the spirit of "\lambda x. (x with atoms)", I will present a modal mu-calculus with atoms. I will also explain what is wrong with it, and how it could perhaps be improved. This …
Oct. 4, 2017, 2:15 p.m.
Mikołaj Bojańczyk (Uniwersytet Warszawski)
joint work with Laure Daviaud and Krishna S (First-order list functions)
We define a class of functions, called first-order list functions, which manipulate objects such as lists, lists of lists, pairs of lists, lists of pairs of lists, etc. The definition is in the style of …
June 7, 2017, 2:15 p.m.
Sylvain Schmitz (ENS de Cachan)
second part (Downward-closures and PTL separability)
I'll present an approach to computing downward-closures and solving separability by piecewise-testable sets using ideal decompositions. The talk will be based on a joint paper with J. Goubault-Larrecq published at ICALP last year.
May 31, 2017, 2:15 p.m.
Thomas Zeume (Uniwersytet Warszawski)
Lower bounds in Dynamic Complexity
Unconditional lower bounds are are hard to prove. For this reason recent work on inexpressibility for dynamic complexity has been centered around fragments of DynFO (i.e. the class of queries maintainable using first-order formulas). In …
May 24, 2017, 2:15 p.m.
Sylvain Schmitz (ENS de Cachan)
Downward-closures and PTL separability
I'll present an approach to computing downward-closures and solving separability by piecewise-testable sets using ideal decompositions. The talk will be based on a joint paper with J. Goubault-Larrecq published at ICALP last year.