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
Please find the abstracts below the schedule and note that some of the slides are made available here, internally.
1 This has been made possible by Antoine Mottet.
Abstracts
Dietrich Kuske: Hanf locality of counting extensions of first-order logic
We introduce a logic that extends first-order logic by counting, integer variables, and by numerical predicates. This logic can be viewed as joint generalization of various counting logics that have been studied in the literature.
We obtain a locality result showing that every formula of this logic can be transformed effectively into a formula in Hanf normal form that is equivalent on all finite structures of fixed bounded degree. A formula is in Hanf normal form if it is a Boolean combination of formulas describing the neighbourhood around its tuple of free variables and arithmetic sentences with numerical predicates over atomic statements describing the number of realizations of a type with a single center.
From this locality result, we infer the following applications:
- The Hanf-locality rank of first-order formulas of bounded quantifier alternation depth only grows polynomially with the formula size.
- The model checking problem for a natural fragment of our logic on structures of bounded degree is fixed-parameter tractable.
- The query evaluation problem for fixed queries from the fragment over fully dynamic databases of bounded degree can be solved efficiently: there is a dynamic algorithm that can enumerate the tuples in the query result with constant delay, and that allows to compute the size of the query result and to test if a given tuple belongs to the query result within constant time after every database update.
(These results are joint work with Nicole Schweikardt.)
Rafael Peñaloza Nyssen: Consequence-preserving Ontology Repair
We consider the problem of repairing an ontology in order to exclude some unwanted (implicit) consequences or errors from it. In order to preserve as much of the original knowledge as possible, we propose to weaken--rather than remove--the axioms causing these errors.
During this talk we will see that applying this simple idea in Description Logics is not as simple as it looks at first sight. In particular, we need to study generalization and specialization operators; revisit the notions of diagnoses and repairs; and develop methods for finding preferred solutions. This presentation will provide a few answers, and many more questions.
Caterina Viola: A maximally tractable class of VCSPs
I will show the maximal tractability of submodular valued constraint languages among the class of piecewise - scalar languages. The proof of this result is based on the maximal tractability of submodular languages among the class of languages over a finite domain (Cohen-Cooper-Jeavons-Krokhin, 2006), which in turn is based on the NP-hardness of the Max-Cut problem.
Joint work with M. Bodirsky and M. Mamino
Gustav Grabolle: Multivalued Dynamic Logic
We are going to establish a weighted linear dynamic logic over non-distributive structures, such as lattices or bi-locally finite strong bimonoids. To this purpose, we will show that formal power series over non-distributive structures are in general not closed under a recursively defined Kleene-operator and propose a solution to this deficiency. Furthermore, we will prove the correctness of certain representation of rational operations on recognizable step functions over lattices.
Helmut Seidl: Polynomial Tree Automata
A polynomial tree automaton can be considered as an attribute grammar with synthesized attributes only where the values of attributes at a node are determined by means of polynomial functions from the attributes of the child nodes.
The presentation explains how the equivalence problem for various classes of tree-to-string transducers can be reduced to the question whether or not a conjunction of polynomial equalities holds for all possible attribute values at the root. In particular, we consider the classes of linear deterministic tree-to-string transducers, streaming tree transducers, and general deterministic topdown tree-to-string transducers.
We prove that polynomial equalities are decidable for general polynomial tree automata. This central result is obtained by relying on inductive polynomial invariants, as known from program proving, and abstract interpretation. We also identify subclasses of polynomial automata where explicit complexity bounds can be provided. We then show how these algorithms give rise to decision procedures of tree-to-string transducers. In particular, we obtain explicit complexity bounds for the equivalence problem for deterministic linear as well as deterministic streaming tree transducers.
Joint work with Sebastian Maneth (Bremen) and Gregor Kemper (München).
Markus Holzer: Reversible Finite Automata
Reversibility is a fundamental concept in physics, with application also in computer science. A reversible computation combines a classical deterministic forward-computation with a deterministic backward-computation such that one from the result of the computation one can reconstruct the initial situation. One motivation to study reversible computation comes from the idea to overcome the limits of classical computations. In 1973 Bennet showed that classical Turing machine and their irreversible computations can be simulated by reversible computations. Since then several other reversible automata models were studied in the literature such, e.g., reversible pushdown automata, reversible multi-head automata, etc. Also reversible finite automata were introduced by Angluin (1982), Pin (1992), and Ambainis & Freivalds (1998). These automata models differ in the number of initial and final states only. We give an overview on well-known and new results on reversible finite automata, with a focus on Ambainis & Freivalds reversible finite automata, which were recently investigated in several conference papers. Some of the presented results were obtained with the co-authors Holger Bock Axelsen, Sebastian Jakobi, and Martin Kutrib.
Daniel Gburek: Bisimulation and logics for stochastic systems with rewards
Stochastic systems with rewards yield a generic stochastic model where both the state and the action space might be uncountable and where every action is decorated by a real-valued reward. We present a characterisation of the bisimulation relation in terms of an expressive action-based probabilistic logic and show that this characterisation is still maintained by a small fragment of this logic.
Johannes Greiner: A short introduction to model theory
This session is meant to be interactive and to familiarize the audience with basic notions of model theory. The presented (classical) theorems are meant to give a basis to understand current research on infinite domain CSPs.
Benedikt Bollig: Communicating Finite-State Machines and Two-Variable Logic
In the early 1960s, Büchi, Elgot, and Trakhtenbrot showed that finite automata over words have the same expressive power as monadic second-order (MSO) logic. Since then, this fundamental theorem has been generalized to other computational devices such as tree automata, asynchronous automata, nested-word automata, and branching automata. Actually, all these devices are complementable, which allows for an inductive translation of formulas into automata. In this talk, we consider communicating finite-state machines (CFMs), introduced by Brand and Zafiropulo in 1983. CFMs are a basic model of finite-state processes that communicate via unbounded FIFO channels. Unfortunately, they are not complementable. In fact, they are strictly less expressive than MSO logic (interpreted over certain partial orders). Nevertheless, CFMs enjoy logical characterizations in terms of fragments of MSO logic. In this talk, we will show that CFMs are expressively equivalent to existential MSO logic with two first-order variables. As the main feature, the logic supports the happens-before relation, which reflects causality in an execution of a distributed system.
This is joint work with Marie Fortin and Paul Gastin.
Christoph Haase: Presburger arithmetic and semi-linear sets: the past, the present and the future
Presburger arithmetic, the first-order theory of the natural numbers with addition and order, is a fragment of number theory that was shown decidable in 1929 by Mojzesz Presburger in his Master's thesis. Seymour Ginsburg and Edwin Spanier showed in 1966 that the sets definable in Presburger arithmetic coincide with semi-linear sets, a generalisation of ultimately periodic sets to higher dimensions. The goal of this talk is to give a comprehensive overview about Presburger arithmetic and semi-linear sets, about their relationship, history and notable results. I will also discuss in more detail some recent work on the descriptive complexity of Boolean operations on semi-linear sets.
This talk is partly based on joint work with Dmitry Chistikov.
Kevin Stier: A Convergence Result on Binomial Markets with Transaction Costs
In this talk, we shortly discuss the classical binomial model and replication as a way of option price determination. Afterwards we introduce transaction costs and analyze two results concerning the super-replication costs of European contingent claims and sketch their proofs.
Erik Paul: Nivat's Theorem for Turing Machines Based on Unsharp Quantum Logic
We present a Nivat theorem for Turing machines based on unsharp quantum logics, i.e., logics where the truth values are taken in a quantum multi-valued (QMV) algebra. More precisely, we show that the weighted languages recognizable by quantum multi-valued Turing machines are exactly those which can be constructed from particularly simple weighted languages recognizable by QMV-Turing machines, restricted to classical recursively enumerable languages, and projections.
Ivan Varzinczak: Next Steps in Reasoning Defeasibly over Description-Logic Ontologies
Description Logics (DLs) are a family of logic-based knowledge representation formalisms with appealing computational properties and a variety of applications at the confluence of modern artificial intelligence and other areas. In particular, DLs are well-suited for representing and reasoning about ontologies and therefore constitute the formal foundations of the Semantic Web. The different DL formalisms that have been proposed in the literature provide us with a wide choice of constructors in the object language. However, these are intended to represent only classical, unquestionable knowledge, and are therefore unable to express and cope with the different aspects of uncertainty and vagueness that often show up in everyday life. Examples of these comprise the various guises of exceptions, typicality (and atypicality), approximations and many others, as usually encountered in the different forms of human quotidian reasoning. A similar argument can be put forward when moving to the level of entailment, that of the sanctioned conclusions from a knowledge base. DL systems provide for a variety of (standard and non-standard) reasoning services, but the underlying notion of entailment remains classical and therefore, depending on the application one has in mind, DLs inherit most of the criticisms raised in the development of the so-called non-classical logics. In this regard, endowing DLs and their associated reasoning services with the ability to cope with defeasibility is a natural step in their development. Indeed, the past two decades have witnessed the surge of many attempts to introduce non-monotonic reasoning capabilities in a DL setting. Among these are default extensions, preferential approaches, circumscription-based ones, and others. In spite of all the progress that has been achieved in the area, the study of non-monotonic reasoning in DLs remains a large avenue for exploration. To witness, the bulk of the effort in this direction has been put only in the definition of accounts of defeasible subsumption and in the characterisation of appropriate notions of defeasible entailment relations. This suggests that existing approaches to reasoning with defeasible inheritance and typicality in ontologies lack constructors that are important from a modelling perspective. Indeed, here we make a case for a number of additional defeasible constructs at the object level enriching the basic DL concept language and propose a corresponding preferential semantics. We show that this does not negatively affect decidability or complexity of reasoning for an important class of DLs, and that existing notions of preferential reasoning can be expressed in terms of our new constructs. In particular, we show how our semantic definitions are fruitful in providing a notion of contextual defeasible subsumption, which allows for an even more fine-grained treatment of exceptions.
Piero Bonatti: KR for Security and Security for KR
Knowledge representation languages such as RDF and OWL are increasingly being used to encode sensitive information. Moreover, a growing amount of knowledge is public, and developers are encouraged to re-use open ontologies. Such application scenarios introduce a new range of confidentiality and integrity risks specifically related to automated inference. Such vulnerabiities call for appropriate security models. A range of solid methods for inference-proof query answering - developed in the area of security - can be profitably adapted to protect confidential knowledge bases, while integrity problems have been addressed with non-standard inference methods.
On the other hand, security and privacy policies have all the characteristic features of knowledge. The same is true of the formal consent to personal data processing that will be required by the forthcoming European General Data Protection Regulation (GDPR). Then knowledge representation languages can be profitably used to formalize policies, and inference engines can be exploited for compliance checking, policy validation, and several other reasoning tasks related to policies.
In this talk we briefly overview some of the mutual relationships between KR&R (Knowledge Representation and Reasoning), and S&P (Security and Privacy), pointing to some opportunities for cross-fertilization.
Gerhard Lakemeyer: Reasoning about Probabilities in Unbounded First-Order Dynamical Domains
When it comes to robotic agents operating in an uncertain world, a major concern in knowledge representation is to better relate high-level logical accounts of belief and action to the low-level probabilistic sensorimotor data. Perhaps the most general formalism for dealing with degrees of belief and, in particular, how such beliefs should evolve in the presence of noisy sensing and acting is the account by Bacchus, Halpern, and Levesque. In this paper, we reconsider that model of belief, and propose a new logical variant that has much of the expressive power of the original, but goes beyond it in novel ways. In particular, by moving to a semantical account of a modal variant of the situation calculus based on possible worlds with unbounded domains and probabilistic distributions over them, we are able to capture the beliefs of a fully introspective knowledge base with uncertainty by way of an only-believing operator. The paper introduces the new logic and discusses key properties as well as examples that demonstrate how the beliefs of a knowledge base change as a result of noisy actions.
This is joint work with Vaishak Belle.
