The color coding means:

: all participate
: Doctoral students participate

Date Time Topic Speaker Room
2016 Apr 5 13:30-16:00 Probabilistic Abstract Argumentation Matthias Thimm
(Universität Koblenz)
Universität Leipzig
P 501 Felix-Klein-Hörsaal
2016 Apr 12 13:30-16:00 MSO+U Mikołaj Bojańczyk
(University of Warsaw)
TU Dresden
APB E005
2016 Apr 26 13:30-16:00 Uniform Interpolation for Expressive Description Logics Patrick Koopmann 
(University Oxford)
TU Dresden
APB E005
Reducts of finitely bounded homogeneous structures, and lifting tractability from finite-domain constraint satisfaction Antoine Mottet
(TU Dresden)
Internal Student Meeting
2016 May 3 13:30-16:00 Playing Games in the Baire Space Wolfgang Thomas
(RWTH Aachen)
Universität Leipzig
P 501 Felix-Klein-Hörsaal
2016 May 10 13:30-16:00 Open-World Probabilistic Databases Ismail Ceylan
(TU Dresden)
TU Dresden
APB E005
2016 May 17 - 20 Spring School
2016 May 24 13:30-16:00 Compositional matrix-space models in natural language processing Shima Asaadi
(TU Dresden)
TU Dresden
APB E005
2016 May 30 - 31 DFG Review Meeting TU Dresden
2016 Jun 7 13:30-16:00 Weighted Automata and Logics for Infinite Nested Words Stefan Dück
(Universität Leipzig)
Universität Leipzig
P 502
On the Quantitative Linear Dynamic Logic George Rahonis
(Aristotle University of Thessaloniki)
2016 Jun 14 13:30-16:00 Probabilistic Programming: Semantics, Termination and Run Times Joost-Pieter Katoen
(RWTH Aachen)
TU Dresden
APB E005
2016 Jun 21 14:00-16:00 Operator precedence languages: new perspectives for an old-fashioned language family Dino Mandrioli
(Politecnico di Milano)
Universität Leipzig
P 501 Felix-Klein-Hörsaal
2016 Jun 28 13:30-16:00 Navigational queries and expressive Description Logics for data management Magdalena Ortiz
(TU Wien) 
TU Dresden
APB E005





Abstracts


Matthias Thimm: Probabilistic Abstract Argumentation

In this talk, we consider augmenting abstract argumentation frameworks with probabilistic information and discuss different constraints to obtain meaningful probabilistic information. We also address the scenario when assessments on the probabilities of a subset of the arguments are given and the probabilities of the remaining arguments have to be derived, taking both the topology of the argumentation framework and principles of probabilistic reasoning into account. We generalize this scenario by also considering inconsistent assessments, i. e., assessments that contradict the topology of the argumentation framework.


Mikołaj Bojańczyk: MSO+U

By famous results of Büchi and Rabin, satisfiability is decidable for MSO on words and trees, both finite and infinite. Can one add something nontrivial to MSO and still retain decidable satisfiability? MSO+U is a logic designed with this in question in mind. In MSO+U, which only makes sense for infinite structures, one extends MSO with a quantifier that can say things like "φ(X) is true for sets X of arbitrarily large size”. In the talk, I will summarise the current state of knowledge on this logic. There are positive results (fragments of the logic are decidable on infinite words and trees, typically using automata with counters) and negative results (the full logic is undecidable).


Patrick Koopmann: Uniform Interpolation for Expressive Description Logics

Description Logics are a family of logics that are used to model ontologies, terminological knowledge bases that are used to represent domain knowledge in a range of areas such as the semantic web, medicine, biology and many more. Uniform interpolation restricts the vocabulary used in an ontology to a specified set of terms, such that information expressible in this vocabulary is preserved. It has potentially many applications, such as in ontology reuse or ontology analysis. The theoretical properties of uniform interpolation in description logics are not encouraging for practical applications: finite representations do not always exist in classical description logics, and the size can be triple exponential with respect to the size of the input already for simpler description logics. We present an approach based on resolution that allows to compute uniform interpolants in various expressive description logics practically in a lot of cases. An evaluation on realistic ontologies shows a high success rate despite the known worst-case complexities.


Antoine Mottet: Reducts of finitely bounded homogeneous structures, and lifting tractability from finite-domain constraint satisfaction

Constraint satisfaction problems (CSPs) appear in many areas of computer science: database theory, qualitative and quantitative reasoning, optimization, … Given a relational structure A, the constraint satisfaction problem of A is the problem that takes as input a finite structure B and that asks whether there is a homomorphism from B to A. While the definition allows for finite and infinite structures A, CSPs have most extensively been studied for finite structures. The theory of finite-domain constraint satisfaction is therefore rather more advanced than its infinite counterpart. I will present a recent reduction that allows to apply results from finite-domain constraint satisfaction to a large class of infinite structures, namely the first-order reducts of finitely bounded homogeneous structures. As time permits, I will also present how to use this in order to derive a full complexity classification of the CSPs of structures that are definable with atoms (modulo the dichotomy conjecture for finite-domain CSPs). The mentioned results have been accepted for publication at LICS, and are joint work with Manuel Bodirsky.


Wolfgang Thomas: Playing Games in the Baire Space

An central step in studying "quantitative models" is the move from Boolean values to values of an infinite domain (such as the set N of natural numbers). We present recent work on this question by solving Church's synthesis problem (on constructing winning strategies of infinite two-player games) in a setting where a play is a sequence of natural numbers rather than a sequence of bits; so a play is an element of the Baire space rather than of the Cantor space. To specify winning conditions we present a natural model of automata ("N-memory automata") equipped with the parity condition, and we introduce corresponding "N-memory transducers". We show that games specified by N-memory parity automata are solvable in the sense that one can decide who wins and - for the winner - construct an N-memory transducer that executes a winning strategy.


Ismail Ceylan: Open-World Probabilistic Databases

Large-scale probabilistic knowledge bases are becoming increasingly important in academia and industry alike. They are constantly extended with new data, powered by modern information extraction tools that associate probabilities with database tuples. In this work, we revisit the semantics underlying such systems. In particular, the closed-world assumption of probabilistic databases, that facts not in the database have probability zero, clearly conflicts with their everyday use. To address this discrepancy, we propose an open-world probabilistic database semantics, which relaxes the probabilities of open facts to intervals. While still assuming a finite domain, this semantics can provide meaningful answers when some probabilities are not precisely known. For this open-world setting, we propose an efficient evaluation algorithm for unions of conjunctive queries. Our open-world algorithm incurs no overhead compared to closed-world reasoning and runs in time linear in the size of the database for tractable queries. All other queries are #P-hard, implying a data complexity dichotomy between linear time and #P. For queries involving negation, however, open-world reasoning can become NP-, or even NP^PP-hard. Finally, we discuss additional knowledge-representation layers that can further strengthen open-world reasoning about big uncertain data.


Shima Asaadi: Compositional matrix-space models in natural language processing

Quantitative models of language have been the subject of intense research in the last two decades: statistical and vector-space models and its variations are prominently used in sentiment analysis and other fields of natural language processing (NLP). In the application of “meaning representation” of text in NLP, vector-space models embody the distributional hypothesis of meaning, according to which the meaning of words is defined by contexts in which they (co-)occur. However, until recently, little attention has been paid to the task of modeling more complex conceptual text structures (e.g. sentence). Recently, compositional matrix-space models of language are proposed for the representation of the meaning of complex text structures. They have been shown to subsume many of known models, both quantitative (vector-space models with diverse composition operation) and qualitative (regular languages, languages based on group theory). However training such models should be done carefully. In this talk we show the correspondence between these models and weighted finite automata so that the problem of learning such matrix-based models can be mapped to the problem of learning weighted finite automata.


Stefan Dück: Weighted Automata and Logics for Infinite Nested Words

Nested words introduced by Alur and Madhusudan are used to capture structures with both linear and hierarchical order, e.g. XML documents, without losing valuable closure properties. Furthermore, Alur and Madhusudan introduced automata and equivalent logics for both finite and infinite nested words, thus extending Büchi's theorem to nested words. Recently, average and discounted computations of weights in quantitative systems found much interest. Here, we will introduce and investigate weighted automata models and weighted MSO logics for infinite nested words. As weight structures we consider valuation monoids which incorporate average and discounted computations of weights as well as the classical semirings. We study several fragments of this weighted logic and show that under suitable restrictions the weighted logic has the same expressive power as weighted nested word automata.


George Rahonis: On the Quantitative Linear Dynamic Logic

Giuseppe De Giacomo and Moshe Vardi introduced in 2013, a combination of propositional dynamic logic and LTL, called linear dynamic logic, which combines the complexity properties of reasoning on LTL and the expressive power of finite automata. We present results, from a recent work with Manfred Droste, on quantitative linear dynamic logic.


Joost-Pieter Katoen: Probabilistic Programming: Semantics, Termination and Run Times

Probabilistic programs are used in different application areas, ranging from machine learning to security, software-defined networking and quantum computing. In this talk, I’ll discuss some semantic issues of probabilistic programming languages and present several nuances of termination: whereas ordinary program termination is about whether a program has an infinite run or not, for probabilistic programs this is much more delicate. I’ll show that almost-sure termination — does a program terminate with probability one? — is "more undecidable" than ordinary termination, and discuss that a program may almost surely terminate although this may on average take an infinite amount of steps. Finally, I’ll sketch a variant of Dijkstra’s wp-calculus to establish the expected run-time of a probabilistic program and treat its usage to some classical randomized algorithms.


Dino Mandiroli: Operator precedence languages: new perspectives for an old-fashioned language family

Operator precedence (OP) grammars and languages have been invented by R. Floyd half a century ago to support efficient, deterministic, parsing of programming languages; not only they proved successful in the compiler construction field, but they also exhibited some “clean” algebraic properties. Nevertheless, their investigation has been abandoned, mainly due to advent of more powerful grammars, typically the LR ones, which generate all deterministic context-free languages. After several decades of oblivion, however, we intensively resumed their study and application under two, seemingly unrelated, major motivations: on the one hand we argue that they enable parsing algorithms that exploit modern parallel architectures much more effectively than those in use in the present state of the practice; on the other hand they enjoy the same algebraic and logic properties as regular languages and other families that ignited the great success of automatic verification techniques such as model-checking, but have a much greater generative power than those families. Precisely, OP languages are closed under all major language operations, thus the containment problem is decidable for them, and admit a logic characterization in terms of a monadic second-order logic as well as regular languages and so-called visibly push-down languages, which are strictly contained in the OP family. We also argue that many other recent research results obtained for smaller classes of languages can be extended to the OP one.


Magdalena Ortiz: Navigational queries and expressive Description Logics for data management

Description Logics (DLs), extensively studied in Knowledge Representation and widely advocated as ontology languages, can provide powerful tools for managing and querying graph-structured data. However, this scenario calls for very expressive ontology and query languages, capable of expressing reachability patters and flexible path navigation. As we illustrate in this talk, these features can be often accommodated at little or no computational cost, making the languages much better suited for ontology-enriched data management. We will recall some important results that have been derived in this area using automata, emphasising the power of this technique for pushing decidability and computational complexity upper bounds to both very expressive ontology languages, and very flexible query languages with advanced navigational capabilities. We will also discuss some recent research where these rich languages and their automata-based algorithms are proving fruitful for tackling other data management challenges, like reasoning about evolving data.