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.
|2020 Oct 27||13:00 - 16:00||Revisiting Synthesis for One-Counter Automata||Guillermo Alberto Perez
(University of Antwerp)
|2020 Nov 03||13:00 - 16:00||Organisation and review meeting||zoom: 84523500974|
|Open problem session|
|2020 Nov 10||15:00 - 18:00||Tower-hardness of the reachability problem for Vector Addition Systems||Wojciech Czerwinski
|2020 Nov 17||13:00 - 16:00||Determinization of Büchi Automata: Unifying the Approaches of Safra and Muller-Schupp||Anton Pirogov
|2020 Nov 24||15:00 - 18:00||A Logical Revolution||Moshe Y. Vardi
|2020 Dec 01||13:00 - 16:00||An Efficient Normalisation Procedure for Linear Temporal Logic||Salomon Sickert-Zehnter
(TU München and Hebrew University, Jerusalem)
|2020 Dec 08||13:00 - 16:00||Good Scientific Practice||Karin Quaas
|Good Scientific Practice||Karin Quaas
|2020 Dec 15||13:00 - 16:00||Separating Positive and Negative Data Examples in the Presence of an Ontology||Frank Wolter
(University of Liverpool)
|2021 Jan 14
|17:00 - 18:00||World Logic Day (Vienna) - Lecture by Georg Gottlob:
"On the future of logic in connection with artificial intelligence"
(University of Oxford, TU Vienna)
|Zoom and youtube links will be provided on this website
(registration encouraged, but not mandatory).
|2021 Jan 26||13:00 - 16:00||Explaining Non-Subsumption by Counterexample||Willi Hieke
|2021 Feb 02||13:00 - 16:00||Relation algebra, games, representations, constraints||Robin Hirsch||zoom: 81108206775|
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.
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)
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.
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.
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.
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.