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.

All seminars sessions can be accessed via the following zoom link: https://tu-dresden.zoom.us/j/81108206775. The passcodes will be sent around via email. 

The passcodes to the virtual meetings can also be inquired from Sandy Seifarth.

Abstracts

Guillermo Alberto Perez: Revisiting Synthesis for One-Counter Automata 

One-counter automata are obtained by extending classical finite-state automata with a counter whose value can range over non-negative integers and be tested for zero. The updates and tests applicable to the counter can further be made parametric by introducing a set of integer-valued variables called parameters. During this talk we will focus on parameter synthesis problems for such automata. That is, we ask whether there exists a valuation of the parameters such that all infinite runs of the automaton satisfy some omega-regular property. The problem has been shown to be encodable in a restricted one-alternation fragment of Presburger arithmetic with divisibility. We will see that said fragment, called EARPAD, is unfortunately undecidable. Fortunately, there is an alternative encoding of the problem into a decidable restriction of EARPAD. Finally, we will study an alternative solution going via alternating two-way automata. The latter gives us a polynomial-space algorithm for the special case of the problem where parameters can only be used in tests, and not updates, of the counter.

Wojciech Czerwinski: Tower-hardness of the reachability problem for Vector Addition Systems

I will give you some intuition behind the challenges one meets when trying to prove that reachability in Vector Addition Systems (aka Petri nets) is Tower-hard and how we managed to overcome them.

Anton Pirogov: Determinization of Büchi Automata: Unifying the Approaches of Safra and Muller-Schupp

Determinization of Büchi automata is a long-known difficult problem that is of practical interest for automata-based approaches to e.g. model checking and synthesis. After the seminal result of Safra, who developed the first asymptotically optimal construction from Büchi into Rabin automata, much work went into improving, simplifying, or avoiding Safra's construction. A different, less known determinization construction was proposed by Muller and Schupp. The two types of constructions share some similarities, but their precise relationship was still unclear. This talk will first shed some light on the relationship of these constructions and then present a construction from nondeterministic Büchi to deterministic parity automata that subsumes both constructions as just two special cases of a more general determinization procedure. (Joint work with Christof Löding)

Moshe Y. Vardi: A logical revolution

Mathematical logic was developed in an effort to provide formal foundations for mathematics. In this quest, which ultimately failed, logic begat computer science, yielding both computers and theoretical computer science. But then logic turned out to be a disappointment as foundations for computer science, as almost all decision problems in logic are either unsolvable or intractable.  Starting from the mid 1970s, however, there has been a quiet revolution in logic in computer science, and problems that are theoretically undecidable or intractable were shown to be quite feasible in practice. This talk describes the rise, fall, and rise of logic in computer science, describing several modern applications of logic to computing, include databases, hardware design, and software engineering.

Frank Wolter: Separating Positive and Negative Data Examples in the Presence of an Ontology

Finding a logical formula that separates positive and negative examples given in the form of labeled data items is fundamental in applications such as concept learning,  reverse engineering of database queries, and generating referring expressions.
In this talk, I will discuss recent results on the existence of a separating formula for incomplete data in the presence of an ontology. Both for the ontology language and the separation language, we concentrate on fragments of first-order logic, including description logics. We consider several forms of separability that differ in the treatment of negative examples and in whether or not they admit the use of additional helper symbols to achieve separation. We characterize separability in a model-theoretic way, compare the separating power of the different languages, and determine the computational complexity of separability as a decision problem.
We also point out very close links to the existence problem for least common subsumers, most specific concepts, and Craig interpolants.

Willi Hieke: Explaining Non-Subsumption by Counterexample 

The task is to provide good explanations of reasoning results for users of a Description Logic (DL) system. In particular, we want to explain non-entailments of a DL knowledge base by means of counterexamples for the DL EL. In our setting, we are given a knowledge base, a subsumption relation that does not follow from the knowledge base and a model of the knowledge base that does not satisfy the subsumption relation is question. We provide three different notions of what a good counterexample is by defining the relevant parts of the given model, and also show how to obtain good counterexamples by model transformation using canonical models of knowledge bases.

Robin Hirsch: Relation algebra, games, representations, constraints

An introduction to games for solving constraints.  I will mainly focus on binary constraints and the binary constraint satisfaction problem. We devise games to test consistency of binary constraints. We also introduce algebras for binary constraints — Relation Algebra — and use the game to test the representability of an algebra, as a concrete algebra of binary relations.  These games can be used to find a recursively enumerable axiomatisation of the representation class, and can also be used to prove that a finite axiomatisation is not possible.