Events in 2015

Markus Rabe: Symbolic Approximation of the Bounded Reachability Probability in Large Markov Chains
16th Jan 2015 10:00:am
Venue: E3 Room 2.22Symbolic Approximation of the Bounded Reachability Probability in Large Markov Chains Abstract: We present a novel technique to analyze the bounded reachability probability problem for large Markov chains. The essential idea is to incrementally search for sets of paths that lead to the goal region and to choose the sets in a way that...

Presentation of Martin Zimmermann and Felix Klein
22nd Jan 2015 2:00:pm
Venue:Speaker: Martin Zimmermann, Universität des Saarlandes Title: The Complexity of Counting Models of Lineartime Temporal Logic Abstract: We determine the complexity of counting models of bounded size of specifications expressed in Lineartime Temporal Logic. Counting word models is #Pcomplete, if the bound is given in unary, and as hard as counting accepting runs of nondeterministic...

Presentation Srivathsan Baluguru
2nd Feb 2015 4:00:pm
Venue: Room 9220Fast detection of cycles in timed automata Abstract: We will present an algorithm to detect if a cycle in a timed automaton can be iterated infinitely often. Existing solutions in tools have a complexity which is exponential in the number of clocks. Our method is polynomial. This method can be incorporated in algorithms for verifying...

Gedenkkolloquium zu Ehren von Prof. Berthold Vöcking
5th Feb 2015 12:00:pm
Venue:Die Fachgruppe Informatik gedenkt mit einem zweitägigen Kolloquium am 5. und 6. Februar 2015 ihrem leider viel zu früh verstorbenen Freund und Kollegen Berthold Vöcking und lädt dazu herzlich ein. Am Donnerstag ab 12 Uhr beginnt das Kolloquium mit einem Empfang vor dem AH 5. Ab ca. 13 Uhr beginnen die Vorträge seiner Freunde, Kollegen...

Young Researchers Conference
24th Feb 2015 7:00:pm
Venue:19:00 – 21:30 Welcome (with drinks and snacks) at “SuperC”, RWTH Aachen (6th Floor)

Young Researchers Conference
25th Feb 2015 9:00:am
Venue:9:00 – 9:15 Welcome 9:15 – 10:15 Moshe Vardi: The Rise and fall of Linear Temporal Logic Coffee Break 10:30 – 11:30 Shiguang Feng : PathChecking for MTL and TPTL over Data Words Claudia Carapelle : Satisfiability of ECTL* with constraints Sascha Wunderlich : Weight Monitoring with Linear Temporal Logic Normann Decker : On an Extension of Freeze LTL...

Young Researchers Conference
26th Feb 2015 9:00:pm
Venue:9:00 – 10:00 JeanFrancois Raskin: Variations on the stochastic shortest path problem Coffee Break 10:20 – 11:20 Vitaly Perevoshchikov : Decomposition of Weighted Timed Automata Parvaneh Babari : A Nivat Theorem for Weighted Picture Automata and Weighted MSO Logics Mohamed Abdelaal : Fuzzy Compression Reﬁnement via Curvature Tracking Saifullah Khan : Trafﬁc Data Dissemination in Realistic Urban VANETs Environment Andreas...

Young Researchers Conference
27th Feb 2015 9:00:am
Venue:9:00 – 10:00 Eric Bodden: SPLlift: statically analyzing software product lines in minutes instead of years Coffee Break 10:20 – 11:20 Bogdan Mihaila : Synthesizing Predicates from Abstract Domain Losses Suvam Mukherjee : Efficient Shape Analysis of Multithreaded Programs Mitra Tabaei Befrouei : Abstraction and Mining of Traces to Explain Concurrency Bugs Christian Müller : An Analysis of Universal Information...

Vortrag: Die 2 Seiten der Gläsernen Decke
3rd Mar 2015 5:00:pm
Venue:„Die 2 Seiten der Gläsernen Decke“, gehalten von Marion Knaths am 03.03 um 17h im SuperC, Generali Saal – Templergraben 55, 6. Etage Frauen in Spitzenpositionen sind immer noch eine Ausnahme. Oftmals wird die berühmte „Gläserne Decke“ als Ursache dafür zitiert. Oben in der Regel die machthabenden Männer, unten in der Regel die aufstrebenden Frauen....

Kinoabend: The Imitation Game
4th Mar 2015 6:00:pm
Venue:Wer hat Lust auf Kino? Alle sind herzlich eingeladen mitzukommen! Wir – das ist eine Initiative aus REGINA e.V. und der GIRegionalgruppe Aachen (RIA) – haben einen Saal im ApolloKino reserviert und gezeigt wird: The Imitation Game Am 4. März 2015 um 18 Uhr Im Apollo Kino&Bar, Pontstraße 141149, 52062 Aachen Der Film von Morten Tyldum...

Presentation Arend Rensink
9th Mar 2015 3:30:pm
Venue: Room 4017 , Seminarraum i1IfNextAlsoElse: Controlling Graph Transformation Abstract: Graph transformation is a declarative, rulebased formalism. However, when using it in practice, it is convenient to schedule rules explicitly, and not just rely on their own application conditions, even though such scheduling adds an imperative flavour. This can be catered for by adding a layer of *control* on top...

Seminar: Professor Chris Myers, University of Utah, USA
17th Mar 2015 2:00:pm
Venue: Room 4017 , Seminarraum i1An Integrated Verification Architecture Abstract: Research in formal verification is hampered by a lack of an integrated verification architecture. Each verification tool in development typically uses its own language for models and properties. This fact means that when a designer wants to verify their system using multiple verification tools, it often requires a timeconsuming and...

Presentation: Prof. Sriram Sankaranarayanan
24th Mar 2015 11:00:am
Venue: Room 9222, E3Switched Region Stabilization of Polynomial Dynamical Systems Abstract: We consider the problem of automatically synthesizing region stabilizing controllers for polynomial dynamical systems. The goal of our synthesis is to produce switching controllers that can switch between finitely many modes to ensure that the resulting closed loop dynamics are guaranteed to reach a given small target...

Presentation: Prof. Luca Bortolussie (Trieste, Italy)
25th Mar 2015 2:00:pm
Venue: Room 5052Machine Learning meets Formal Verification Abstract: We will discuss novel applications of stateoftheart Machine Learning statistical tools to deal with uncertainty in Continuous Time Markov Chains, combining them with classic tools from formal methods, mainly Model Checking. Uncertain CTMC are Markov Chains whose rates depend on some fixed parameter, whose precise value is unknown, but...

Presentation: Roberta Lanciani
25th Mar 2015 4:00:pm
Venue:Stochastic Approximations and Verifications In this talk, we discuss the use of stochastic approximations to validate properties of Markov population models. This type of Markovian models are used to describe the evolution of large systems of interacting entities, and their verification, using standard stochastic model checking techniques, is ampered by the large number of possible...

Presentation: Nils Jansen
26th Mar 2015 10:00:am
Venue: Room 9222, E3Counterexamples in Probabilistic Verification The topic of this thesis is roughly to be classified into the formal verification of probabilistic systems. In particular, the generation of counterexamples for discretetime Markov Models is investigated. A counterexample for discretetime Markov Chains (DTMCs) is classically defined as a (finite) set of paths. In this work, this set of...

Prof. Lijun Zhang: Polynomial Quantitative Loop Invariants by Lagrange Interpolation
22nd Apr 2015 10:00:am
Venue:Polynomial Quantitative Loop Invariants by Lagrange Interpolation Abstract: We apply multivariate Lagrange interpolation to synthesizing polynomial quantitative loop invariants for probabilistic programs. Lagrange interpolation allows to find better constraints for unknown loop invariants. Random sampling furthermore generates constraints to pin point quantitative invariants. We evaluate our technique by several case studies with polynomial quantitative...

Deni Raco: Umsetzung der formalen Entwicklungsmethodik FOCUS in dem Theorembeweiser Isabelle zur Verifikation verteilter Systeme
23rd Apr 2015 11:14:am
Venue: 
AutoMathA 2015
6th May 2015
Venue:Jewels of Automata: from Mathematics to Applications Leipzig, May 69, 2015 The conference AutoMathA 2015 will survey a wide picture of research in automata theory and related mathematical fields. It will consist of 26 invited lectures which will describe significant progress over the past years, and will be a meeting point for both young and...

Simon Lessenich: Counting Logics and Games with Counters
13th May 2015 2:00:pm
Venue: Raum 9U09Referent: Dipl.Inform. Simon Lessenich Titel: Counting Logics and Games with Counters Abstract: In verification and synthesis, properties or models of interest are often quantitative, and many quantitative aspects involve counting. For example, one might be interested in the amount of memory required by a system, how many simultaneous requests a system has to process along...

Presentation Christian Meirich
20th May 2015 10:00:am
Venue: Room 5052 
Presentation: Christian Meirich
20th May 2015 10:15:am
Venue: Room 5052Optimization of Railwaynetworks The background of this talk is the motivation to optimize the capacitive load in the field of railway operation research. Especially there are approaches of the strategic network planning in the field of the (German) Federal Transport Infrastructure Plan. A plan like this is a comprehensive compilation of the German government for...

Abschlussveranstaltung Graduiertenkolleg AlgoSyn
17th Jun 2015
Venue: Room 9222, E3Abschlussveranstaltung Graduiertenkolleg AlgoSyn 10.00 Begrüßung 10.15 Präsentation Rückblick auf 9 Jahre AlgoSyn 11.00 Vortrag Sascha Geulen: Learningbased Control Strategies for Hybrid Electric Vehicles 12.00 Vortrag Johanna Nellen: simulation results of learningbased control strategies 13.00 Mittagspause 13.30 Koordination der Abschlussarbeiten und Einteilung der Untergruppen 14.15 Das GKintere Projekt „Scientific Life“ 14.45 Präsentation „Das Modell Graduiertenkolleg als...

Presentation: Rupak Majumdar
19th Jun 2015 3:00:pm
Venue: Room 9222, E3Algorithmic Formal Methods in Continuous Control Abstract: Algorithmic formal methods such as model checking and reactive synthesis were originally developed in the context of discrete systems such as hardware circuits and software. Over the last few years, these techniques have played an increasingly important role in the development of high assurance cyberphysical systems, in which...

Dr. Jan Oliver Ringert, Tel Aviv University, Israel:On Challenges in Reactive Synthesis for Software Engineers: Support for LTL Specification Patterns and a Case Study
8th Sep 2015 1:00:pm
Venue:Reactive synthesis is an automated procedure to obtain a correctbyconstruction reactive system from a given specification. Despite recent advancements on the theory and algorithms of reactive synthesis, many challenges remain in bringing reactive synthesis technologies to the hands of software engineers. GR(1) is a wellknown fragment of linear temporal logic introduced by Piterman et al....

Friedrich Gretz: Semantics and Loop Invariant Synthesis for Probabilistic Programs
25th Sep 2015 10:00:am
Venue: Room 9222, E3Referent: Dipl.Inform. Friedrich Gretz Titel: Semantics and Loop Invariant Synthesis for Probabilistic Programs Abstract: In this thesis we consider sequential probabilistic programs. Such programs are a means to model randomised algorithms in computer science. They facilitate the formal analysis of performance and correctness of algorithms or security aspects of protocols. We develop an operational semantics...
Events in 2014

Presentation Christian Meirich: Capacity of a railway network
15th Jan 2014 10:00:am
Venue: Room 5052On behalf of the German Railway Authority (Eisenbahnbundesamt) the suitability of a parameter “Capacity of railway infrastructure” in the target and performance agreement (LuFV) between the federal government and Deutsche Bahn AG has been analyzed. Today the capacity of railway lines can be calculated as well as the capacity of railway nodes by means of...

project “Mechanisms of scientific life”
5th Feb 2014 10:00:am
Venue: Room 5052Presentation of the first results an next steps

AlgoSynWorkshop together with GK PUMA (Programm Und ModellAnalyse, TU LMU)
26th Mar 2014 11:00:am
Venue:1st Day, 26.03.2014 10.30 Bus Departure (Entrance Parkinglot MiesvanderRoheStr.) 12:30 Lunch at BonnAachen International Center for Information Technology BIT; Dahlmannstraße 2; D53113 Bonn 14.00 Presentation by the representative H. Seidl und W. Thomas 14.30 15.45 Short presentations from Aachen (7 min) 15.45 – 16.00 Coffee Break 16.00 – 17.15 Short presentations from Munich (5 – 10 min)...

Benedikt Brütsch: Synthesizing Structured Reactive Programs: How Much Memory Do They Need?
23rd Apr 2014 10:00:am
Venue: Room 5052Benedikt Brütsch: “Synthesizing Structured Reactive Programs: How Much Memory Do They Need?”. Abstract: Existing approaches to the synthesis of controllers in reactive systems typically involve the construction of transition systems such as Mealy automata. In 2011, Madhusudan proposed structured programs over a finite set of Boolean variables as a more succinct formalism to represent the...

Visit the Railway Signalling Lab (ELVA) of the Institute of Transport Science
7th May 2014 10:00:am
Venue: Room 5052Visit the Railway Signalling Lab (ELVA) of the Institute of Transport Science. “Synthesizing Structured Reactive Programs: How Much Memory Do They Need?”. The meeting point will be in the foyer of the building of civil engineering (MiesvanderRoheStraße 1) at 10.15 a. m.. The AlgoSyn members starting from the Informatikzentrum will meet in front of room...

Benjamin Kaminski: Analyzing Expected Outcomes and AlmostSure Termination of Probabilistic Programs is Hard
28th May 2014 10:00:am
Venue: Room 5052We consider the hardness of computing expected outcomes and almostsure termination of probabilistic programs. We show that deciding almostsure termination and deciding whether the expected outcome of a program equals a given rational value is $\Pi^0_2$complete. Computing lower and upper bounds on the expected outcome is shown to be recursively enumerable and $\Sigma^0_2$complete, respectively.

Ibtissem Ben Makhlouf and Sarah Winter: Presentation of their work
2nd Jul 2014 10:00:am
Venue: Room 5052Ibtissem Ben Makhlouf: Reachability Analysis of Hybrid Systems Using Geometric Approximations Hybrid systems combine discrete events and continuous behaviors in the same framework. The discrete part is represented as transitions between locations, in which the continuous part is described as a differential equation and that generally in a confined invariant domain. The transitions are commonly...

Christina Jansen: Generating Inductive Predicates for Symbolic Execution of PointerManipulating Programs
16th Jul 2014
Venue: Room 5052Generating Inductive Predicates for Symbolic Execution of PointerManipulating Programs Separation Logic (SL) is an extension of Hoare Logic that supports reasoning about pointermanipulating programs. It employs inductivelydefined predicates for specifying the (dynamic) data structures maintained at runtime, such as lists or trees. To support symbolic execution, SL introduces abstraction rules that yield symbolic representations...

Oliver Göbel: Online Independent Set Beyond the WorstCase
6th Aug 2014 10:00:am
Venue: Room 5052Title: Online Independent Set Beyond the WorstCase Abstract: We investigate online algorithms for maximum independent set on graph classes with bounded inductive independence number $\rho$ like interval and disk graphs with applications to, e.g., task scheduling, spectrum allocation and admission control. In the online setting, nodes of an unknown graph arrive one by one over...

Johanna Nellen: A CEGAR Approach for the Reachability Analysis of Sequential Function Charts
22nd Oct 2014 10:00:am
Venue: Room 5052Johanna Nellen: A CEGAR Approach for the Reachability Analysis of Sequential Function Charts We address the safety analysis of chemical plants controlled by programmable logic controllers (PLCs). We consider sequential function charts (SFCs) for the programming of the PLCs, extended with the specification of the dynamic plant behavior. The resulting hybrid SFC models can be...

Presentation of Johanna Nellen
22nd Oct 2014 10:00:am
Venue: Room 5052 
Ufuk Topcu: CorrectByConstruction Control Synthesis for Autonomous Systems
31st Oct 2014 11:00:am
Venue:Ufuk Topcu: CorrectByConstruction Control Synthesis for Autonomous Systems How can we affordably build trustworthy autonomous, networked systems? Partly motivated by this question, I describe a shift from the traditional “design+verify” approach to “specify+synthesize” in modelbased engineering. I then discuss our recent results on automated synthesis of correctbyconstruction, hierarchical control protocols. These results account for hybrid...

AlgoSyn – FAllWorkshop in Schleiden
6th Nov 2014
Venue:Jährlicher AlgoSyninterner Workshop

Presentation of Christian Meirich
26th Nov 2014 10:00:am
Venue: Room 5052Präsentation von Christian Meirich: Erhöhung der Leistungsfähigkeit durch eine optimale Ausnutzung von Kapazitäten des Eisenbahnnetzen Im Eisenbahnwesen beschreibt die Kapazität die zulässige Anzahl an Zugfahrten auf einem Infrastrukturbereich innerhalb eines Zeitfensters. Derzeit ist es nicht möglich die einzelnen Kapazitäten von Eisenbahnstrecken mit denen der Eisenbahnknoten zu verrechnen, da unterschiedliche Rechenansätze hierfür verwendet werden. Somit lassen...

Promotionscafé
11th Dec 2014 3:30:pm
Venue: Room 9220Nach der Promotion in die Industrie Mehr Informationen: www.informatik.rwthaachen.de/Promotionscafe/

AlgoSynMeeting
7th Jan 2015 10:00:am
Venue: Room 5052Agenda Mechanism of Scientific Life FFM 2015 Election: New Steering Committee

Young Researchers Conference
25th Feb 2015
Venue:Young Researchers Conference “Frontiers of Formal Methods” Aachen, Germany February 25 – 27, 2015 organized by the DFG Research Training Groups AlgoSyn (Algorithmic Synthesis of Reactive and DiscreteContinuous Systems), Aachen PUMA (Program and Model Analysis), München QuantLA (Quantitative Logics and Automata), Dresden & Leipzig SCARE (System Correctness under Adverse Conditons), Oldenburg and the Austrian...
Events in 2013

Prof. Dr. Oliver Niggemann: Industrie 4.0 = Industrie 3.0 + Wissensverarbeitung?
24th Jul 2013 10:00:am
Venue: Room 5052Die zunehmende IKTIntegration und neue Anforderungen der Produktionstechnik erhöhen die Komplexität der Automation zunehmend und führen zur Überforderung der Menschen mit damit einhergehender sinkender Arbeitseffektivität. Um dieser Situation zu begegnen hat die Bundesregierung das Thema Industrie 4.0 ins Leben gerufen, welches als zusammenhängendes Forschungsfeld für die Automation aufgefasst werden kann. Durch den Einsatz von intelligenten...

Promotionscafé
23rd Sep 2013 3:00:pm
Venue:Frauen und Männer im Team – gleiche Chancen, gleiche Rechte?! Als Gast wird Frau Dr. Brands, die Gleichstellungsbeauftragte der RWTH Aachen, vortragen. Mehr Informationen: www.informatik.rwthaachen.de/Promotionscafe/

Presentation Deni Raco
24th Sep 2013 5:00:pm
Venue: Room 2202 
Presentation Gereon Kremer and Frédéric Reinhardt
2nd Oct 2013 10:00:am
Venue: 
annual AlgoSyn workshop
9th Oct 2013 11:00:am
Venue:From Wed 9th Oct (departure from Aachen around 11am) to Fri 11th Oct (departure from Dagstuhl in the afternoon) we shall have our annual AlgoSyn workshop, this time in Dagstuhl (instead of Rolduc). All AlgoSyns (doctoral students and professors) are requested to do their registration. Schedule

AlgoSyn Fall School
23rd Oct 2013
Venue:AlgoSyn Fall School (October 23rd – 25th, associated with SAGT 2013) Part A: Algorithmic Game Theory, Mechanism Design, Auction Systems Lectures on Computational Complexity in Games and Auctions by Constantinos Daskalakis (Massachusetts Institute of Technology) Lectures on Linear programming and Mechanism Design by Rakesh Vohra (Kellog School of Management) Part B: Games and...

Presentation Matteo Mio
13th Nov 2013 10:00:am
Venue: E3 Room 2.22First Talk: Game Semantics for Probabilistic muCalculi In this talk I will consider several probabilistic (or quantitative) variants of Kozen’s Modal muCalculus, designed for expressing properties of probabilisticnondeterministic transition systems. Two type of semantics can be defined for these logics: one denotational and one based on a novel kind of games which I call Tree...

Presentation Matteo Mio
14th Nov 2013 10:00:am
Venue: E3 Room 2.22Second Talk: Semantic Foundations of Quantitative (realvalued) Logics based on Functional Analysis Abstract: Several notions of bisimulation for Probabilistic Nondeterministic Transition Systems (PNTS) have been proposed in the literature. I will develop the theory of what I call “UpperExpectation bisimilarity” using standard results of linear algebra and functional analysis and provide strong mathematical foundations for...

Presentation Namit Chaturvedi: Languages of Infinite Traces and Deterministic Asynchronous Automata
27th Nov 2013
Venue:Abstract: In the theory of deterministic automata for languages of infinite words, a fundamental result relates the family of infinitary limits of regular languages and the family of omegalanguages recognized by deterministic Buechi automata. Furthermore, a theorem due to L. Landweber states that an omegaregular language is recognized by a deterministic Buechi automaton if and...

Presentation Friedrich Gretz
11th Dec 2013
Venue: 
Presentation Friedrich Gretz
12th Dec 2013
Venue: E3 room 2.22 (2nd floor)