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

• 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

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

¹ 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 FL₀

In the early days of Description Logic research, the inexpressive DL FL₀ 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 FL₀, 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.

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 context-sensitive and non-deterministic 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 non-determinism 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 one-mode, two-mode and multi-mode weighted networks by applying the ideas and methodology we have developed for solving some fundamental problems of the theory of multi-valued 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 goal-directed way in a priori unknown environments. SLAM is known to be solved in many, if not most instances. A map self-acquired via SLAM would set the spatial frame for all of the robot's space-related 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.

Marie-Laure Mugnier: Answering Conjunctive Regular Path Queries over Existential Rule Knowledge Bases

Ontology-mediated 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 DL-Lite_R, and the wider class of (frontier) guarded rules (which generalizes for instance the DL ELHI). While most work in ontology-mediated 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 Jean-Francois Baget, Meghyn Bienvenu and Michael Thomazo.