Termine Vorträge (Archiv)

Treffer 101 - 130 von 130 Ergebnissen

  • 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 Weisfeiler-Leman Dimension of Planar Graphs is at most 3
    Sandra Kiefer
    We prove that the Weisfeiler-Leman (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 WL-algorithm correctly tests isomorphism of graphs in a minor-closed class whenever it determines the orbits of the automorphism group of any vertex-/arc-colored 3-connected graph belonging to this class. Then we prove that, apart from several exceptional graphs (which have WL-dimension at most 2), the individualization of two correctly chosen vertices of a colored 3-connected planar graph followed by the 1-dimensional WL-algorithm produces the discrete vertex partition. This implies that the 3-dimensional WL-algorithm determines the orbits of a colored 3-connected planar graph. As a byproduct of the proof, we get a classification of the 3-connected 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 Computation
    Erkal Selman
  • 02.06.2017
    10:15 - 11:45
    ATI
    A Purely Relational Language for Choiceless Computation
    Erkal 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
    Graph decompositions using MSO transductions
    Marlin Frickenschmidt
  • 17.05.2017
    15:30 - 16:30
     
    Answering database queries under updates
    Nicole Schweikardt
    Query 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 k-ary relation obtained by evaluating a k-ary query Q on a relational database D. For Boolean queries, all three tasks boil down to (4) Answering: Decide if Q(D) is non-empty. Compared to the dynamic descriptive complexity framework introduced by Patnaik and Immerman (1997), which focuses on the expressive power of first-order 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
    Learning MSO-definable hypotheses on strings
    Martin Ritzert
  • 05.05.2017
    10:15 - 11:45
    ATI
    Tree Automata with Constraints for Infinite Trees
    Patrick Landwehr
  • 28.04.2017
    10:15 - 11:45
    ATI
    On the Expressiveness of Unfolding Proofs for Recursive Data Structures
    Christof Löding
    Unfolding 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 Urbana-Champaign), 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 quasi-polynomial time
    Katrin Dannert
    The problem of deciding parity games is known to be in NP and in co-NP 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 Multiteam-Semantik
    Richard Wilke
    Klassische Logiken werden mit der so genannten Tarski-Semantik 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 Team-Semantik. 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 Multiteam-Semantik, welche sich eben dieser Herausforderung stellen.
  • 03.03.2017
    10:15 - 11:15
     
    The First-Order Logic of Hyperproperties
    Martin Zimmermann
    We 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 first-order logic. Kamp's seminal theorem (in the formulation due to Gabbay et al.) states that linear-time temporal logic (LTL) is expressively equivalent to first-order logic over the natural numbers with order. We introduce first-order 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 First-Order Logic of Hyperproperties
    Martin Zimmermann
    We 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 first-order logic. Kamp's seminal theorem (in the formulation due to Gabbay et al.) states that linear-time temporal logic (LTL) is expressively equivalent to first-order logic over the natural numbers with order. We introduce first-order 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 GI
    Gaurav Rattan
    Using 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 Isomorphism
    Daniel Neuen
    The 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 k-dimensional Weisfeiler Leman is used for refinement instead of color refinement (i.e. 1-dimensional 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 Isomorphism
    Daniel Neuen
    The 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 k-dimensional Weisfeiler Leman is used for refinement instead of color refinement (i.e. 1-dimensional 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
    N-Memory Automata Over the Alphabet N
    Patrick Landwehr
    An automaton model for words over the alphabet of the natural numbers is presented - the so called N-memory automaton. We explain its close connection to MSO-logic and discuss its expressive power and closure properties. Additionally we show among other decidability results the solvability of the non-emptiness 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 First-Order 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 monomial-PC (a weaker variant of the Polynomial Calculus) which are guaranteed to produce polynomial-size proofs. It turns out that the power of these restricted proof systems can be described in terms of other well-known logics, namely we obtain equivalences with least fixed-point logic (LFP), existential least fixed-point logic (EFP) and fixed-point logic with counting (FPC).