
Termin
Titel

30.06.2017
10:15  11:45
ATI
Regular Separability of One Counter Automata
work by Wojciech Czerwiński and Sławomir Lasota

30.06.2017
10:15  11:45
ATI
Regular Separability of One Counter Automata
work by Wojciech Czerwiński and Sławomir Lasota

23.06.2017
10:15  11:45
ATI
The 4/3 Additive Spanner Exponent Is Tight
work by Amir Abboud and Greg Bodwin

16.06.2017
10:15  11:45
ATI
The WeisfeilerLeman Dimension of Planar Graphs is at most 3Sandra KieferWe prove that the WeisfeilerLeman (WL) dimension of the class of all finite planar graphs is at most 3. In particular, every finite planar graph is definable in fixed point logic with counting using at most 4 variables. The previously best known upper bounds for the dimension and number of variables were 14 and 15, respectively. First we show that, for dimension 3 and higher, the WLalgorithm correctly tests isomorphism of graphs in a minorclosed class whenever it determines the orbits of the automorphism group of any vertex/arccolored 3connected graph belonging to this class. Then we prove that, apart from several exceptional graphs (which have WLdimension at most 2), the individualization of two correctly chosen vertices of a colored 3connected planar graph followed by the 1dimensional WLalgorithm produces the discrete vertex partition. This implies that the 3dimensional WLalgorithm determines the orbits of a colored 3connected planar graph. As a byproduct of the proof, we get a classification of the 3connected planar graphs with fixing number 3. This is joint work with Ilia Ponomarenko and Pascal Schweitzer.

02.06.2017
10:15  11:45
ATI
A Purely Relational Language for Choiceless ComputationErkal Selman

02.06.2017
10:15  11:45
ATI
A Purely Relational Language for Choiceless ComputationErkal Selman

30.05.2017
10:30  11:30
The Connection Between Visibly Pushdown and Operator Precedence Languages
Mietze Tang
Bachelor thesis final talk

30.05.2017
10:30  11:30
The Connection Between Visibly Pushdown and Operator Precedence Languages
Mietze Tang
Bachelor thesis final talk

19.05.2017
10:15  11:45
ATI

17.05.2017
15:30  16:30
Answering database queries under updatesNicole SchweikardtQuery evaluation is one of the most fundamental tasks in databases, and a vast amount of literature is devoted to the complexity of this problem. This talk will focus on query evaluation in the “dynamic setting”, where the database may be updated by inserting or deleting tuples. In this setting, an evaluation algorithm receives a query Q and an initial database D and starts with a preprocessing phase that computes a suitable data structure to represent the result of evaluating Q on D. After every database update, the data structure is updated so that it represents the result of evaluating Q on the updated database. The data structure shall be designed in such a way that it quickly provides the query result, preferably in constant time (i.e., independent of the database size). We focus on the following flavours of query evaluation. (1) Testing: Decide whether a given tuple t is contained in Q(D). (2) Counting: Compute the number of tuples that belong to Q(D). (3) Enumeration: Enumerate Q(D) with a bounded delay between the output tuples. Here, as usual, Q(D) denotes the kary relation obtained by evaluating a kary query Q on a relational database D. For Boolean queries, all three tasks boil down to (4) Answering: Decide if Q(D) is nonempty. Compared to the dynamic descriptive complexity framework introduced by Patnaik and Immerman (1997), which focuses on the expressive power of firstorder logic on dynamic databases and has led to a rich body of literature, we are interested in the computational complexity of query evaluation. We say that a query evaluation algorithm is efficient if the update time is either constant or at most polylogarithmic in the size of the database. In this talk I want to give an overview of recent results in this area.

12.05.2017
10:15  11:45
ATI

05.05.2017
10:15  11:45
ATI

28.04.2017
10:15  11:45
ATI
On the Expressiveness of Unfolding Proofs for Recursive Data StructuresChristof LödingUnfolding proofs are a heuristic that is used for verifying properties of heap manipulating programs with recursively defined data structures (like lists or trees). The heuristic reduces the property to be verified to a finite set of quantifier formulas, which can be tested for satisfiability by an SMT solver. The quantifier formulas are basically obtained by instantiating (unfolding) the recursive definitions with concrete terms referring to heap elements. In this joint ongoing work with P. Madhusudan and Lucas Pena (University of Illinois UrbanaChampaign), we aim at understanding which properties can proven using this heuristic.

25.04.2017
10:30  11:30
Complexity of cardinality problems for automata on infinite words
Duc Thanh Tran
Bachelor thesis final talk

21.04.2017
11:45  12:45
Complexity of determinizing automata by pruning the transition relation
Philip Tse
Bachelor thesis final talk

29.03.2017
10:00  11:00
Complexity of the Graph Homomorphism Problem
Philipp Niemietz

29.03.2017
10:00  11:00
Complexity of the Graph Homomorphism Problem
Philipp Niemietz

24.03.2017
10:15  11:45
Parity games in quasipolynomial time
Katrin Dannert
The problem of deciding parity games is known to be in NP and in coNP but it is unknown, whether it is solvable in polynomial time. Recently it has been shown that the problem can be solved both in quasipolynomial time and in FPT with the number of colours as the parameter. In order to obtain these runtimes, space efficient winning statistics for a play are maintained by building up and combining "favourable" sequences whose lengths are powers of two. This yields an alternating polylogarithmic space algorithm, which can be translated both into a quasipolyno mial time algorithm and an FPT algorithm. Based on the paper Deciding Parity Games in Quasipolynomial Time by Calude, Jain, Khoussainov, Li and Stephan

20.03.2017
11:00  12:00
Properties of Limit Deterministic Büchi Automata
Max Ohn

20.03.2017
12:00  13:00
Uniformization of Rational Relations
Yordan Manolov

14.03.2017
11:00  12:00
Logiken mit MultiteamSemantik
Richard Wilke
Klassische Logiken werden mit der so genannten TarskiSemantik aus gewertet. Dabei gibt eine Zuweisung den vorkommenden Variablen einer Formel ihre Bedeutung. Dieses Konzept st ̈oßt an seine Grenzen sobald man Abh ̈angigkeiten zwischen den Variablen ausdru ̈cken m ̈ochte. Verschiedene Logiken sind entwickelt worden um derartige Aussagen treffen zu k ̈onnen. Das ju ̈ngste Konzept ist die TeamSemantik. Man betrachtet dort zu ei ner Formel eine Menge von Zuweisungen, die miteinander interagieren. So kann man beispielsweise die Aussage treffen, dass der Wert einer Variable y ausschließlich vom Wert der Variable x abh ̈angig ist. Ein Team kann als Datenbank betrachtet werden, wobei jede Zuweisung einen Eintrag repr ̈asentiert. In reellen Anwendungen kann es von großer Be deutung sein, wie oft ein gewisser Eintrag vorkommt. Wir betrachtet daher Logiken mit MultiteamSemantik, welche sich eben dieser Herausforderung stellen.

03.03.2017
10:15  11:15
The FirstOrder Logic of HyperpropertiesMartin ZimmermannWe investigate the logical foundations of hyperproperties. Hyperproperties generalize trace properties, which are sets of traces, to sets of sets of traces. The most prominent application of hyperproperties is information flow security: information flow policies characterize the secrecy and integrity of a system by comparing two or more execution traces, for example by comparing the observations made by an external observer on execution traces that result from different values of a secret variable. In this paper, we establish the first connection between temporal logics for hyperproperties and firstorder logic. Kamp's seminal theorem (in the formulation due to Gabbay et al.) states that lineartime temporal logic (LTL) is expressively equivalent to firstorder logic over the natural numbers with order. We introduce firstorder logic over sets of traces and prove that HyperLTL, the extension of LTL to hyperproperties, is strictly subsumed by this logic. We furthermore exhibit a fragment that is expressively equivalent to HyperLTL, thereby establishing Kamp's theorem for hyperproperties. Based on joint work with Bernd Finkbeiner (Saarland University).

03.03.2017
10:15  11:15
The FirstOrder Logic of HyperpropertiesMartin ZimmermannWe investigate the logical foundations of hyperproperties. Hyperproperties generalize trace properties, which are sets of traces, to sets of sets of traces. The most prominent application of hyperproperties is information flow security: information flow policies characterize the secrecy and integrity of a system by comparing two or more execution traces, for example by comparing the observations made by an external observer on execution traces that result from different values of a secret variable. In this paper, we establish the first connection between temporal logics for hyperproperties and firstorder logic. Kamp's seminal theorem (in the formulation due to Gabbay et al.) states that lineartime temporal logic (LTL) is expressively equivalent to firstorder logic over the natural numbers with order. We introduce firstorder logic over sets of traces and prove that HyperLTL, the extension of LTL to hyperproperties, is strictly subsumed by this logic. We furthermore exhibit a fragment that is expressively equivalent to HyperLTL, thereby establishing Kamp's theorem for hyperproperties. Based on joint work with Bernd Finkbeiner (Saarland University).

17.02.2017
10:15  11:15
Compact graphs and the LP approach to GIGaurav RattanUsing the LP formulation for GI, we describe the class of compact graphs, proposed by Tinhofer. Isomorphism testing for such graphs can be done efficiently, using the linear program for GI. The recognition problem for such graphs remains open. Towards a partial understanding of this class, we describe some connections of this class with Color Refinement and Individualization techniques.

03.02.2017
10:15  11:15
ATI
An exponential lower bound for Individualization/Refinement algorithms for Graph IsomorphismDaniel NeuenThe individualization and refinement paradigm provides a strong toolbox for testing isomorphism of two graphs and indeed, it provides the only methods for isomorphism testing which are also viable for practical uses. From the theoretical point of view, no meaningful lower bounds on the worst case complexity of these tools are known. In fact, it is an open question whether these simple methods might provide similar upper bounds than existing algorithms combining complex group theoretic and combinatorial tools. In this work we give a negative answer to this question and construct a family of graphs that provides an exponential lower bound for methods based on the individualization and refinement paradigm. Other than previous constructions like Miyazaki graphs, our construction is immune to changing the cell selector or invariants used within the algorithm. Furthermore, our graphs also provide exponential lower bounds in the case where kdimensional Weisfeiler Leman is used for refinement instead of color refinement (i.e. 1dimensional Weisfeiler Leman) and the arguments even work when the automorphism group is initially known to the algorithm. In particular, under some moderate assumptions, our lower bounds are independent from which heuristics are used for cell selection, node invariants and automorphism detection.

03.02.2017
10:15  11:15
ATI
An exponential lower bound for Individualization/Refinement algorithms for Graph IsomorphismDaniel NeuenThe individualization and refinement paradigm provides a strong toolbox for testing isomorphism of two graphs and indeed, it provides the only methods for isomorphism testing which are also viable for practical uses. From the theoretical point of view, no meaningful lower bounds on the worst case complexity of these tools are known. In fact, it is an open question whether these simple methods might provide similar upper bounds than existing algorithms combining complex group theoretic and combinatorial tools. In this work we give a negative answer to this question and construct a family of graphs that provides an exponential lower bound for methods based on the individualization and refinement paradigm. Other than previous constructions like Miyazaki graphs, our construction is immune to changing the cell selector or invariants used within the algorithm. Furthermore, our graphs also provide exponential lower bounds in the case where kdimensional Weisfeiler Leman is used for refinement instead of color refinement (i.e. 1dimensional Weisfeiler Leman) and the arguments even work when the automorphism group is initially known to the algorithm. In particular, under some moderate assumptions, our lower bounds are independent from which heuristics are used for cell selection, node invariants and automorphism detection.

27.01.2017
10:15  11:15
ATI
NMemory Automata Over the Alphabet NPatrick LandwehrAn automaton model for words over the alphabet of the natural numbers is presented  the so called Nmemory automaton. We explain its close connection to MSOlogic and discuss its expressive power and closure properties. Additionally we show among other decidability results the solvability of the nonemptiness problem.

20.01.2017
10:15  11:15
ATI
Ramanujan Graphs in Polynomial Time
Lars Beckers

13.01.2017
10:15  11:15
ATI
Differential Privacy
Andreas Klinger

13.01.2017
14:15  15:15
Extensions of FirstOrder Logic by Propositional Proof Systems
Benedikt Pago
Propositional proof systems such as Resolution or the Polynomial Calculus have been studied as approaches for solving computationally difficult problems, e.g. Graph Isomorphism. As this problem requires proofs of exponential size, this motivates the question of which problems have only polynomial proof complexity. We address this by analysing the expressive power of logics incorporating suitably restricted versions of Resolution and monomialPC (a weaker variant of the Polynomial Calculus) which are guaranteed to produce polynomialsize proofs. It turns out that the power of these restricted proof systems can be described in terms of other wellknown logics, namely we obtain equivalences with least fixedpoint logic (LFP), existential least fixedpoint logic (EFP) and fixedpoint logic with counting (FPC).