Organizers

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

Information

Wednesdays, 2:15 p.m. , room: 5050

Research fields

List of talks

Jan. 15, 2014, 2:15 p.m.
Mikołaj Bojańczyk (Uniwersytet Warszawski)
Weak MSO+U with path quantifiers
Over infinite trees, satisfiability is decidable for weak monadic second-order logic extended by the unbounding quantifier U and quantification over infinite paths. The proof is by reduction to emptiness for a certain automaton model, while …
Jan. 8, 2014, 2:15 p.m.
Eryk Kopczyński (Uniwersytet Warszawski)
Infinite sets in practice
We present a C++ library allowing computation over infinite sets. The programmer is able to represent infinite sets (in finite memory), as well as loop over them (in finite time). The elements of these sets …
Dec. 18, 2013, 2:15 p.m.
Paweł Parys (Uniwersytet Warszawski)
joint work with Achim Blumensath, Thomas Colcombet, Denis Kuperberg and Michael Vanden Boom
This work is a step towards solving regular cost functions on infinite trees (which is already done for words - finite and infinite - and for finite words).We consider cost functions over infinite trees defined …
Dec. 11, 2013, 2:15 p.m.
Michał Skrzypczak (Uniwersytet Warszawski)
joint work with Tomasz Gogacz, Henryk Michalewski and Matteo Mio
I will present some investigations on measure properties of regular tree languages. The motivation for this research comes from the dissertation of Matteo Mio. I plan to focus on two aims: the first aim is …
Dec. 4, 2013, 2:15 p.m.
Denis Kuperberg (Uniwersytet Warszawski)
joint work with Udi Boker, Orna Kupferman, Michał Skrzypczak
One of the advantages of deterministic automata is that they composewell with trees and games. In the theory of cost functions, suchdeterministic automata are not always available, so a weaker notionwas introduced: history-deterministic automata, which …
Nov. 27, 2013, 2:15 p.m.
Adam Witkowski (Uniwersytet Warszawski)
Regular Tree Pattern Queries and Datalog
Regular Tree Pattern Queries (RTPQ) are queries for data trees that were defined during a research on Active XML.We found that this formalism is interesting on its own and closely connected to Datalog.I will talk …
Nov. 20, 2013, 2:15 p.m.
Thomas Colcombet (LIAFA, Université Paris 7)
continuation
We will show how to solve cost-MSO over finite words, paying a particular attention to the use of the non-standard aspect of Internal Set Theory.
Nov. 13, 2013, 2:15 p.m.
Thomas Colcombet (LIAFA, Université Paris 7)
Regular Cost-Functions and Internal Set Theory
In this talk, I will take as an excuse regular cost-functions (an extension of regular languages with quantitative capabilities) for presenting "Internal Set Theory" (IST), an axiomatic extension of ZFC that has native non-standard analysis …
Nov. 6, 2013, 2:15 p.m.
Paweł Parys (Uniwersytet Warszawski)
joint work with Achim Blumensath and Thomas Colcombet
I will talk about a new extension of the MSO logic in the style of MSO+U, which is called Asymptotic MSO. This logic refers to structures (in particular omega-words) whose elements are weighted with natural …
Oct. 30, 2013, 2:15 p.m.
Matteo Mio (CWI - Amsterdam)
Game Semantics for Probabilistic mu-Calculi
In this talk I will consider (a family of) probabilistic (or quantitative) variants of Kozen's Modal mu-Calculus, designed for expressing properties of probabilistic-nondeterministic transition systems. Two type of semantics can be defined for these logics: …
Oct. 23, 2013, 2:15 p.m.
Matteo Mio (CWI - Amsterdam)
Foundations of Quantitative Logics based on Functional Analysis
Several notions of bisimulation relations for Probabilistic Nondeterministic Transition Systems (PNTS's) have been proposed in the literature. I will develop the theory of what I call "Upper-Expectation bisimilarity" using standard results of linear algebra and …
Oct. 16, 2013, 2:15 p.m.
Teodor Knapik (joint work with Didier Caucal) (University of New Caledonia)
Two MSO-compatible operations: Shelah-Stupp's iteration and Muchnik's iteration
In the early seventies, Shelah proposed a model-theoretic construction,nowadays called "iteration". This construction is an infinitereplication in a tree-like manner where every vertex possesses its owncopy of the original structure. Stupp proved that the decidability …
June 19, 2013, 2:15 p.m.
Aleksander Zabłocki (Uniwersytet Warszawski)
Squeezing theory into practice: automata in natural language processing
I will sketch some aspects of using automata in natural language processing: more precisely, in efficient applying a set of search-replace rules for richly annotated text. Although this might seem trivial (build-determinize-compose-run), our practical applications …
June 12, 2013, 2:15 p.m.
Laure Daviaud (LIAFA, Université Paris 7)
joint work with Thomas Colcombet
Distance automata are automata weighted over the semiring (N U {+infinity},min,+) (the tropical semiring). Such automata compute functions from words to N U {+infinity} such as the number of occurrences of a given letter. It …
June 5, 2013, 2:15 p.m.
Claire David (Université Paris-Est Marne-la-Vallée)
joint work with W.Czerwinski, K. Losemann, W. Martens
Intuitively, a regular expression is deterministic if, when reading a word from left to right without looking ahead, one always knows where in the expression the next symbol will be matched. The set of languages …