- informatik-vortraege - lists.rwth-aachen.de

Einladung: Informatik Oberseminar Sebastian Junges
by Junges, Sebastian 15 Jan '20

15 Jan '20

+********************************************************************** * * * Einladung * * * * Informatik-Oberseminar * * * +********************************************************************** Zeit: Donnerstag, 13. Februar 2019, 13.00 Uhr Ort: Informatikzentrum, E3, Raum 9222 Referent: Sebastian Junges, M.Sc. Lehrstuhl für Informatik 2 (Software Modeling and Verification) Thema: Parameter Synthesis in Markov Models Abstract: Markov models comprise states with probabilistic transitions. The analysis of these models is ubiquitous and studied in, among others, reliability engineering, artificial intelligence, systems biology, and formal methods. Naturally, their analysis crucially depends on the transition probabilities. Often, these probabilities are approximations based on data or reflect configurable parts of a modelled system. To represent the uncertainty about the probabilities, we study parametric Markov models, in which the probabilities are symbolic expressions rather than concrete values. More precisely, we consider parametric Markov decision processes (pMDPs) and parametric Markov chains (pMCs) as special case. Substitution of the parameters yields classical, parameter-free Markov decision processes (MDPs) and Markov chains (MCs). A pMDP thus induces uncountably many MDPs. Each MDP may satisfy reachability and reward properties, such as "the maximal probability that the system reaches an `offline' state is less than 0.01%", or "the maximal expected energy consumption is less than 20 kWh." Lifting these properties to pMDPs yields fundamental problems asking: - "Is there an induced MDP satisfying the property?" (feasibility), its dual - "Do all induced MDPs satisfy the property?" (validity), and advanced problems such as "What is a concise representation for all induced MCs satisfying the property?" We study these problems on a conceptual level, and design and implement both improved and novel algorithms. On the conceptual side, a thorough discussion of the feasibility problem yields new results, such as: (1) that answering various variants of the feasibility problem is — in terms of complexity — as hard as finding roots of a multivariate polynomial, and (2) that these problems are tightly connected to the analysis of memoryless strategies in partially observable MDPs, a famous model in artificial intelligence. Additionally, we introduce family MCs (fMCs), a subclass of pMCs with finitely many induced MCs. Among others, fMCs define fundamental problems underlying the quantitative analysis of software product lines and sketching of probabilistic programs. On the algorithmic side, (1) we present and analyse improved but previously known approaches, and combine them to meet practical needs. Their analysis inspired (2) three new and orthogonal approaches, utilising advances in convex optimisation, as well as adapting prominent ideas such as inductive synthesis and abstraction-refinement to the particular setting. All methods efficiently exploit advances in the off-the-shelf analysis of MDPs. On the empirical side, the new methods improve the state-of-the-art considerably, handling hundreds of parameters and millions of states. All the approaches we present have been implemented in open-source tools. Es laden ein: die Dozentinnen und Dozenten der Informatik

1 0

Vortrag Dr. Markus Freitag (heute)
by Christian Herold 14 Jan '20

14 Jan '20

Sehr geehrte Damen und Herren, wir möchten Sie freundlich auf den Vortrag (s.u.) von Herr Dr. Markus Freitag heute Nachmittag um 14:30 hinweisen. Bitte entschuldigen Sie die kurzfristige Ankündigung. Mit freundlichen Grüßen, Christian Herold *********************************************************************** * * * Einladung zum Gastvortrag * * * ************************************************************************ Zeit: Dienstag, 14. Januar 2020, 14:30 Ort: Ahornstraße 55, E2, Raum 5056 Referent: Dr. Markus Freitag Titel: (Some) Research Happening at Google Translate Abstract: Machine Translation is one of the most appealing research topics in Natural Language Processing and Machine Learning. In this talk, you will be given an overview of some of the current research efforts happening at Google Translate. We will start with a project with the end-goal of training a single model to translate between all languages supported by Google Translate. Neural models can be trained to perform several tasks simultaneously as exemplified by multilingual NMT using a single model to translate between multiple languages. Apart from reducing operational costs, multilingual models improve performance on low and zero-resource language pairs due to joint training. We attempt to study multilingual neural machine translation, using a massive open-domain dataset containing over 25 billion parallel sentences in 103 languages. In the second half of the talk, we focus on translationese, a term that refers to artifacts present in text that was translated into a given language that distinguish it from text originally written in that language. These artifacts include lexical and word order choices that are influenced by the source language as well as the use of more explicit and simpler constructions. Machine translation has an undesirable propensity to produce translationese artifacts, which can lead to higher BLEU scores while being liked less by human raters. First, we train an Automatic Post Editing (APE) model that convert the translationese output into a more natural text. We use this model as a tool to reveal systematic problems with reference translations. Second, we model translationese and original (i.e. natural) text as separate languages in a multilingual model, and pose the question: can we perform zero-shot translation between original source text and original target text? To sum up, we will discuss why a loss in BLEU score does not always mean lower translation quality. -- Christian Herold Faculty of Mathematics, Computer Science and Natural Sciences HLTPR - Human Language Technology and Pattern Recognition RWTH Aachen University Ahornstraße 55 D-52074 Aachen Tel: +49 241 80 21613 Fax: +49 241 80 22219 herold(a)i6.informatik.rwth-aachen.de www.hltpr.rwth-aachen.de

1 0

Erinnerung: Informatik-Kolloquium Michael Schaub (08.01.2020 **morgen**, 14:00)
by Joost-Pieter Katoen 07 Jan '20

07 Jan '20

*********************************************************************** * * * Einladung * * * Informatik-Kolloquium * * *********************************************************************** Zeit: Mittwoch, 8. Januar 2020, 14:00 Uhr Ort: Raum 9222, Gebäude E3, Informatikzentrum Referent: Michael Schaub University of Oxford, UK and MIT, USA Thema: Data Science for Networks Abstract: Networks have become a widely adopted model for a range of systems, cutting across Science and Engineering. However, our theoretical understanding of many fundamental phenomena that arise in complex networks and networked systems is still limited. My vision is to develop a data science for networks and dynamical systems that will contribute to addressing this challenge, by combining data-driven and model-based approaches, using the language of graphs and networks. In this talk, we will give a brief overview of such a Data Science for Networks. We first discuss how networks appear naturally within models in different research domains and illustrate the underlying scientific questions via examples drawn from applications. We then examine in some detail the problem of feature learning from graphs with unobserved edges, in which we aim to learn certain aspects of a graph solely from dynamical observations on its nodes, without knowledge of the edge-set of the graph. We conclude with a brief outlook on future challenges and open problems. Es laden ein: die Dozentinnen und Dozenten der Informatik

1 0

Einladung: Informatik-Kolloquium Michael Schaub (08.01.2020, 14:00)
by Thomas Noll 13 Dec '19

13 Dec '19

*********************************************************************** * * * Einladung * * * Informatik-Kolloquium * * *********************************************************************** Zeit: Mittwoch, 8. Januar 2020, 14:00 Uhr Ort: Raum 9222, Gebäude E3, Informatikzentrum Referent: Michael Schaub University of Oxford, UK and MIT, USA Thema: Data Science for Networks Abstract: Networks have become a widely adopted model for a range of systems, cutting across Science and Engineering. However, our theoretical understanding of many fundamental phenomena that arise in complex networks and networked systems is still limited. My vision is to develop a data science for networks and dynamical systems that will contribute to addressing this challenge, by combining data-driven and model-based approaches, using the language of graphs and networks. In this talk, we will give a brief overview of such a Data Science for Networks. We first discuss how networks appear naturally within models in different research domains and illustrate the underlying scientific questions via examples drawn from applications. We then examine in some detail the problem of feature learning from graphs with unobserved edges, in which we aim to learn certain aspects of a graph solely from dynamical observations on its nodes, without knowledge of the edge-set of the graph. We conclude with a brief outlook on future challenges and open problems. Es laden ein: die Dozentinnen und Dozenten der Informatik

1 0

[Informatik-assistenten] Einladung: Informatik-Oberseminar Christoph Matheja
by Matheja, Christoph 11 Dec '19

11 Dec '19

+********************************************************************** * * * Einladung * * * * Informatik-Oberseminar * * * +********************************************************************** Zeit: Donnerstag, 9. Januar 2019, 14.00 Uhr Ort: Informatikzentrum, E3, Raum 9222 Referent: Christoph Matheja, M.Sc. Lehrstuhl für Informatik 2 (Software Modeling and Verification) Thema: Automated Reasoning and Randomization in Separation Logic Abstract: We study three aspects of program verification with separation logic: 1. Reasoning about quantitative properties, such as the probability of memory-safe termination, of randomized heap-manipulating programs. 2. Automated reasoning about the robustness of and entailments between formulas in the symbolic heap fragment of separation logic itself. 3. Automated reasoning about pointer programs by combining abstractions based on separation logic with the above techniques and model checking. Regarding the first item, we extend separation logic to reason about quantities, which evaluate to real numbers, instead of predicates, which evaluate to Boolean values. Based on the resulting quantitative separation logic, we develop a weakest precondition calculus à la Dijkstra for quantitative reasoning about randomized heap-manipulating programs. We show that this calculus is a sound and conservative extension of both separation logic and McIver and Morgan's weakest preexpectations which preserves virtually all properties of classical separation logic. We demonstrate its applicability by several case studies. Regarding the second item, we develop an algorithmic framework based on heap automata to compositionally check robustness properties, e.g., satisfiability or acyclicity, of symbolic heaps with inductive predicate definitions. We consider two approaches to discharge entailments for fragments of separation logic. In particular, this includes a pragmatic decision procedure with nondeterministic polynomial-time complexity for entailments between graphical symbolic heaps. Regarding the third item, we introduce Attestor - an automated verification tool for analyzing Java programs operating on dynamic data structures. The tool involves the generation of an abstract state space employing inductive predicate definitions in separation logic. Properties of individual states are defined by heap automata. LTL model checking is then applied to this state space, supporting the verification of both structural and functional correctness properties. Attestor is fully automated, procedure modular, and provides informative visual feedback including counterexamples for violated properties. Es laden ein: die Dozentinnen und Dozenten der Informatik

1 0

Einladung: Informatik-Oberseminar Daniel Neuen
by Daniel Neuen 03 Dec '19

03 Dec '19

+********************************************************************** * * * Einladung * * * * Informatik-Oberseminar * * * +********************************************************************** Zeit: Dienstag, 17. Dezember 2019, 12.00 Uhr Ort: Raum 5053.2 (großer Bit-Raum), Ahornstr. 55 Referent: Daniel Neuen M.Sc. Lehrstuhl Informatik 7 Thema: The Power of Algorithmic Approaches to the Graph Isomorphism Problem Abstract: The Graph Isomorphism Problem asks, given two input graphs, whether they are structurally the same, that is, whether there is a renaming of the vertices of the first graph in order to transform it to the second graph. By a recent breakthrough result of Babai, this problem can be solved in quasipolynomial time. However, despite extensive research efforts, it remains one of only few natural problems in NP that are neither known to be solvable in polynomial time nor known to be NP-complete. Over the past five decades several powerful techniques tackling the Graph Isomorphism Problem have been investigated uncovering various surprising links between different approaches. One of the most fundamental methods in the context of graph isomorphism testing is the Weisfeiler-Leman algorithm and the related paradigm of individualization and refinement. The latter is in particular employed in all practical tools tackling the isomorphism problem. We present new upper and lower bounds on the power of such purely combinatorial approaches. For example, this leads to the first exponential lower bounds on the worst-case complexity of all state-of-the-art isomorphism tools used in practice. A second crucial approach to the Graph Isomorphism Problem is based on group-theoretic techniques. In this direction, one of the algorithmic cornerstones is Luks polynomial time algorithm for testing isomorphism of bounded degree graphs. Adapting the novel group-theoretic methods by Babai developed for his quasipolynomial time isomorphism test we give an isomorphism test for graphs of maximum degree d with a running time bounded by a polynomial of degree polylogarithmic in d. As a consequence of this result we also obtain an improved fpt algorithm for testing isomorphism of graphs of bounded tree-width. Es laden ein: die Dozentinnen und Dozenten der Informatik

1 0

Einladung: Informatik-Oberseminar Matthias Hoelzel
by Matthias Hoelzel 27 Nov '19

27 Nov '19

+********************************************************************** * * * Einladung * * * * Informatik-Oberseminar * * * +********************************************************************** Zeit: Dienstag, 10. Dezember 2019, 12:00 Uhr Ort: Raum 9222, Gebäude E3, Ahornstr. 55 Referent: Matthias Hoelzel, M.Sc. LuF Math. Grundlagen der Informatik (Lehrgebiet Informatik 7) Thema: Fragments of Existential Second-Order Logic and Logics with Team Semantics Abstract: Team semantics is the modern basis for logics of dependence and independence whose formulae are not evaluated with single assignments, but with sets of such assignments. We study different fragments of logics with team semantics and existential second-order logic (ESO) such as the union-closed fragments of these logics, inclusion logic of restricted arity and logics with team semantics using weaker dependency concepts. We will present syntactic characterisations for the union-closed fragment of ESO and inclusion-exclusion logic. In order to obtain these characterisation results, novel inclusion-exclusion games are utilised as a bridge between semantical and syntactical fragments. These games are not only the model-checking games of ESO-sentences, but they can also be adapted for fragments of ESO and give rise to the definition of a single team-based atom that captures the union-closed fragment. Further we answer an open question due to Rönnholm regarding the connection between inclusion logic of restricted arity and a fragment of greatest fixed-point logic. Finally, we study variants of logics with dependency concepts, which can distinguish elements only up to a given equivalence. We juxtapose these new logics with equivalent fragments of ESO and analyse their expressive powers. Es laden ein: die Dozentinnen und Dozenten der Informatik

1 0

Einladung: Informatik Oberseminar Stefan Breuers
by Stefan Breuers 25 Nov '19

25 Nov '19

+********************************************************************** * * * Einladung * * * * Informatik-Oberseminar * * * +********************************************************************** Zeit: Montag, 02. Dezember 2019, 13:30 Uhr Ort: UMIC Research Centre, room 025, Mies-van-der-Rohe Strasse 15 Referent: Stefan Breuers, MSc., Lehrstuhl Informatik 8 (Computer Vision) Thema: Multi-object Tracking and Person Analysis from Mobile Robot Platforms Abstract: Detecting and tracking the persons in a scene has been an active field of research in the area of computer vision for decades. One of the main applications are mobile platforms, such as autonomous cars or service robots. In this talk, we are going to analyze different tracking approaches working on the image domain and have a deeper look at their errors, before we move forward to multi-object tracking from robots operating in the 3D world. We present our detection-tracking framework for systematic tracking evaluation and our insights on experiments in challenging environments. On top of that detection-tracking pipeline, we then run person analysis modules and look at the benefits of such an integration for an improved person-robot interaction. By utilizing the temporal information in the form of the person track identities, we enable a robust and efficient operation of expensive deep learning analysis methods on low-cost platforms. We conclude the talk by presenting an explorative work on the integration of person re-identification and multi-object tracking to overcome common compromises of classical tracking approaches, taking a step towards an end-to-end, image-to-track paradigm. Es laden ein: die Dozentinnen und Dozenten der Informatik

1 0

Einladung: Informatik Oberseminar Herr Marius Alwin Shekow
by Daniele Gloeckner 05 Nov '19

05 Nov '19

+********************************************************************** * * * Einladung * * * * Informatik-Oberseminar * * * +********************************************************************** Zeit: Freitag, 22.11.2019 um 13.00 Uhr Ort: Informatikzentrum, E3, Raum 5053.2 (ggü. AH 6) Referent: Marius Alwin Shekow, M. Sc. Informatik 5 Thema: Syncpal: A Simple and Iterative Reconciliation Algorithm for File Synchronization Abstract: To facilitate collaboration scenarios and data management across multiple devices, knowledge workers and individuals use file synchronizers. These tools replicate the devices local file system to a cloud storage. As Marius Shekow discusses in his doctoral viva, bugs in these file synchronizers force users to detect and fix synchronization errors manually, resulting in cost-intensive iterations in cooperation processes, which should be avoided. He presents the three core challenges in file synchronization which he examined in his doctoral thesis. You will learn about (a) heterogeneity of file systems and alternatives to handle their incompatibilities, (b) conflicting operations and options for conflict resolution, and (c) inferring a valid operation propagation order to optimize the synchronization efficiency and correctness. The speaker presents how these challenges are solved by example with the iterative Syncpal algorithm he developed in his thesis. The evaluation of its implementation shows that Syncpal improves the handling of file system heterogeneity and synchronizes changes from long offline periods correctly. Es laden ein: die Dozentinnen und Dozenten der Informatik

1 0

Terminänderung: Informatik-Oberseminar Florian Göbe
by Göbe, Florian 29 Oct '19

29 Oct '19

+********************************************************************** * * * Terminänderung * * * * Informatik-Oberseminar * * * +********************************************************************** ++++++++ * ALTE ZEIT: Donnerstag, 7. November 2019, 10:00 Uhr * NEUE ZEIT: Donnerstag, 7. November 2019, 9:30 Uhr ++++++++ Ort: Raum 2359|222 (9222), Informatikzentrum Erweiterungsbau 3 Referent: Florian Göbe, M.Sc.RWTH Informatik 11 – Embedded Software Thema: Überwachung von SPS-Programmen zur Laufzeit mittels ereignisdiskreter Systeme Kurzfassung: Bei der von Ramadge und Wonham eingeführten Supervisory Control Theory (SCT) handelt es sich um einen der verbreitetsten Ansätze für die Synthese von Lösungen im Bereich diskreter Steuerungen. In diesem Vortrag wird ein Ansatz vorgestellt, der das SCT-Rahmenwerk zur Überwachung existierender SPS-Steuerungsprogramme einsetzt. Letztere werden als vom Benutzer manuell implementiert angenommen, weswegen ihre Fehlerfreiheit in Bezug auf gewisse Anforderungen, beispielsweise an die funktionale Sicherheit, nicht in allen prinzipiell möglichen Situationen formal sichergestellt werden kann. Im vorgestellten Ansatz können diese Anforderungen als ereignisdiskrete Systeme formalisiert werden. Mittels einer modifizierten Form des Ramadge-Wonham-Rahmenwerkes wird aus diesen Modellen schließlich eine Überwachungsschicht generiert. Diese verhindert frühzeitig solche Aktionen der Steuerung, die schlussendlich zu einer Verletzung der Anforderungen führen könnten. Um eine möglichst große Bandbreite realistischer Anwendungsfälle abzudecken, wurden mehrere Anpassungen am ursprünglichen Rahmenwerk vorgenommen und Erweiterungen eingeführt, beispielsweise bedingte Transitionen, Vorlagen sowie Ereigniserzwingung zur Verhinderung unerwünschter Vorkommnisse. Das vorgestellte Konzept bildet den gesamten Prozess von der Erstellung der Anforderungsmodelle bis hin zu einer auf der Zielhardware direkt einsetzbaren Sicherheitsschicht ab und wurde in Form eines Werkzeugs prototypisch realisiert und evaluiert. Es laden ein: die Dozentinnen und Dozenten der Informatik

1 0