It is possible to subscribe to a daily updated calendar that contains appointments from the table below using the following URIs^{1}:
 For all seminars: http://www.math.tudresden.de/~mottet/cal/quantla.ics
 For all large seminars (PIs): http://www.math.tudresden.de/~mottet/cal/quantlanostudent.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
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:0016: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 FL_{0}  Pavlos Marantidis (Scholarship Holder) 
TU Dresden APB E005 
Metric Temporal Description Logics with IntervalRigid Names  Patrick Koopmann (TU Dresden) 

2018 Apr 24  12:45‑16:00  Gossiping in MessagePassing Systems  Paul Gastin (ENS Cachan) 
Universität Leipzig P 501 FelixKleinHörsaal 
2018 May 08  13:00‑16:00  How hard is it to color a 3colorable 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   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 FelixKleinHörsaal 
2018 May 2226  WATA 2018  
2018 May 29  13:00‑16:00  Dynamic Programming and Weighted Automata  Sven Dziadek (Scholarship Holder) 
Universität Leipzig P 702 FelixKleinHörsaal 
Inconsistent Argumentation  Markus Ulbricht (Scholarship Holder) 

2018 Jun 05  13:00‑16:00  Complexity of Projection with Stochastic Actions in a Probabilistic Description Logic  Benjamin Zarrieß (TU Dresden) 
TU Dresden APB E005 
2018 Jun 12  12:45‑16:00  Weighted automata and networks  Miroslav Ćirić (University of Niš) 
Universität Leipzig P 501 FelixKleinHörsaal 
2018 Jun 19  12:45‑16:00  Costs and Rewards in Priced Timed Automata  Mahsa Shirmohammadi (Université AixMarseille) 
Universität Leipzig P 501 FelixKleinHörsaal 
Bounded Model Checking of Onecounter Automata for MTL  Danny Richter (Associated Doctoral Student) 

2018 Jul 03  12:45‑16:00  What your Robot still needs to Know about its Environment once all is SLAMmed  Joachim Hertzberg (Universität Osnabrück) 
Universität Leipzig P 501 FelixKleinHörsaal 
2018 Jul 10  13:00‑16:00  Answering Conjunctive Regular Path Queries over Existential Rule Knowledge Bases  MarieLaure 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 firstorder 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 secondorder 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 twodimensional grids. Over words, we recall the (not so wellknown) 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 firstorder logic FO and MSO (as well as between treewalking 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 nondefinability results for MTC. For example, it is open whether there are sets of unlabelled grids that are definable in existential monadic secondorder logic EMSO but not in MTC.
Pavlos Marantidis: Functional Models and Data Complexity for FL_{0}
In the early days of Description Logic research, the inexpressive DL FL_{0} 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 socalled functional models has rekindled the interest, since, on the one hand it has the potential to outperform ALC reasoners (even though it stays ExpTimehard in the worst case), and on the other hand, it has already helped in answering open problems about nonstandard inferences for FL_{0}, 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 IntervalRigid Names
Description logics are a wellestablished formalism to define terminological knowledge in socalled 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 intervalrigid names, which offer an additional way of specifying quantitative temporal constraints.
Paul Gastin: Gossiping in MessagePassing Systems
We study the gossip problem in a messagepassing 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 nondeterministic gossip protocol for messagepassing 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 messagepassing systems capture wellknown extensions of lineartime temporal logics to a concurrent setting.
Jakub Opršal: How hard is it to color a 3colorable graph by a constant number of colors?
One of the wellknown NPcomplete problems is deciding whether a given (nonoriented) 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 NPhard for each constant k, not much is known; in particular, NPhardness 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 wellcontrollable 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 setup 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 forcingconnected components in the landscape of models of ZFC.
Benjamin Zarrieß: Complexity of Projection with Stochastic Actions in a Probabilistic Description Logic
Integrating probabilistic notions of uncertainty into languages for reasoning about actions is a popular approach to adequately deal for instance with possibly fallible acting and sensing. In this talk, an action language extended with quantitative notions of uncertainty is considered. In our setting, the initial beliefs of an agent are represented as a probabilistic knowledge base with axioms formulated in the Description Logic ALCO. Action descriptions describe the possibly contextsensitive and nondeterministic effects of actions and provide likelihood distributions over the different possible outcomes. A decidability result for the probabilistic projection problem, which is the basic reasoning task needed for predicting the outcome of action sequences, is presented. Furthermore, we look at the problem of how the nondeterminism in the action model affects the complexity of the projection problem.
Miroslav Ćirić: Weighted automata and networks
In large and complex networks it is impossible to understand the relationship between each pair of actors, but to a certain extent, it may be possible to understand the system, by classifying actors and describing relationships on the class level. Actors in the same class can be considered to occupy the same position, or play the same role in the network. Positional analysis is a branch of social network analysis whose main aim is to identify the position or role of actors in the network on the basis of relationships between them. For instance, in a terrorist or criminal network, roles should be identified on the basis of communication between members, without insight into the content of the conversation.
In this talk, we deal with positional analysis of onemode, twomode and multimode weighted networks by applying the ideas and methodology we have developed for solving some fundamental problems of the theory of multivalued and weighted automata, e.g. state reduction, simulation and bisimulation.
Joachim Hertzberg: What your Robot still needs to Know about its Environment once all is SLAMmed
Map building, or rather, Simultaneous Localization and Mapping (SLAM), is one of the fundamental abilities that autonomous mobile robots need to have for acting in a goaldirected way in a priori unknown environments. SLAM is known to be solved in many, if not most instances. A map selfacquired via SLAM would set the spatial frame for all of the robot's spacerelated knowledge and action. Still, as there is more to do for a mobile robot than navigate, there is more for it to know about its environment than landmarks, traversable area, and occupied and free space. Anchoring many sorts of knowledge to space is needed in addition to, and hopefully in combination with, basic SLAM.
The talk reviews own work about a SLAM approach that is part of autonomous environment exploration. It explains how to extend it into building semantic maps for serving many more purposes than just navigation. And it speculates about ways for robots to handle the symbolic knowledge that comes with a semantic map under the regular robots' plagues of change and sensing error.
MarieLaure Mugnier: Answering Conjunctive Regular Path Queries over Existential Rule Knowledge Bases
Ontologymediated query answering is concerned with the problem of answering queries over knowledge bases consisting of a database instance and an ontology. In this talk, I will first review the framework of existential rules and their relationships with description logics. I will in particular focus on two classes of existential rules, for which the problem of answering conjunctive queries is decidable, and even tractable in terms of data complexity, namely linear rules, a natural extension of DLLite_R, and the wider class of (frontier) guarded rules (which generalizes for instance the DL ELHI). While most work in ontologymediated query answering focuses on conjunctive queries, navigational queries (like regular path queries) are gaining increasing attention. I will present recent results on the complexity of answering conjunctive regular path queries, a class of queries that generalizes both conjunctive queries and regular path queries, over linear and guarded knowledge bases.
These results are joint work with JeanFrancois Baget, Meghyn Bienvenu and Michael Thomazo.