It is possible to subscribe to a daily updated calendar that contains appointments from the table below using the following URIs1:

  • For all seminars: http://www.math.tu-dresden.de/~mottet/cal/quantla.ics
  • For all large seminars (PIs): http://www.math.tu-dresden.de/~mottet/cal/quantla-no-student.ics

How to subscribe to calendars may differ between applications, for the Mac OS Calendar App go to File -> New Calendar Subscription... and supply one of the given URIs.

The color coding means:

: all participate
: Doctoral students participate
: next seminar

Please find the abstracts below the schedule and note that some of the slides are made available here, internally.

Date Time Topic Speaker Room
2018 Apr 10 13:00‑16:00
14:00-16:00
On Monadic Transitive Closure Logic MTC Wolfgang Thomas
(RWTH Aachen)
TU Dresden
APB E005
2018 Apr 17 13:00‑16:00 Functional Models and Data Complexity for FL0 Pavlos Marantidis
(Scholarship Holder)
TU Dresden
APB E005
Metric Temporal Description Logics with Interval-Rigid Names Patrick Koopmann
(TU Dresden)
2018 Apr 24 12:45‑16:00 Gossiping in Message-Passing Systems Paul Gastin
(ENS Cachan)
Universität Leipzig
P 501
Felix-Klein-Hörsaal
2018 May 08 13:00‑16:00 How hard is it to color a 3-colorable graph by a constant number of colors? Jakub Opršal
(TU Dresden)
TU Dresden
APB 3027
The Modal Logic of Generic Multiverses Jakob Piribauer
(Scholarship Holder)
2018 May 15 13:00‑16:00 - cancelled due to illness -

Leila Amgoud
(CNRS, Toulouse)

TU Dresden
APB E005
2018 May 22 14:00‑16:00 The Sequentialisation of Automata and Transducers Jacques Sakarovitch
(CNRS Paris)
Universität Leipzig
P 501
Felix-Klein-Hörsaal
2018 May 22-26 WATA 2018
2018 May 29 13:00‑16:00 Weighted ω Pushdown Automata Sven Dziadek
(Scholarship Holder)
Universität Leipzig
P 702
Felix-Klein-Hörsaal
Inconsistent Argumentation Markus Ulbricht
(Scholarship Holder)
2018 Jun 05 13:00‑16:00 TBA Benjamin Zarrieß
(TU Dresden)
TU Dresden
APB E005
2018 Jun 12 12:45‑16:00     Universität Leipzig
P 501
Felix-Klein-Hörsaal
2018 Jun 19 12:45‑16:00     Universität Leipzig
P 501
Felix-Klein-Hörsaal
2018 Jul 03 12:45‑16:00 TBA Joachim Hertzberg
(Universität Osnabrück)
Universität Leipzig
P 501
Felix-Klein-Hörsaal
2018 Jul 10 13:00‑16:00 TBA Marie-Laure Mugnier
(University of Montpellier)
TU Dresden
APB E005

 

1 This has been made possible by Antoine Mottet.



Abstracts


Wolfgang Thomas: On Monadic Transitive Closure Logic MTC

Monadic transitive closure Logic MTC is the extension of first-order logic by the construct that allows to pass from a formula F(x,y) to F*(x,y), expressing that a path from x to y exists where each step is in accordance with F. MTC is a very natural logic for expressing reachability properties. Despite this role it does not share the prominence that monadic second-order logic MSO enjoys. We survey results (and proof ideas) on the expressive power of MTC over the domains of finite words, finite ranked trees, and (labelled or unlabelled) finite two-dimensional grids. Over words, we recall the (not so well-known) proof that precisely the regular languages are definable in MTC, thus establishing here an equivalence between MSO and MTC. Over trees, MTC is located strictly between first-order logic FO and MSO (as well as between tree-walking automata and standard tree automata); these are nontrivial results of Bojanczyk, Colcombet, Segoufin, ten Cate, and others. Over grids the power of MTC is not yet clear; we are lacking a good method to show non-definability results for MTC. For example, it is open whether there are sets of unlabelled grids that are definable in existential monadic second-order logic EMSO but not in MTC.


Pavlos Marantidis: Functional Models and Data Complexity for FL0

In the early days of Description Logic research, the inexpressive DL FL0 was considered to be the smallest possible DL. When it was later shown that subsumption reasoning wrt general TBoxes is as hard as for the more expressive ALC, the community lost interest in this DL. However, the recent approach of reasoning with so-called functional models has rekindled the interest, since, on the one hand it has the potential to outperform ALC reasoners (even though it stays ExpTime-hard in the worst case), and on the other hand, it has already helped in answering open problems about non-standard inferences for FL0, like existence and computation of least common subsumer and most specific concept, and the exact data complexity of query answering.


Patrick Koopmann: Metric Temporal Description Logics with Interval-Rigid Names

Description logics are a well-established formalism to define terminological knowledge in so-called ontologies. Specifically, an ontology defines relations between concepts, which describe sets of individual objects, and may assign concepts to specific individual objects. In applications that deal with temporally changing information, specifying concepts and ontologies only statically is often insufficient. Motivated by this, extensions of description logics with temporal logics such as linear temporal logic (LTL) have been investigated. While LTL allows to speak about time only qualitatively (something happened at some point in the past), metric temporal logics allow to speak about time also in a quantitative manner (something happened in the last 5 minutes), which is often required in order to describe temporal behaviour accurately. This talk presents extensions of a description logic with metric temporal operators, and with a new formalism called interval-rigid names, which offer an additional way of specifying quantitative temporal constraints.


Paul Gastin: Gossiping in Message-Passing Systems

We study the gossip problem in a message-passing environment: When a process receives a message, it has to decide whether the sender has more recent information on other processes than itself. This problem is at the heart of many distributed algorithms, and it is tightly related to questions from formal methods concerning the expressive power of distributed automata. We provide a non-deterministic gossip protocol for message-passing systems with unbounded FIFO channels, using only finitely many local states and a finite message alphabet. We show that this is optimal in the sense that there is no deterministic counterpart. As an application, the gossip protocol allows us to show that message-passing systems capture well-known extensions of linear-time temporal logics to a concurrent setting.


Jakub Opršal: How hard is it to color a 3-colorable graph by a constant number of colors?

One of the well-known NP-complete problems is deciding whether a given (non-oriented) graph is colorable by 3 colors. We will focus on a more relaxed problem, decide which of the two is true: the given graph is colorable by 3 colors, or it is even colorable by k colors. If neither of the cases happen to be true, there are no requirements on the output of the algorithm. While this problem is generally believed to be NP-hard for each constant k, not much is known; in particular, NP-hardness is known only for k = 3 and 4. We will discuss how universal algebra can be used to give some answers.


Jakob Piribauer: The Modal Logic of Generic Multiverses

In contemporary set theory, forcing plays a crucial role for establishing independence results. The forcing construction, introduced by Cohen in 1963 to show the independence of the continuum hypothesis (CH) from ZFC, allows us to add new sets with well-controllable properties to models of ZFC. In this way, we can change the truth value of some independent sentences as e.g. CH. In 2008, Hamkins and Löwe introduced the modal logic of forcing as an analysis of the general patterns which this change of truth values exhibits by means of modal logic.

In this talk, we present a general set-up for a modal logic investigation of truth patterns obtained by arbitrary model constructions and generalize results about the modal logic of forcing by looking at generic multiverses, the forcing-connected components in the landscape of models of ZFC.