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.
1 This has been made possible by Antoine Mottet.
The valued constraint satisfaction problem (VCSP) is a framework for studying the computational complexity of classes of discrete optimisation problems. It was introduced as an optimisation version of the constraint satisfaction problem (CSP), where the goal is to assign labels to variables under some given set of constraints. The VCSP captures both Max CSP-type problems, where one wants to optimise the number of satisfied constraints and integer programming-type problems, where one adds an objective function to an ordinary CSP to indicate the desirability of each assignment.
As the VCSP is hard in general, any meaningful study of its complexity requires restricting the problem in some way. One can, for example, restrict the type of cost functions that are allowed to appear in the description of an instance. Another possibility is to restrict the structure of the instance, that is, the way that cost functions are combined. I will talk about problems, algorithms, and hardness results in the context of various such restrictions.
Translations from Linear Temporal Logic (LTL) to various types of automata on infinite words have been studied extensively. They are a central part of the automata-theoretic approach to model checking. The idea is to reduce the question of whether a system satisfies a property, which is given as an LTL-formula, to the emptiness check of an automaton. A standard automaton model that is used to represent LTL formulas are non-deterministic Büchi automata (NBA).
In this talk, I will introduce an algorithm for translating LTL to NBA and show how it can be adapted to produce unambiguous Büchi automata (UBA). Unambiguity is a restricted form of determinism and may be used in cases where determinism is required in classical approaches. For example, a polynomial time algorithm for model checking Markov chains against UBA-properties is known, which is not possible for properties specified by NBA.
In this talk, I will provide some insights into the proof of the decidability of the finite sequentiality problem for unambiguous max-plus tree automata. A max-plus tree automaton is called unambiguous if there is at most one accepting run on every tree. The finite sequentiality problem asks whether for a given max-plus tree automaton, there exist finitely many deterministic max-plus tree automata whose pointwise maximum is equivalent to the given automaton.
Although optical character recognition (OCR) quality has improved substantially over the last decade, it still struggles on historic material. Instead of developing historical models for existing OCR, it can be prudent to first build complementary tools for post-correction, which feed from all visual and contextual cues of OCR itself, but maintain their own comprehensive models. Many existing post-correction approaches employ weighted finite-state transducers (WFST), which allow for compact storage and processing of symbol sequences. Using prior knowledge on what mistakes OCR typically makes, how new words are formed grammatically, and which words are likely to appear next to each other,a post-correction system can be modelled as the composition of single transducers representing input character hypotheses, error model, lexicon, and word-level language model, each weighted with probabilities.
In this talk, I will discuss the basics and challenges of OCR post-correction using WFST in the context of the joint coordinated research effort OCR-D, which is aimed at developing OCR methods for printed historic material in preparation of automated mass-digitisation of all German-speaking prints from the 16th to 19th century.
In this talk, we consider a weighted Feferman-Vaught decomposition theorem for disjoint unions and products of finite structures. The classical Feferman-Vaught Theorem describes how the evaluation of a first order sentence in a generalized product of relational structures can be reduced to the evaluation of sentences in the contributing structures and the index structure. The logic we employ for our weighted extension is based on the weighted MSO logic introduced by Droste and Gastin to obtain a Büchi-type result for weighted automata. We show that for disjoint unions and products of structures, the evaluation of formulas from two respective fragments of the logic can be reduced to the evaluation of formulas in the contributing structures. We also prove that the respective restrictions are necessary. Surprisingly, for the case of disjoint unions, the fragment is the same as the one used in the Büchi-type result of weighted automata. In fact, even the formulas used to show that the respective restrictions are necessary are the same in both cases. However, here proving that they do not allow for a Feferman-Vaught-like decomposition is more complex and employs Ramsey’s Theorem.
Different semantics of abstract Argumentation Frameworks (AFs) provide different levels of decisiveness for reasoning about the acceptability of conflicting arguments. The stable semantics is useful for applications requiring a high level of decisiveness, as it assigns to each argument the label “accepted” or the label “rejected”. Unfortunately, stable labellings are not guaranteed to exist, thus raising the question as to which parts of AFs are responsible for this non-existence. In this talk, I will discuss this issue by investigating a more general question concerning preferred labellings (which may be less decisive than stable labellings but are always guaranteed to exist): why a given preferred labelling may not be stable and thus undecided on some arguments.
The Weisfeiler-Leman algorithm is a simple polynomial-time algorithm that solves the graph isomorphism problem heuristically, that is, it may sometimes fail to distinguish two graphs G,H even though they are not isomorphic. Which pairs of graphs G,H are correctly distinguished by the algorithm? There are various known characterizations, using counting logics, using the Sherali-Adams hierarchy in linear programming, and using pebble games. We add a new characterization that is based on classic works of Lovász on the numbers of graph homomorphisms. In the talk, we also discuss some relations to subgraph counting algorithms as well as machine learning.
(Joint work with Martin Grohe and Gaurav Rattan)
Sliding-window streaming algorithms get as input a stream of data values and have to answer queries about the last n values for a certain window size n. In the talk we consider queries that are given by regular languages. More precisely, we consider the so-called sliding window word problem for a language L: Given a data stream of symbols a1 a2 a3 a4 ..., answer at every time instant t, whether at-n+1 ... at belongs to L. We are mainly interested in the space complexity of this problem measured in the window length n. For regular languages, we prove that the space complexity of the sliding window word problem is either constant, logarithmic, or linear. Moreover, for the constant and logarithmic space classes we provide very natural characterizations: For every regular language L the sliding window word problem can be solved in
(i) constant space if and only if L is a boolean combination of regular length languages and suffix-testable languages and in
(ii) logarithmic space if and only if L is a boolean combination of regular length languages and regular left ideals. If we allow randomized streaming algorithms with a two-sided error, then the above space trichotomy becomes a space quatrochotomy: for every regular languages, the space complexity of the sliding window word problem is either constant, doubly logarithmic, logarithmic, or linear.
(joint work with Moses Ganardi and Danny Hucke)
Founded in the early 2000s by Denecker, Marek and Truszczynski, approximation fixpoint theory (AFT) is an abstract, algebraic theory to characterize semantics of non-monotonic logics. In recent years, interest in AFT has gradually increased, with applications now ranging from foundations of database theory to abstract argumentation.
In this presentation, we provide an overview of the field: we start from the motivations that drove Denecker et al to the conception of this field, discuss both theoretical developments and applications, and end with potential topics for future improvements.
Of particular interest in this presentation is the application of AFT for (weighted) argumentation.
A finite word transduction is a binary relation of finite words. After an introduction on recent results about word transductions, in particular about logics and automata for word transductions and their connections, the talk introduces a new logic to specify properties of word transductions. This logic will lead us to a new characterization of the robust class of so called regular transductions. Decidability results for model-checking and synthesising transductions are also presented. Finally, a strong connection between transductions and data words (over an infinite alphabet) is given, leading to a new decidable logic for data words.
James Worrell: Synthesis of Algebraic and Semi-Algebraic Invariants
Invariants are one of the most fundamental and useful notions in automated verification, dynamical systems, and control theory. Current research on invariant generation employs an eclectic array of techniques, including abductive inference, abstract interpretation, constraint solving, interpolation, and machine learning. In this talk we give a select overview of previous work on invariant synthesis, focussing on a simple class of programs with affine updates. Our starting point is a classical algorithm of Michael Karr for discovering affine invariants. We proceed to mention a large number of variations and generalisations of this work to the case of polyhedral and algebraic invariants. In the main body of the talk we describe two recent procedures to compute the strongest algebraic invariant of an affine program and to synthesise semi-algebraic invariants for proving non-termination of linear loops .
This talk is based on joint work with Shaull Almagor, Dmitry Chistikov, Ehud Hrushovski, Amaury Pouly, and Joël Ouaknine.