BEGIN:VCALENDAR
VERSION:2.0
PRODID:-////NONSGML Events //EN
CALSCALE:GREGORIAN
X-WR-CALNAME: - Events
X-ORIGINAL-URL:http://www.algosyn.rwth-aachen.de/events/event/
X-WR-CALDESC: - Events
BEGIN:VEVENT
UID:20130805T0743Z-1375688591.6484-EO-333-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20130724T164116Z
LAST-MODIFIED:20130731T143230Z
DTSTART:20130724T080000Z
DTEND:20130724T090000Z
SUMMARY: Prof. Dr. Oliver Niggemann: Industrie 4.0 = Industrie 3.0 + Wissen
 sverarbeitung?
DESCRIPTION: Die zunehmende IKT-Integration und neue Anforderungen der Prod
 uktionstechnik erhöhen die Komplexität der Automation zunehmend und führen 
 zur Überforderung der Menschen mit damit einhergehender sinkender Arbeitsef
 fektivität. Um dieser Situation zu begegnen hat die Bundesregierung das The
 ma Industrie 4.0 ins Leben gerufen\, &#8230\; <a href="http://www.algosyn.r
 wth-aachen.de/events/event/industrie-4-0-industrie-3-0-wissensverarbeitung/
 ">Continue reading <span class="meta-nav">&#8594\;</span></a>
X-ALT-DESC;FMTTYPE=text/html: Die zunehmende IKT-Integration und neue Anfor
 derungen der Produktionstechnik erhöhen die Komplexität der Automation zune
 hmend und führen zur Überforderung der Menschen mit damit einhergehender si
 nkender Arbeitseffektivität. Um dieser Situation zu begegnen hat die Bundes
 regierung das Thema Industrie 4.0 ins Leben gerufen\, welches als zusammenh
 ängendes Forschungsfeld für die Automation aufgefasst werden kann. Durch de
 n Einsatz von intelligenten Assistenzsystemen soll der Mensch bei fortschre
 itender Systemkomplexität unterstützt und nicht weiter von wertschöpfenden 
 Tätigkeiten abgehalten werden. Am Beispiel ausgewählter Projekte des Spitze
 nclusters "it's OWL" und der Lemgoer Modellfabrik werden typische Assistenz
 funktionen für die Selbstkonfiguration\, Selbstdiagnose und Selbstoptimieru
 ng in der Automation vorgestellt sowie deren notwendige Fähigkeiten analysi
 ert. Wichtige\, in diesem Feld vorhandene\, offene Forschungsfragen werden 
 adressiert und erste Ergebnisse präsentiert.
 
 The slides of the talk ar
 e available <a href="https://dl.dropboxusercontent.com/u/14090531/VortragNi
 ggemann.pdf" rel="nofollow">here</a>.
LOCATION:Room 5052
GEO:50.778320;6.060860
ORGANIZER:Ulrich Loup
END:VEVENT
BEGIN:VEVENT
UID:20130912T1334Z-1378992851.8863-EO-634-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20130912T102649Z
LAST-MODIFIED:20130913T102352Z
DTSTART:20130923T130000Z
DTEND:20130923T143000Z
SUMMARY: Promotionscafé
DESCRIPTION: Frauen und Männer im Team &#8211\; gleiche Chancen\, gleiche R
 echte?! Als Gast wird Frau Dr. Brands\, die Gleichstellungsbeauftragte der 
 RWTH Aachen\, vortragen. Mehr Informationen:  www.informatik.rwth-aachen.de
 /Promotionscafe/
X-ALT-DESC;FMTTYPE=text/html: Frauen und Männer im Team - gleiche Chancen\,
  gleiche Rechte?!
 
 <a href="http://www.algosyn.rwth-aachen.de/wp-conten
 t/uploads/2013/09/Promotionscafe_23_09_2013.jpg"><img class="alignnone size
 -medium wp-image-636" alt="Promotionscafe_23_09_2013" src="http://www.algos
 yn.rwth-aachen.de/wp-content/uploads/2013/09/Promotionscafe_23_09_2013-300x
 212.jpg" width="300" height="212" /></a>
 
 Als Gast wird Frau Dr. Brands
 \, die
 Gleichstellungsbeauftragte der RWTH Aachen\, vortragen.
 Mehr Inf
 ormationen:  www.informatik.rwth-aachen.de/Promotionscafe/
ORGANIZER:Helen Bolke-Hermanns
END:VEVENT
BEGIN:VEVENT
UID:20130913T1603Z-1379088206.3191-EO-641-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20130913T102700Z
LAST-MODIFIED:20130920T071156Z
DTSTART:20130924T150000Z
DTEND:20130924T160000Z
SUMMARY: Presentation Deni Raco
X-ALT-DESC;FMTTYPE=text/html: 
LOCATION:Room 2202
GEO:50.778320;6.060860
ORGANIZER:Helen Bolke-Hermanns
END:VEVENT
BEGIN:VEVENT
UID:20130913T1603Z-1379088206.3215-EO-642-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20130913T102852Z
LAST-MODIFIED:20130913T102852Z
DTSTART:20131002T080000Z
DTEND:20131002T093000Z
SUMMARY: Presentation Gereon Kremer and Frédéric Reinhardt
X-ALT-DESC;FMTTYPE=text/html: 
ORGANIZER:Helen Bolke-Hermanns
END:VEVENT
BEGIN:VEVENT
UID:20130924T0912Z-1380013951.8088-EO-680-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20130924T090754Z
LAST-MODIFIED:20131008T104544Z
DTSTART:20131009T090000Z
DTEND:20131011T110000Z
SUMMARY: annual AlgoSyn workshop
DESCRIPTION: From Wed 9th Oct (departure from Aachen around 11am) to Fri 11
 th 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 &#8230\; <a href="http://www.algosyn
 .rwth-aachen.de/events/event/annual-algosyn-workshop-2/">Continue reading <
 span class="meta-nav">&#8594\;</span></a>
X-ALT-DESC;FMTTYPE=text/html: From Wed 9th Oct (departure from Aachen aroun
 d 11am) to
 Fri 11th Oct (departure from Dagstuhl in the afternoon)
 we s
 hall have our annual AlgoSyn workshop\, this time in Dagstuhl
 (instead of
  Rolduc).
 
 All AlgoSyns (doctoral students and professors) are requeste
 d
 to do their registration.
 
 <a href="http://www.algosyn.rwth-aachen.
 de/?page_id=712">Schedule</a>
 
ORGANIZER:algoadmin
END:VEVENT
BEGIN:VEVENT
UID:20130924T0912Z-1380013951.8115-EO-682-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20130924T091054Z
LAST-MODIFIED:20131004T103750Z
DTSTART;VALUE=DATE:20131023
DTEND;VALUE=DATE:20131026
SUMMARY: AlgoSyn Fall School
DESCRIPTION: AlgoSyn Fall School (October 23rd &#8211\; 25th\, associated w
 ith SAGT 2013) &#160\; Part A: Algorithmic Game Theory\, Mechanism Design\,
  Auction Systems Lectures on Computational Complexity in Games and Auctions
  by Constantinos Daskalakis (Massachusetts Institute of Technology) Lecture
 s on Linear programming and &#8230\; <a href="http://www.algosyn.rwth-aache
 n.de/events/event/algosyn-fall-school-2/">Continue reading <span class="met
 a-nav">&#8594\;</span></a>
X-ALT-DESC;FMTTYPE=text/html: <h1><a title="AlgoSyn Fall School" href="http
 ://algo.rwth-aachen.de/fallschool/">AlgoSyn Fall School</a>
 <small>(Octob
 er 23rd - 25th\, associated with <b><a href="http://algo.rwth-aachen.de/sag
 t2013/" target="_new3">SAGT 2013</a></b>)</small></h1>
 &nbsp\;
 <h2>Part
  A: Algorithmic Game Theory\, Mechanism Design\, Auction Systems</h2>
 <ul
 >
 	<li>Lectures on Computational Complexity in Games and Auctions
 by <a
  href="http://people.csail.mit.edu/costis/" target="_new3">Constantinos Das
 kalakis (Massachusetts Institute of Technology)</a></li>
 </ul>
 <ul>
 	
 <li>Lectures on Linear programming and Mechanism Design
 by <a href="http:
 //www.kellogg.northwestern.edu/faculty/vohra/htm/" target="_new3">Rakesh Vo
 hra (Kellog School of Management)</a></li>
 </ul>
 &nbsp\;
 
 &nbsp\;

  <h2>Part B: Games and Software Synthesis\, Automata and Learning\, Softwar
 e Verification</h2>
 <ul>
 	<li>Lectures on Automata and Learning Based M
 ethods in Software Verification
 by <a href="http://cs.illinois.edu/people
 /faculty/madhusudan-parthasarathy/" target="_new3">Madhusudan Parthasarathy
 \, University of Illinois at Urbana-Champaign</a></li>
 </ul>
 <ul>
 	<l
 i>Featured talk on Games\, Synthesis\, Verification and Learning: A Bird's 
 Eye View of AlgoSyn
 by <a href="http://www.automata.rwth-aachen.de/%7Etho
 mas/" target="_new3">Wolfgang Thomas\, RWTH Aachen U.</a></li>
 </ul>
 Re
 gister and more information: <a href="http://algo.rwth-aachen.de/fallschool
 /">here</a>
ORGANIZER:algoadmin
END:VEVENT
BEGIN:VEVENT
UID:20130912T1334Z-1378992851.8959-EO-639-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20130912T104346Z
LAST-MODIFIED:20131105T102326Z
DTSTART:20131113T090000Z
DTEND:20131113T103000Z
SUMMARY: Presentation Matteo Mio
DESCRIPTION: First Talk: Game Semantics for Probabilistic mu-Calculi In thi
 s talk I will consider several probabilistic (or quantitative) variants of 
 Kozen&#8217\;s Modal mu-Calculus\, designed for expressing properties of pr
 obabilistic-nondeterministic transition systems. Two type of semantics can 
 be defined for these logics: &#8230\; <a href="http://www.algosyn.rwth-aach
 en.de/events/event/presentation-matteo-mio/">Continue reading <span class="
 meta-nav">&#8594\;</span></a>
X-ALT-DESC;FMTTYPE=text/html: <strong>First Talk: Game Semantics for Probab
 ilistic mu-Calculi</strong>
 
 In this talk I will consider several proba
 bilistic (or quantitative) variants of Kozen's Modal mu-Calculus\, designed
  for expressing properties of probabilistic-nondeterministic transition sys
 tems. Two type of semantics can be defined for these logics: one denotation
 al and one based on a novel kind of games which I call Tree games. I will d
 iscuss the main result of my PhD thesis: the equivalence of the two semanti
 cs (proved in ZFC set theory extended with Martin’s Axiom at the first unco
 untable cardinal). I will also present some more recent results (joint work
  with Alex Simpson).
LOCATION:E3 Room 2.22
GEO:50.778320;6.060860
ORGANIZER:Helen Bolke-Hermanns
END:VEVENT
BEGIN:VEVENT
UID:20131105T1724Z-1383672283.8365-EO-1184-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20131105T101611Z
LAST-MODIFIED:20131105T102401Z
DTSTART:20131114T090000Z
DTEND:20131114T103000Z
SUMMARY: Presentation Matteo Mio
DESCRIPTION: Second Talk: Semantic Foundations of Quantitative (real-valued
 ) Logics based on Functional Analysis Abstract: Several notions of bisimula
 tion for Probabilistic Nondeterministic Transition Systems (PNTS) have been
  proposed in the literature. I will develop the theory of what I call &#822
 0\;Upper-Expectation bisimilarity&#8221\; &#8230\; <a href="http://www.algo
 syn.rwth-aachen.de/events/event/presentation-matteo-mio-2/">Continue readin
 g <span class="meta-nav">&#8594\;</span></a>
X-ALT-DESC;FMTTYPE=text/html: <strong>Second Talk: Semantic Foundations of 
 Quantitative (real-valued) Logics based on Functional Analysis</strong>
 

 
 Abstract: Several notions of bisimulation for Probabilistic Nondeterminis
 tic Transition Systems (PNTS) have been proposed in the literature. I will 
 develop the theory of what I call "Upper-Expectation bisimilarity" using st
 andard results of linear algebra and functional analysis and provide strong
  mathematical foundations for real-valued modal logics for PNTS's.
LOCATION:E3 Room 2.22
GEO:50.778320;6.060860
ORGANIZER:Isabel Jahns
END:VEVENT
BEGIN:VEVENT
UID:20131121T1131Z-1385033481.5588-EO-1236-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20131121T102332Z
LAST-MODIFIED:20131125T113145Z
DTSTART;VALUE=DATE:20131127
DTEND;VALUE=DATE:20131128
SUMMARY: Presentation Namit Chaturvedi: Languages of Infinite Traces and De
 terministic Asynchronous Automata
DESCRIPTION: Abstract: In the theory of deterministic automata for language
 s of infinite words\, a fundamental result relates the family of infinitary
  limits of regular languages and the family of omega-languages recognized b
 y deterministic Buechi automata. Furthermore\, a theorem due to L. &#8230\;
  <a href="http://www.algosyn.rwth-aachen.de/events/event/presentation-namit
 -chaturvedi/">Continue reading <span class="meta-nav">&#8594\;</span></a>
X-ALT-DESC;FMTTYPE=text/html: <b></b><span style="font-size: small\;"><span
 >Abstract: </span></span>
 
 <span style="font-size: small\;"><span>In th
 e theory of deterministic automata for languages of infinite words\, a fund
 amental result relates the family of infinitary limits of regular languages
  and the family of omega-languages recognized by deterministic Buechi autom
 ata. Furthermore\, a theorem due to L. Landweber states that an omega-regul
 ar language is recognized by a deterministic Buechi automaton if and only i
 f it is recognized by a deterministic Muller automaton whose acceptance com
 ponent is closed under supersets. With the known definitions of asynchronou
 s automata\, these results does not extend to the context of traces. We int
 roduce the family of deterministic\, synchronization-aware asynchronous aut
 omata which allows us to establish these results\, while the definition of 
 Muller automata obtained therein captures all omega-regular trace languages
 . We also positively answer an open question in the theory of traces\, name
 ly\, whether every omega-regular trace language can be expressed as a finit
 e Boolean combination of deterministically Buechi recognizable languages.</
 span></span>
ORGANIZER:Isabel Jahns
END:VEVENT
BEGIN:VEVENT
UID:20131121T1131Z-1385033481.5623-EO-1237-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20131121T102426Z
LAST-MODIFIED:20131121T102426Z
DTSTART;VALUE=DATE:20131211
DTEND;VALUE=DATE:20131212
SUMMARY: Presentation Friedrich Gretz
X-ALT-DESC;FMTTYPE=text/html: 
ORGANIZER:Isabel Jahns
END:VEVENT
BEGIN:VEVENT
UID:20131121T1131Z-1385033481.5646-EO-1238-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20131121T102456Z
LAST-MODIFIED:20131211T133300Z
DTSTART;VALUE=DATE:20131212
DTEND;VALUE=DATE:20131213
SUMMARY: Presentation Friedrich Gretz
X-ALT-DESC;FMTTYPE=text/html: 
LOCATION:E3 room 2.22 (2nd floor)
GEO:50.778590;6.064304
ORGANIZER:Ulrich Loup
END:VEVENT
BEGIN:VEVENT
UID:20140108T1205Z-1389182730.7988-EO-1244-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20140108T114407Z
LAST-MODIFIED:20140109T102616Z
DTSTART:20140115T090000Z
DTEND:20140115T103000Z
SUMMARY: Presentation Christian Meirich: Capacity of a railway network
DESCRIPTION: On 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 &#8230\;
  <a href="http://www.algosyn.rwth-aachen.de/events/event/presentation-chris
 tian-meirich/">Continue reading <span class="meta-nav">&#8594\;</span></a>
 
X-ALT-DESC;FMTTYPE=text/html: On behalf of the German Railway Authority (Ei
 senbahnbundesamt) the suitability of a parameter “Capacity of railway infra
 structure” in the target and performance agreement (LuFV) between the feder
 al government and Deutsche Bahn AG has been analyzed.
 
 Today the capaci
 ty of railway lines can be calculated as well as the capacity of railway no
 des by means of analytic algorithms. The scope of the work was to investiga
 te if it is possible to define one single parameter “Capacity” for the whol
 e railway network. Therefore methods to aggregate the single values for lin
 es and nodes have been analyzed.
 
 Currently there is no generally accep
 ted method to allocate the key figures of lines and nodes. As a result a si
 ngle parameter to describe a railway network’s capacity is not given nowada
 ys.
LOCATION:Room 5052
GEO:50.778320;6.060860
ORGANIZER:Helen Bolke-Hermanns
END:VEVENT
BEGIN:VEVENT
UID:20140124T1020Z-1390558813.8904-EO-1253-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20140124T101407Z
LAST-MODIFIED:20140124T101407Z
DTSTART:20140205T090000Z
DTEND:20140205T103000Z
SUMMARY: project &#8220\;Mechanisms of scientific life&#8221\;
DESCRIPTION: Presentation of the first results an next steps
X-ALT-DESC;FMTTYPE=text/html: Presentation of the first results an next ste
 ps
LOCATION:Room 5052
GEO:50.778320;6.060860
ORGANIZER:Helen Bolke-Hermanns
END:VEVENT
BEGIN:VEVENT
UID:20140124T1050Z-1390560613.6427-EO-1254-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20140124T102616Z
LAST-MODIFIED:20140325T094122Z
DTSTART:20140326T100000Z
DTEND:20140327T130000Z
SUMMARY: AlgoSyn-Workshop together with GK PUMA (Programm- Und Modell-Analy
 se\, TU LMU)
DESCRIPTION: 1st Day\, 26.03.2014 10.30  Bus Departure (Entrance Parkinglot
  Mies-van-der-Rohe-Str.) 12:30 Lunch at Bonn-Aachen International Center fo
 r Information Technology B-IT\; Dahlmannstraße 2\; D-53113 Bonn 14.00 Prese
 ntation by the representative H. Seidl und W. Thomas 14.30- 15.45 Short pre
 sentations from Aachen (7 min) &#8230\; <a href="http://www.algosyn.rwth-aa
 chen.de/events/event/algosyn-workshop-togehter-with-gk-puma-programm-und-mo
 dell-analyse-tu-lmu/">Continue reading <span class="meta-nav">&#8594\;</spa
 n></a>
X-ALT-DESC;FMTTYPE=text/html: 1st Day\, 26.03.2014
 
 10.30  Bus Departur
 e (Entrance Parkinglot Mies-van-der-Rohe-Str.)
 
 12:30 Lunch at Bonn-Aac
 hen International Center for Information Technology B-IT\; Dahlmannstraße 2
 \; D-53113 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)
 
 17.30 - 18.30 Visit to Arithmeum
 
 20.00 Dinner
 
 
 2nd Day: 27.03.
 
 9.00 - 9.10 Begin/Feedback
 
 9.10  - 9.55 Presentat
 ion Prof. Thomas: Richard Buechi - Persönliche Eindrücke zu Leben und Werk 
 eines großen Forschers
 
 9.55 - 10.40 Presentation Dr. Martin Zimmermann
 : Degrees of Lookahead in Weak Regular Infinite Games
 
 10.40 - 11.00 Co
 ffee Break
 
 11.00 - 12.30 Presentation from Munich
 
 12.30 - 13.30 L
 unch
 
 13.30 - 14.15 Project from Aachen "Mechanisms of Scientific Life"
 
 
 14.15 - 14.30 Coffee Break
 
 14.30 - 16.00 Conference Project 2015
  /Future Work
 
 &nbsp\;
 <div>
 <h1>1      Adressen</h1>
 </div>
 Ho
 tel Acora\, <a href="https://mail.comsys.rwth-aachen.de/owa/redir.aspx?C=2a
 adab99374d4004b02a6871b6b04971&amp\;URL=http%3a%2f%2fwww.acora.de" target="
 _blank">www.acora.de</a>
 
 Westpreußenstraße 20-30
 D-53119 Bonn
 
 T
 el.: +49 (0) 228 / 66 86-0
 E-Mail: <a href="mailto:bonn@acora.de">bonn@ac
 ora.de</a>
 
 Arithmeum
 
 Lennéstrasse 2\, 53113 Bonn\, Tel: 02 28 - 7
 3 87 90
 Öffnungszeiten: Dienstag - Sonntag\, 11:00 - 18:00
 
 &nbsp\;

  
 B-IT Zentrum
 
 Dahlmannstraße 2\, 53113 Bonn
 
 &nbsp\;
 
 Risto
 rante - Pizzeria "Tuscolo"
 
 Kaiser-Karl-Ring 63
 53111 Bonn
 
 0228 
 694665
 
 <a href="http://www.tuscolo.de/"> www.tuscolo.de </a>
 
ORGANIZER:Helen Bolke-Hermanns
END:VEVENT
BEGIN:VEVENT
UID:20140410T1155Z-1397130937.5945-EO-1333-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20140410T114636Z
LAST-MODIFIED:20140429T072414Z
DTSTART:20140423T080000Z
DTEND:20140423T090000Z
SUMMARY: Benedikt Brütsch: Synthesizing Structured Reactive Programs: How M
 uch Memory Do They Need?
DESCRIPTION: Benedikt Brütsch: &#8220\;Synthesizing Structured Reactive Pro
 grams: How Much Memory Do They Need?&#8221\;. Abstract: Existing approaches
  to the synthesis of controllers in reactive systems typically involve the 
 construction of transition systems such as Mealy automata. In 2011\, Madhus
 udan proposed structured programs &#8230\; <a href="http://www.algosyn.rwth
 -aachen.de/events/event/algosyn-presentation/">Continue reading <span class
 ="meta-nav">&#8594\;</span></a>
X-ALT-DESC;FMTTYPE=text/html: <span><span style="font-family: Verdana\;">Be
 nedikt Brütsch: "</span></span><span><span style="font-family: Verdana\;">S
 ynthesizing Structured Reactive Programs: How Much Memory Do They Need?".

  </span></span>
 <span><span style="font-family: Verdana\;">Abstract:
 Ex
 isting approaches to the synthesis of controllers in reactive systems typic
 ally involve the construction of transition systems such as Mealy automata.
  In 2011\, Madhusudan proposed structured programs over a finite set of Boo
 lean variables as a more succinct formalism to represent the controller. He
  provided an algorithm to construct such a program from a given omega-regul
 ar specification without synthesizing a transition system first. The comple
 xity of his algorithm is doubly exponential in the number of Boolean variab
 les that can be used by the program.
 
 In this talk\, I will show a supe
 rpolynomial lower bound for the number of Boolean variables that are requir
 ed for a structured program to satisfy a given LTL specification\, (almost)
  matching the known upper bound. </span></span>
LOCATION:Room 5052
GEO:50.778320;6.060860
ORGANIZER:Helen Bolke-Hermanns
END:VEVENT
BEGIN:VEVENT
UID:20140410T1155Z-1397130937.5966-EO-1334-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20140410T114655Z
LAST-MODIFIED:20140429T072839Z
DTSTART:20140507T080000Z
DTEND:20140507T090000Z
SUMMARY: Visit the Railway Signalling Lab (ELVA) of the Institute of Transp
 ort Science
DESCRIPTION: Visit the Railway Signalling Lab (ELVA) of the Institute of Tr
 ansport Science. &#8220\;Synthesizing Structured Reactive Programs: How Muc
 h Memory Do They Need?&#8221\;. The meeting point will be in the foyer of t
 he building of civil engineering (Mies-van-der-Rohe-Straße 1) at 10.15 &#82
 30\; <a href="http://www.algosyn.rwth-aachen.de/events/event/algosyn-presen
 tation-2/">Continue reading <span class="meta-nav">&#8594\;</span></a>
X-ALT-DESC;FMTTYPE=text/html: Visit the Railway Signalling Lab (ELVA) of th
 e Institute of Transport Science.
 "Synthesizing Structured Reactive Progr
 ams: How Much Memory Do They Need?".
 
 The meeting point will be in the 
 foyer of the building of civil engineering (Mies-van-der-Rohe-Straße 1) at 
 10.15 a. m..
 
 The AlgoSyn members starting from the Informatikzentrum w
 ill meet in front of room 5052 at 10.00 a. m.
 
 &nbsp\;
 
 &nbsp\;
 

 
 <b>The Railway Signalling Lab of RWTH Aachen University</b>
 
 The Inst
 itute of Transport Science of RWTH Aachen University holds a Railway Signal
 ling Lab for research and development\, for the education teaching of stude
 nts and for further educational seminars. The lab has several functional mo
 dels with different scales. There is a railway network models with scale 0\
 , which can be controlled by different types of interlocking systems. The m
 odel was built between 1960 and 1962 in the basement of the new building of
  the Faculty of Civil Engineering. The special clearance\, traction voltage
  and track-release of the lab require certain adaptations when using genera
 l scale 0 vehicles.
 
 <b>Interlocking</b>
 
 The scale-0-model is cont
 rolled by seven original interlocking systems. Four mechanical interlocking
  boxes are situated. One station is controlled by two electromechanical int
 erlocking boxes of type E 43. Further there is another station which is ope
 rated by a relay interlocking box of type DrS.
 
 The station (type DrS) 
 is supplied with an automatic presence-of-trains indication. The operation 
 of the track circuits is simulated by the model. The automatic block sectio
 ns between two stations DrS and E 43 are controlled by track circuits\, too
 . All other sections are protected by electric manual blocks. The block in 
 E 43 and DrS is partly supported by motor inductors.
 
 <b>Operation</b>

 
 
 The scale-0-model can be used in two modes for educational and further
  educational purpose. In the first mode\, special switch orders can be simu
 lated and trained for regular-\, irregular- and disturbed operation. In thi
 s special operation it is important that the block handles and plungers\, e
 mergency buttons and storing relays can be directly manipulated for educati
 onal reasons\, which is not possible in real operation for safety reason. I
 n the second mode\, it is possible to operate the lab with a given timetabl
 e of 30 minutes. This period can be stretched out to one hour to let the st
 udents have time enough to be familiarized to the system. After familiarizi
 ng is finished\, it is also possible to accelerate the model clock. The exp
 eriences the students achieved by operating after a given timetable is very
  useful. The students run into high level of operational stress that might 
 lead to mistakes that gives rise to disposing problems\, like for example a
  deadlock.
LOCATION:Room 5052
GEO:50.778320;6.060860
ORGANIZER:Helen Bolke-Hermanns
END:VEVENT
BEGIN:VEVENT
UID:20140410T1155Z-1397130937.5986-EO-1335-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20140410T114709Z
LAST-MODIFIED:20140505T085331Z
DTSTART:20140528T080000Z
DTEND:20140528T090000Z
SUMMARY: Benjamin Kaminski: Analyzing Expected Outcomes and Almost-Sure Ter
 mination of Probabilistic Programs is Hard
DESCRIPTION: We consider the hardness of computing expected outcomes and al
 most-sure termination of probabilistic programs. We show that deciding almo
 st-sure termination and deciding whether the expected outcome of a program 
 equals a given rational value is $\\Pi^0_2$-complete. Computing lower and u
 pper &#8230\; <a href="http://www.algosyn.rwth-aachen.de/events/event/algos
 yn-presentation-3/">Continue reading <span class="meta-nav">&#8594\;</span>
 </a>
X-ALT-DESC;FMTTYPE=text/html: <span style="font-size: small\;">We consider 
 the hardness of computing expected outcomes and almost-sure termination of 
 probabilistic programs. We show that deciding almost-sure termination and d
 eciding whether the expected outcome of a program equals a given rational v
 alue is $\\Pi^0_2$-complete. Computing lower and upper bounds on the expect
 ed outcome is shown to be recursively enumerable and $\\Sigma^0_2$-complete
 \, respectively.
 </span>
LOCATION:Room 5052
GEO:50.778320;6.060860
ORGANIZER:Helen Bolke-Hermanns
END:VEVENT
BEGIN:VEVENT
UID:20140410T1155Z-1397130937.6006-EO-1336-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20140410T114727Z
LAST-MODIFIED:20140617T071107Z
DTSTART:20140702T080000Z
DTEND:20140702T090000Z
SUMMARY: Ibtissem Ben Makhlouf and Sarah Winter: Presentation of their work
DESCRIPTION: Ibtissem 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 represente
 d as transitions between locations\, in which the continuous part is descri
 bed as &#8230\; <a href="http://www.algosyn.rwth-aachen.de/events/event/alg
 osyn-presentation-4/">Continue reading <span class="meta-nav">&#8594\;</spa
 n></a>
X-ALT-DESC;FMTTYPE=text/html: <p style="text-align: left\;" align="center">
 Ibtissem Ben Makhlouf: Reachability Analysis of Hybrid Systems Using Geomet
 ric Approximations</p>
 <p style="text-align: left\;">Hybrid systems combi
 ne discrete events and continuous behaviors in the same framework. The disc
 rete part is represented as transitions between locations\, in which the co
 ntinuous part is described as a differential equation and that generally in
  a confined invariant domain. The transitions are commonly triggered if a r
 elated guard condition is fulfilled. After an eventually reset condition\, 
 the hybrid automaton springs to the next location if its invariant conditio
 n is met.</p>
 <p style="text-align: left\;">The reachability analysis con
 sists in computing all states reached by a hybrid automaton when starting w
 ith an initial set or under uncertainties in the input.</p>
 <p style="tex
 t-align: left\;">In this talk\, I will give an overview on methods for comp
 uting reachable sets of linear time-invariant hybrid systems.  I will parti
 cularly focus on techniques based on set mapping theory and geometric set a
 pproximations.</p>
 <p style="text-align: left\;">Sarah Winter: Synthesis 
 of Deterministic Top-down Tree Transducers from Automatic Tree Relations</p
 >
 <p style="text-align: left\;">We consider the synthesis of deterministi
 c tree transducers from automaton definable specifications\, given as binar
 y relations\, over finite trees. We consider the case of specifications tha
 t are deterministic top-down tree automatic\, meaning the specification is 
 recognizable by a deterministic top-down tree automaton that reads the two 
 given trees synchronously in parallel. In this setting we study tree transd
 ucers that are allowed to have either bounded delay or arbitrary delay.Dela
 y is caused whenever the transducer reads a symbol from the input tree but 
 does not produce output.</p>
 <p style="text-align: left\;">We provide dec
 ision procedures for both bounded and arbitrary delay that yield determinis
 tic top-down tree transducers which realize the specification for valid inp
 ut trees.Similar to the case of relations over words\, we use two-player ga
 mes to obtain our results.</p>
LOCATION:Room 5052
GEO:50.778320;6.060860
ORGANIZER:Helen Bolke-Hermanns
END:VEVENT
BEGIN:VEVENT
UID:20140410T1155Z-1397130937.6026-EO-1337-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20140410T114742Z
LAST-MODIFIED:20140613T122403Z
DTSTART;VALUE=DATE:20140716
DTEND;VALUE=DATE:20140717
SUMMARY: Christina Jansen: Generating Inductive Predicates for Symbolic Exe
 cution of Pointer-Manipulating Programs
DESCRIPTION: Generating Inductive Predicates for Symbolic Execution of Poin
 ter-Manipulating Programs &#160\; Separation Logic (SL) is an extension of 
 Hoare Logic that supports reasoning about pointer-manipulating programs. It
  employs inductively-defined predicates for specifying the (dynamic) data s
 tructures maintained at runtime\, such as &#8230\; <a href="http://www.algo
 syn.rwth-aachen.de/events/event/algosyn-presentation-5/">Continue reading <
 span class="meta-nav">&#8594\;</span></a>
X-ALT-DESC;FMTTYPE=text/html: Generating Inductive Predicates for Symbolic 
 Execution of Pointer-Manipulating Programs
 
 &nbsp\;
 
 Separation Log
 ic (SL) is an extension of Hoare Logic that supports reasoning about pointe
 r-manipulating programs. It employs inductively-defined predicates for spec
 ifying the (dynamic) data structures maintained at runtime\, such as lists 
 or trees. To support symbolic execution\, SL introduces abstraction rules t
 hat yield symbolic representations of concrete heap states. Whenever concre
 te program instructions are to be applied\, so-called unrolling rules are u
 sed to locally concretise the symbolic heap. To enable automatic generation
  of a complete set of unrolling rules\, however\, predicate definitions hav
 e to meet certain requirements\, which are currently only implicitly specif
 ied and manually established.
 
 &nbsp\;
 
 To tackle this problem\, we
  exploit the relationship between SL and hyperedge replacement grammars (HR
 Gs). The latter represent (abstracted) heaps by hypergraphs containing plac
 eholders whose interpretation is specified by grammar rules. Earlier work h
 as shown that the correctness of heap abstraction using HRGs requires certa
 in structural properties\, such as increasingness\, which can automatically
  be established. We show that it is exactly the Separation Logic counterpar
 ts of those properties that enable a direct generation of abstraction and u
 nrolling rules from predicate definitions for symbolic execution.
 
 &nbs
 p\;
 
 Technically\, this result is achieved by first providing formalisa
 tions of the structural properties in SL. We then extend an existing transl
 ation between SL and HRGs such that it covers all HRGs describing data stru
 ctures\, and show that it preserves these structural properties.
LOCATION:Room 5052
GEO:50.778320;6.060860
ORGANIZER:Helen Bolke-Hermanns
END:VEVENT
BEGIN:VEVENT
UID:20140730T1015Z-1406715359.35-EO-1390-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20140730T100554Z
LAST-MODIFIED:20140730T100640Z
DTSTART:20140806T080000Z
DTEND:20140806T213000Z
SUMMARY: Oliver Göbel: Online Independent Set Beyond the Worst-Case
DESCRIPTION: Title: Online Independent Set Beyond the Worst-Case Abstract: 
 We investigate online algorithms for maximum independent set on graph class
 es with bounded inductive independence number $\\rho$ like interval and dis
 k graphs with applications to\, e.g.\, task scheduling\, spectrum allocatio
 n and admission &#8230\; <a href="http://www.algosyn.rwth-aachen.de/events/
 event/oliver-gobel-online-independent-set-beyond-the-worst-case/">Continue 
 reading <span class="meta-nav">&#8594\;</span></a>
X-ALT-DESC;FMTTYPE=text/html: Title: Online Independent Set Beyond the Wors
 t-Case
 
 Abstract: We investigate online algorithms for maximum independ
 ent set on graph classes with bounded inductive independence number $\\rho$
  like interval and disk graphs with applications to\, e.g.\, task schedulin
 g\, spectrum allocation and admission control. In the online setting\, node
 s of an unknown graph arrive one by one over time. An online algorithm has 
 to decide whether an arriving node should be included into the independent 
 set. Since traditional (worst-case) competitive analysis only yields devast
 ating results\, we conduct a stochastic analysis of the problem and introdu
 ce a generic sampling approach that allows to devise online algorithms for 
 a variety of input models.
LOCATION:Room 5052
GEO:50.778320;6.060860
ORGANIZER:Helen Bolke-Hermanns
END:VEVENT
BEGIN:VEVENT
UID:20140925T0845Z-1411634759.1848-EO-1398-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20140925T083115Z
LAST-MODIFIED:20140925T083115Z
DTSTART:20141022T080000Z
DTEND:20141022T093000Z
SUMMARY: Presentation of Johanna Nellen
X-ALT-DESC;FMTTYPE=text/html: 
LOCATION:Room 5052
GEO:50.778320;6.060860
ORGANIZER:Helen Bolke-Hermanns
END:VEVENT
BEGIN:VEVENT
UID:20141021T0849Z-1413881398.7766-EO-1400-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20141021T084039Z
LAST-MODIFIED:20141021T084039Z
DTSTART:20141022T080000Z
DTEND:20141022T093000Z
SUMMARY: Johanna Nellen: A CEGAR Approach for the Reachability Analysis of 
 Sequential Function Charts
DESCRIPTION: Johanna Nellen: A CEGAR Approach for the Reachability Analysis
  of Sequential Function Charts We address the safety analysis of chemical p
 lants controlled by programmable logic controllers (PLCs). We consider sequ
 ential function charts (SFCs) for the programming of the PLCs\, extended &#
 8230\; <a href="http://www.algosyn.rwth-aachen.de/events/event/johanna-nell
 en-a-cegar-approach-for-the-reachability-analysis-of-sequential-function-ch
 arts/">Continue reading <span class="meta-nav">&#8594\;</span></a>
X-ALT-DESC;FMTTYPE=text/html: <b>Johanna Nellen: A CEGAR Approach for the R
 eachability Analysis of Sequential Function Charts</b>
 
 We address the 
 safety analysis of chemical plants controlled by programmable logic control
 lers (PLCs). We consider sequential function charts (SFCs) for the programm
 ing of the PLCs\, extended with the specification of the dynamic plant beha
 vior. The resulting hybrid SFC models can be transformed to hybrid automata
 \, opening the way to the application of advanced techniques for their reac
 hability analysis.
 
 However\, the hybrid automata models are often too 
 large to be analyzed.
 
 To keep the size of the models moderate\, we pro
 pose a counterexample-guided abstraction refinement (CEGAR) approach\, whic
 h starts with the purely discrete SFC model of the controller and extends i
 t with those parts of the dynamic behavior\, which are relevant for proving
  or disproving safety.
LOCATION:Room 5052
GEO:50.778320;6.060860
ORGANIZER:Helen Bolke-Hermanns
END:VEVENT
BEGIN:VEVENT
UID:20141021T0849Z-1413881398.7796-EO-1401-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20141021T084146Z
LAST-MODIFIED:20141022T070445Z
DTSTART:20141031T100000Z
DTEND:20141031T113000Z
SUMMARY: Ufuk Topcu: Correct-By-Construction Control Synthesis for Autonomo
 us Systems
DESCRIPTION: Ufuk Topcu: Correct-By-Construction Control Synthesis for Auto
 nomous Systems How can we affordably build trustworthy autonomous\, network
 ed systems? Partly motivated by this question\, I describe a shift from the
  traditional &#8220\;design+verify&#8221\; approach to &#8220\;specify+synt
 hesize&#8221\; in model-based engineering. I then discuss our &#8230\; <a h
 ref="http://www.algosyn.rwth-aachen.de/events/event/ufuk-topcu-correct-by-c
 onstruction-control-synthesis-for-autonomous-systems/">Continue reading <sp
 an class="meta-nav">&#8594\;</span></a>
X-ALT-DESC;FMTTYPE=text/html: <b>Ufuk Topcu: Correct-By-Construction Contro
 l Synthesis for Autonomous Systems</b>
 
 How can we affordably build tru
 stworthy autonomous\, networked systems?
 
 Partly motivated by this ques
 tion\, I describe a shift from the traditional "design+verify" approach to 
 "specify+synthesize" in model-based engineering. I then discuss our recent 
 results on automated synthesis of correct-by-construction\, hierarchical co
 ntrol protocols. These results account for hybrid dynamics that are subject
  to rich temporal logic specifications and heterogenous uncertainties\, and
  that operate in adversarial environments. They combine ideas from control 
 theory with those from computer science\, and exploit underlying system-the
 oretic interpretations to suppress the inherent computational complexity. T
 he expressivity of the resulting design methodology enables us to formally 
 investigate a number of emerging issues in autonomous\, networked systems. 
 I conclude my talk with a brief overview of several such issues from my ong
 oing projects: (i) compositional synthesis for the so-called fractionated s
 ystems\; (ii) effects of perception imperfections on protocol synthesis\; (
 iii) interfaces between learning modules and reactive controllers with prov
 able guarantees of correctness\; and (iv) human-embedded autonomy.
 
 &nb
 sp\;
 
 Bio:
 
 Ufuk Topcu is a Research Assistant Professor in the Dep
 artment of Electrical and Systems Engineering at the University of Pennsylv
 ania.
 
 He received his Ph.D. from the University of California\, Berkel
 ey and was a Postdoctoral Scholar at the California Institute of Technology
  until 2012. His research is on the analysis\, design\, and verification of
  autonomous\, networked systems.
ORGANIZER:Helen Bolke-Hermanns
END:VEVENT
BEGIN:VEVENT
UID:20140808T0910Z-1407489033.6587-EO-1392-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20140808T085929Z
LAST-MODIFIED:20140808T085929Z
DTSTART;VALUE=DATE:20141106
DTEND;VALUE=DATE:20141107
SUMMARY: AlgoSyn &#8211\; FAllWorkshop in Schleiden
DESCRIPTION: Jährlicher AlgoSyn-interner Workshop
X-ALT-DESC;FMTTYPE=text/html: Jährlicher AlgoSyn-interner Workshop
ORGANIZER:Helen Bolke-Hermanns
END:VEVENT
BEGIN:VEVENT
UID:20141111T0919Z-1415697551.532-EO-1523-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20141111T081546Z
LAST-MODIFIED:20141118T083320Z
DTSTART:20141126T090000Z
DTEND:20141126T103000Z
SUMMARY: Presentation of Christian Meirich
DESCRIPTION: Präsentation von Christian Meirich: Erhöhung der Leistungsfähi
 gkeit 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 e
 s nicht möglich die einzelnen Kapazitäten von &#8230\; <a href="http://www.
 algosyn.rwth-aachen.de/events/event/presentation-of-christian-meirich/">Con
 tinue reading <span class="meta-nav">&#8594\;</span></a>
X-ALT-DESC;FMTTYPE=text/html: Präsentation von Christian Meirich: <b>Erhöhu
 ng der Leistungsfähigkeit durch eine optimale Ausnutzung von Kapazitäten de
 s Eisenbahnnetzen </b>
 
 Im Eisenbahnwesen beschreibt die Kapazität die 
 zulässige Anzahl an Zugfahrten auf einem Infrastrukturbereich innerhalb ein
 es Zeitfensters. Derzeit ist es nicht möglich die einzelnen Kapazitäten von
  Eisenbahnstrecken mit denen der Eisenbahnknoten zu verrechnen\, da untersc
 hiedliche Rechenansätze hierfür verwendet werden. Somit lassen sich momenta
 n zwar lokale Engpässe identifizieren\, jedoch können globale Aussagen nur 
 grob abgeschätzt werden. Ziel ist es für Eisenbahnnetze netzweite Aussagen 
 über (zukünftige) Engpässe treffen zu können und die wirksamsten Engpassbes
 eitigungen zu ermitteln. Im Rahmen der strategischen Netzplanung kommt der 
 Bundesverkehrswegeplan zur Anwendung. Dieser ist eine Zusammenstellung in F
 orm eines verkehrsträgerübergreifenden Investitionsrahmenplans der Bundesre
 gierung. Er beinhaltet neben den genannten Engpassanalysen auch die Themens
 chwerpunkte der Verkehrserzeugung sowie der Verkehrsumlegung einzelner Verk
 ehre\, um eine sinnvollere Ausnutzung des Netzes zu gewährleisten.
 
 &nb
 sp\;
 
 Ein Optimierungskriterium bei der Zuteilung der Kapazitäten im Ei
 senbahnnetz stellt die maximale Ausnutzung der vorhandenen Netzkapazitäten 
 unter Beachtung eines fest vorgegebenen Routings der Zugfahrten dar (Abfolg
 e von Kanten und Knoten). In einem weiteren Schritt sollen bestimmte Kriter
 ien wie z. B. die Gewichtung von verschiedenen Zügen oder Strecken berücksi
 chtigt werden\, damit ggf. eine sinnvolle Reduktion von Zugfahrten auf best
 immten Streckenabschnitten berücksichtigt werden kann. Als wesentliche Eing
 angsgröße der Optimierung dienen die einzelnen Kapazitäten der Eisenbahnstr
 ecken und Eisenbahnknoten\, wobei der Eisenbahnknoten sich in drei Teilbere
 iche aufgliedert.
 
 &nbsp\;
 
 Der Vortrag erläutert den aktuellen Arb
 eitsstand und stellt noch offene Probleme vor\, welche anschließend gemeins
 am diskutiert werden sollen.
 
 &nbsp\;
LOCATION:Room 5052
GEO:50.778320;6.060860
ORGANIZER:Helen Bolke-Hermanns
END:VEVENT
BEGIN:VEVENT
UID:20141127T1110Z-1417086613.1854-EO-1533-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20141127T105636Z
LAST-MODIFIED:20141127T110622Z
DTSTART:20141211T143000Z
DTEND:20141211T160000Z
SUMMARY: Promotionscafé
DESCRIPTION: Nach der Promotion in die Industrie Mehr Informationen:  www.i
 nformatik.rwth-aachen.de/Promotionscafe/
X-ALT-DESC;FMTTYPE=text/html: Nach der Promotion in die Industrie
 
 <img
  class="alignnone size-medium wp-image-636" alt="Promotionscafe_23_09_2013"
  src="//www.algosyn.rwth-aachen.de/wp-content/uploads/Promotionscafe_11_12_
 14.jpg" width="300" height="212" />
 
 Mehr Informationen:  www.informati
 k.rwth-aachen.de/Promotionscafe/
LOCATION:Room 9220
GEO:50.778476;6.059939
ORGANIZER:Isabel Jahns
END:VEVENT
BEGIN:VEVENT
UID:20141222T1250Z-1419252604.1509-EO-1536-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20141222T114137Z
LAST-MODIFIED:20141222T114252Z
DTSTART:20150107T090000Z
DTEND:20150107T103000Z
SUMMARY: AlgoSyn-Meeting
DESCRIPTION: Agenda Mechanism of Scientific Life FFM 2015 Election: New Ste
 ering Committee
X-ALT-DESC;FMTTYPE=text/html: <strong>Agenda</strong>
 
 Mechanism of Sci
 entific Life
 
 FFM 2015
 
 Election: New Steering Committee
LOCATION:Room 5052
GEO:50.778320;6.060860
ORGANIZER:Helen Bolke-Hermanns
END:VEVENT
BEGIN:VEVENT
UID:20150115T1229Z-1421324947.843-EO-1539-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20150115T081338Z
LAST-MODIFIED:20150115T081338Z
DTSTART:20150116T090000Z
DTEND:20150116T103000Z
SUMMARY: Markus Rabe: Symbolic Approximation of the Bounded Reachability Pr
 obability in Large Markov Chains
DESCRIPTION: Symbolic Approximation of the Bounded Reachability Probability
  in Large Markov Chains &#160\; Abstract: We present a novel technique to a
 nalyze the bounded reachability probability problem for large Markov chains
 . The essential idea is to incrementally search for sets of paths &#8230\; 
 <a href="http://www.algosyn.rwth-aachen.de/events/event/markus-rabe-symboli
 c-approximation-of-the-bounded-reachability-probability-in-large-markov-cha
 ins/">Continue reading <span class="meta-nav">&#8594\;</span></a>
X-ALT-DESC;FMTTYPE=text/html: Symbolic Approximation of the Bounded Reachab
 ility Probability in Large Markov Chains
 
 &nbsp\;
 
 Abstract:
 
 W
 e present a novel technique to analyze the bounded reachability probability
  problem for large Markov chains. The essential idea is to incrementally se
 arch for sets of paths that lead to the goal region and to choose the sets 
 in a way that allows us to easily determine the probability mass they repre
 sent.
 
 &nbsp\;
 
 We encode the search for sets of paths as a sequenc
 e of quantified bitvector problems. To effectively discharge the quantified
  bit vector problems using an SMT solver\, we employ a finite-precision abs
 traction on the Markov chain and a custom quantifier elimination strategy. 
 The experimental evaluation on the PRISM benchmark models demonstrates that
  the approach scales to models that are out of reach for previous methods.

 
 
 &nbsp\;
LOCATION:E3 Room 2.22
GEO:50.778320;6.060860
ORGANIZER:Helen Bolke-Hermanns
END:VEVENT
BEGIN:VEVENT
UID:20150115T1229Z-1421324947.8486-EO-1538-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20150115T080547Z
LAST-MODIFIED:20150115T080547Z
DTSTART:20150122T130000Z
DTEND:20150122T150000Z
SUMMARY: Presentation of Martin Zimmermann and Felix Klein
DESCRIPTION: Speaker: Martin Zimmermann\, Universität des Saarlandes Title:
  The Complexity of Counting Models of Linear-time Temporal Logic Abstract: 
 We determine the complexity of counting models of bounded size of specifica
 tions expressed in Linear-time Temporal Logic. Counting word models is #P-c
 omplete\, if &#8230\; <a href="http://www.algosyn.rwth-aachen.de/events/eve
 nt/presentation-of-martin-zimmermann-and-felix-klein/">Continue reading <sp
 an class="meta-nav">&#8594\;</span></a>
X-ALT-DESC;FMTTYPE=text/html: Speaker: Martin Zimmermann\, Universität des 
 Saarlandes
 
 Title: The Complexity of Counting Models of Linear-time Tem
 poral Logic
 
 Abstract:
 
 We determine the complexity of counting mod
 els of bounded size of specifications expressed in Linear-time Temporal Log
 ic. Counting word models is #P-complete\, if the bound is given in unary\, 
 and as hard as counting accepting runs of non-deterministic polynomial-spac
 e Turing machines\, if the bound is given in binary. Counting tree models i
 s as hard as counting accepting runs of non-deterministic exponential-time 
 Turing machines\, if the bound is given in unary. For a binary encoding of 
 the bound\, the problem is at least as hard as counting accepting runs of n
 on-deterministic exponential space Turing machines. On the other hand\, it 
 is not harder than counting accepting runs of non-deterministic doubly-expo
 nential time Turing machines.
 
 This is joint work with Hazem Torfah.
 
 
 <a href="http://arxiv.org/abs/1408.5752">http://arxiv.org/abs/1408.5752<
 /a>
 
 &nbsp\;
 
 Speaker: Felix Klein\, Universität des Saarlandes
 

 
 Title: How Much Lookahead is Needed to Win Infinite Games?
 
 Abstract:
 
 
 Delay games are two-player games of infinite duration in which one pl
 ayer may delay her moves to obtain a lookahead on her opponent's moves. For
  omega-regular winning conditions it is known that such games can be solved
  in doubly-exponential time and that doubly-exponential lookahead is suffic
 ient.
 
 We improve upon both results by giving an exponential time algor
 ithm and an exponential upper bound on the necessary lookahead. This is com
 plemented by showing EXPTIME-hardness of the solution problem and tight exp
 onential lower bounds on the lookahead. Both lower bounds already hold for 
 safety conditions. Furthermore\, solving delay games with reachability cond
 itions is shown to be PSPACE-complete.
 
 This is joint work with Martin 
 Zimmermann.
 
 <a href="http://arxiv.org/abs/1412.3701">http://arxiv.org/
 abs/1412.3701</a>
ORGANIZER:Helen Bolke-Hermanns
END:VEVENT
BEGIN:VEVENT
UID:20150126T1233Z-1422275591.6502-EO-1541-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20150126T122701Z
LAST-MODIFIED:20150126T122701Z
DTSTART:20150202T150000Z
DTEND:20150202T163000Z
SUMMARY: Presentation Srivathsan Baluguru
DESCRIPTION: Fast detection of cycles in timed automata Abstract: We will p
 resent an algorithm to detect if a cycle in a timed automaton can be iterat
 ed infinitely often. Existing solutions in tools have a complexity which is
  exponential in the number &#8230\; <a href="http://www.algosyn.rwth-aachen
 .de/events/event/presentation-srivathsan-baluguru/">Continue reading <span 
 class="meta-nav">&#8594\;</span></a>
X-ALT-DESC;FMTTYPE=text/html: <strong>Fast detection of cycles in timed aut
 omata</strong>
 
 Abstract: We will present an algorithm to detect if a c
 ycle in a timed automaton can be iterated infinitely often. Existing soluti
 ons in tools have a complexity which is exponential in the number of clocks
 . Our method is polynomial. This method can be incorporated in algorithms f
 or verifying Büchi properties on timed automata. Experiments show a signifi
 cant reduction in search space.
 
 This is joint work with A. Deshpande\,
  F. Herbreteau\, T.T. Tran and I.
 Walukiewicz.
LOCATION:Room 9220
GEO:50.778476;6.059939
ORGANIZER:Isabel Jahns
END:VEVENT
BEGIN:VEVENT
UID:20150202T0954Z-1422870862.0421-EO-1545-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20150202T095357Z
LAST-MODIFIED:20150202T095357Z
DTSTART:20150205T110000Z
DTEND:20150206T120000Z
SUMMARY: Gedenkkolloquium zu Ehren von Prof. Berthold Vöcking
DESCRIPTION: Die Fachgruppe Informatik gedenkt mit einem zweitägigen Kolloq
 uium am 5. und 6. Februar 2015 ihrem leider viel zu früh verstorbenen Freun
 d und Kollegen Berthold Vöcking und lädt dazu herzlich ein. Am Donnerstag a
 b 12 Uhr beginnt das Kolloquium mit einem &#8230\; <a href="http://www.algo
 syn.rwth-aachen.de/events/event/gedenkkolloquium-zu-ehren-von-prof-berthold
 -vocking/">Continue reading <span class="meta-nav">&#8594\;</span></a>
X-ALT-DESC;FMTTYPE=text/html: Die Fachgruppe Informatik gedenkt mit einem z
 weitägigen Kolloquium am 5. und 6. Februar 2015 ihrem leider viel zu früh v
 erstorbenen 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 un
 d Doktoranden\, die den wissenschaftlichen Lebensweg von Berthold Vöcking a
 ufzeichnen. Im Anschluss an die Vorträge ist Donnerstagabend ein gemeinsame
 s Abendessen geplant.
 
 Am Freitag von 10 bis 11 Uhr wird Berthold Vöcki
 ng als Wissenschaftler und seiner akademischen Arbeit in der Informatik ged
 acht. Die Veranstaltung klingt nach einem Vortrag von Bruce Maggs aus.
 <t
 able>
 <tbody>
 <tr>
 <th colspan="2">Vorläufiges Programm</th>
 </tr>

 
 <tr>
 <th colspan="2">Donnerstag\, 5. Februar 2015</th>
 </tr>
 <tr>

  <td>12:00 - 13:00</td>
 <td>Come together</td>
 </tr>
 <tr>
 <td>13:00
  - 13:25</td>
 <td>Friedhelm Meyer auf der Heide -- Berthold's First Theor
 em</td>
 </tr>
 <tr>
 <td>13:25 - 13:40</td>
 <td>Christian Scheideler 
 -- Meine Forschung mit Berthold - ein Glücksfall!</td>
 </tr>
 <tr>
 <td
 >13:40 - 13:55</td>
 <td>Matthias Westermann -- Von Katzen und Autos - Wie
  uns Katzenstreu wieder auf die Spur brachte</td>
 </tr>
 <tr>
 <td>13:5
 5 - 14:10</td>
 <td>Petra Berenbrink -- Berthold und das Always-Go-Left Pr
 otokoll</td>
 </tr>
 <tr>
 <td>14:10 - 14:25</td>
 <td>Bruce Maggs -- .
 ..</td>
 </tr>
 <tr>
 <td>14:25 - 14:45</td>
 <td>Pause</td>
 </tr>
 
 <tr>
 <td>14:45 - 15:10</td>
 <td>Kurt Mehlhorn -- Bertholds Jahre am MPI
  für Informatik</td>
 </tr>
 <tr>
 <td>15:10 - 15:25</td>
 <td>Peter Sa
 nders -- Parallelism and Much More</td>
 </tr>
 <tr>
 <td>15:25 - 15:35<
 /td>
 <td>Christian Schindelhauer -- Rumor Spreading in Berkeley</td>
 </
 tr>
 <tr>
 <td>15:35 - 15:50</td>
 <td>Christian Sohler -- Von Hasen und
  Jägern</td>
 </tr>
 <tr>
 <td>15:50 - 16:20</td>
 <td>Pause</td>
 </t
 r>
 <tr>
 <td>16:20 - 16:45</td>
 <td>Artur Czumaj -- On Random Choices<
 /td>
 </tr>
 <tr>
 <td>16:45 - 17:00</td>
 <td>Heiko Röglin -- Berthold
 s Beiträge zur Smoothed Analysis</td>
 </tr>
 <tr>
 <td>17:00 - 17:30</t
 d>
 <td>Matthias Englert und Harald Räcke -- First Contact - How Berthold 
 introduced us to Research</td>
 </tr>
 <tr>
 <th colspan="2">Freitag\, 6
 . Februar 2015</th>
 </tr>
 <tr>
 <td>10:15 - 10:30</td>
 <td>Ernst Sch
 machtenberg\, Rektor der RWTH University</td>
 </tr>
 <tr>
 <td>10:00 - 
 10:15</td>
 <td>Thomas Seidl\, Fachgruppe Informatik</td>
 </tr>
 <tr>

  <td>10:30 - 10:40</td>
 <td>Christel Baier\, Deutsche Forschungsgemeinsch
 aft</td>
 </tr>
 <tr>
 <td>10:40 - 10:50</td>
 <td>Martin Dietzfelbinge
 r\, Gesellschaft für Informatik</td>
 </tr>
 <tr>
 <td>10:50 - 11:00</td
 >
 <td>Studierende der Informatik\, Fachschaft</td>
 </tr>
 <tr>
 <td>1
 1:15 - 12:15</td>
 <td>Bruce Maggs -- The Internet at the Speed of Light</
 td>
 </tr>
 <tr>
 <td>12:15 - 13:00</td>
 <td>Ausklang</td>
 </tr>
 <
 /tbody>
 </table>
ORGANIZER:Helen Bolke-Hermanns
END:VEVENT
BEGIN:VEVENT
UID:20150224T1038Z-1424774291.1553-EO-1553-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20150224T102352Z
LAST-MODIFIED:20150224T103459Z
DTSTART:20150224T180000Z
DTEND:20150224T203000Z
SUMMARY: Young Researchers Conference
DESCRIPTION: 19:00 &#8211\; 21:30 Welcome (with drinks and snacks) at &#822
 0\;SuperC&#8221\;\, RWTH Aachen (6th Floor)
X-ALT-DESC;FMTTYPE=text/html: <table width="700" border="1" cellspacing="5"
  cellpadding="6">
 <tbody>
 <tr>
 <td width="100">19:00 - 21:30</td>
 <
 td>Welcome (with drinks and snacks) at "SuperC"\, RWTH Aachen (6th Floor)</
 td>
 </tr>
 </tbody>
 </table>
ORGANIZER:Isabel Jahns
END:VEVENT
BEGIN:VEVENT
UID:20140808T0910Z-1407489033.661-EO-1393-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20140808T090017Z
LAST-MODIFIED:20140819T102744Z
DTSTART;VALUE=DATE:20150225
DTEND;VALUE=DATE:20150301
SUMMARY: Young Researchers Conference
DESCRIPTION: Young Researchers Conference &#8220\;Frontiers of Formal Metho
 ds&#8221\; Aachen\, Germany February 25 &#8211\; 27\, 2015 &#160\; organize
 d by the DFG Research Training Groups AlgoSyn (Algorithmic Synthesis of Rea
 ctive and Discrete-Continuous Systems)\, Aachen PUMA (Program and Model Ana
 lysis)\, München QuantLA (Quantitative Logics &#8230\; <a href="http://www.
 algosyn.rwth-aachen.de/events/event/young-researchers-conference/">Continue
  reading <span class="meta-nav">&#8594\;</span></a>
X-ALT-DESC;FMTTYPE=text/html: <div id="header_sagt"></div>
 <h1><a href="h
 ttp://ffm2015.rwth-aachen.de/">Young Researchers Conference "Frontiers of F
 ormal Methods"</a>
 <small>Aachen\, Germany
 February 25 - 27\, 2015</sma
 ll></h1>
 &nbsp\;
 
 organized by the DFG Research Training Groups
 <a 
 href="http://www.algosyn.rwth-aachen.de">AlgoSyn (Algorithmic Synthesis of 
 Reactive and Discrete-Continuous Systems)\, Aachen</a>
 <a href="https://p
 uma.informatik.tu-muenchen.de">PUMA (Program and Model Analysis)\, München<
 /a>
 <a href="http://lat.inf.tu-dresden.de/quantla/">QuantLA (Quantitative
  Logics and Automata)\, Dresden &amp\; Leipzig</a>
 <a href="http://www.sc
 are.uni-oldenburg.de/">SCARE (System Correctness under Adverse Conditons)\,
  Oldenburg</a>
 and the <a href="http://arise.or.at/">Austrian Research Ne
 twork ARiSE (Rigorous System Engineering)</a>
 
 &nbsp\;
 
 This confer
 ence is a forum of young researchers (typically PhD students\, but also mas
 ter students and postdocs) for exchanging current research results and broa
 dening their academic network. The scope of the conference ranges over form
 al and algorithmic methods in computer science in a broad sense. Typical to
 pics are connected with the research areas of the participating research tr
 aining groups as indicated above. The conference consists of invited lectur
 es (1 hour) and short presentations (talks of 12 minutes duration). Submiss
 ions are open for short presentations given by young researchers (up to two
  years after completion of PhD). A short presentation is submitted via the 
 submission webpage with an extended abstract of 2-5 pages written by a sing
 le author. The results may have been accepted or even published elsewhere. 
 Each author is free to submit his/her “best result” (possibly obtained join
 tly with others). Multiple submissions by one author are not permitted. The
  language of the conference is English. Proceedings will be published as a 
 technical report of RWTH Aachen University\, containing extended abstracts 
 of accepted short presentations as well as material from invited lectures. 
 The program committee and the list of invited speakers will be announced du
 ring the summer.
 
 Important Dates:
 <table>
 <tbody>
 <tr>
 <td>Sub
 mission:</td>
 <td>December 15\, 2014</td>
 </tr>
 <tr>
 <td>Notificati
 on:</td>
 <td>January 15\, 2015</td>
 </tr>
 <tr>
 <td>Conference:</td>
 
 <td>February 25 - 27\, 2015</td>
 </tr>
 </tbody>
 </table>
ORGANIZER:Helen Bolke-Hermanns
END:VEVENT
BEGIN:VEVENT
UID:20150224T1038Z-1424774291.1718-EO-1554-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20150224T102622Z
LAST-MODIFIED:20150224T103258Z
DTSTART:20150225T080000Z
DTEND:20150225T193000Z
SUMMARY: Young Researchers Conference
DESCRIPTION: 9:00 &#8211\; 9:15 Welcome 9:15 &#8211\; 10:15 Moshe Vardi: Th
 e Rise and fall of Linear Temporal Logic Coffee Break 10:30 &#8211\; 11:30 
 Shiguang Feng : Path-Checking for MTL and TPTL over Data Words Claudia Cara
 pelle : Satisfiability of ECTL* with constraints Sascha &#8230\; <a href="h
 ttp://www.algosyn.rwth-aachen.de/events/event/young-researchers-conference-
 3/">Continue reading <span class="meta-nav">&#8594\;</span></a>
X-ALT-DESC;FMTTYPE=text/html: <table width="700" border="1" cellspacing="5"
  cellpadding="6">
 <tbody>
 <tr>
 <td width="100">9:00 - 9:15</td>
 <td
 >Welcome</td>
 </tr>
 <tr>
 <td>9:15 - 10:15</td>
 <td>
 <ul>
 	<li>M
 oshe Vardi: The Rise and fall of Linear Temporal Logic</li>
 </ul>
 </td>
 
 </tr>
 <tr>
 <td></td>
 <td>Coffee Break</td>
 </tr>
 <tr>
 <td>10
 :30 - 11:30</td>
 <td>
 <ul>
 	<li>Shiguang Feng : <em>Path-Checking for
  MTL and TPTL over Data Words</em></li>
 	<li>Claudia Carapelle : <em>Sati
 sfiability of ECTL* with constraints</em></li>
 	<li>Sascha Wunderlich : <
 em>Weight Monitoring with Linear Temporal Logic</em></li>
 	<li>Normann De
 cker : <em>On an Extension of Freeze LTL Part I - Decidability</em></li>
 
 	<li>Daniel Thoma : <em>On an Extension of Freeze LTL: Part II - Complexity
 </em></li>
 </ul>
 </td>
 </tr>
 <tr>
 <td></td>
 <td>Coffee Break</t
 d>
 </tr>
 <tr>
 <td>11:45 - 12:45</td>
 <td>
 <ul>
 	<li>Edon Kelmen
 di : <em>Two-player shift-invariant and submixing stochastic games are half
 -positional</em></li>
 	<li>Pierre Carlier : <em>Composition of Stochastic
  Timed Automata</em></li>
 	<li>David Müller : <em>Are Good-for-games Auto
 mata Good for Probabilistic Model Checking?</em></li>
 	<li>Dennis Guck : 
 <em>Markov Reward Automata in Railway Engineering</em></li>
 	<li>Yang Gao
  : <em>Decision Procedure for Stochastic Satisfiability Modulo Theories wit
 h Continuous Domain</em></li>
 </ul>
 </td>
 </tr>
 <tr>
 <td></td>
 
 <td>
 <h2>Lunch Break</h2>
 </td>
 </tr>
 <tr>
 <td>14:00 - 15:00</td>
 
 <td>
 <ul>
 	<li><a>Bernd Finkbeiner: <em>Distributed Synthesis</em></
 a></li>
 </ul>
 </td>
 </tr>
 <tr>
 <td></td>
 <td>Coffee Break</td>

 
 </tr>
 <tr>
 <td>15:20 - 16:20</td>
 <td>
 <ul>
 	<li>Jan Oliver Rin
 gert : <em>Extensible Support for Specification Patterns in GR(1) Synthesis
  -- Work in Progress</em></li>
 	<li>Mickael Randour : <em>Games with Wind
 ow Quantitative Objectives</em></li>
 	<li>Loredana Sorrentino : <em>On Pr
 omptness in Parity Games</em></li>
 	<li>Benedikt Brütsch : <em>Synthesizi
 ng Structured Reactive Programs via Deterministic Tree Automata</em></li>

  	<li>Florian Corzilius : <em>SMT-RAT: An SMT-Compliant Nonlinear Real and 
 Integer Arithmetic Toolbox</em></li>
 </ul>
 </td>
 </tr>
 <tr>
 <td><
 /td>
 <td>Coffee Break</td>
 </tr>
 <tr>
 <td>16:40 - 17:40</td>
 <td>
 
 <ul>
 	<li>Dmitriy Traytel : <em>Derivatives of WS1S Formulas</em></li>
 
 	<li>Stephan Barth : <em>Deciding Monadic Second Order Logic over omega-
 words by Specialized Finite Automata</em></li>
 	<li>Simon Leßenich : <em>
 A Quantitative Counting Monadic Second-Order Logic</em></li>
 	<li>Sarah W
 inter : <em>Uniformization of Automatic Tree Relations by Top-down Tree Tra
 nsducers</em></li>
 	<li>Frederic Reinhardt : <em>Automatic Structures wit
 h Parameters</em></li>
 </ul>
 </td>
 </tr>
 <tr>
 <td>19:00</td>
 <t
 d>Optional: Guided tour through the city\, Fischpüddelchen</td>
 </tr>
 <
 /tbody>
 </table>
ORGANIZER:Isabel Jahns
END:VEVENT
BEGIN:VEVENT
UID:20150224T1038Z-1424774291.1888-EO-1555-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20150224T102840Z
LAST-MODIFIED:20150224T102840Z
DTSTART:20150226T200000Z
DTEND:20150226T225900Z
SUMMARY: Young Researchers Conference
DESCRIPTION: 9:00 &#8211\; 10:00 Jean-Francois Raskin: Variations on the st
 ochastic shortest path problem Coffee Break 10:20 &#8211\; 11:20 Vitaly Per
 evoshchikov : Decomposition of Weighted Timed Automata Parvaneh Babari : A 
 Nivat Theorem for Weighted Picture Automata and Weighted MSO Logics Mohamed
  Abdelaal : Fuzzy Compression &#8230\; <a href="http://www.algosyn.rwth-aac
 hen.de/events/event/young-researchers-conference-4/">Continue reading <span
  class="meta-nav">&#8594\;</span></a>
X-ALT-DESC;FMTTYPE=text/html: <table width="700" border="1" cellspacing="5"
  cellpadding="6">
 <tbody>
 <tr>
 <td width="100">9:00 - 10:00</td>
 <t
 d>
 <ul>
 	<li><a>Jean-Francois Raskin: <em>Variations on the stochastic 
 shortest path problem</em></a></li>
 </ul>
 </td>
 </tr>
 <tr>
 <td></
 td>
 <td>Coffee Break</td>
 </tr>
 <tr>
 <td>10:20 - 11:20</td>
 <td>

 
 <ul>
 	<li>Vitaly Perevoshchikov : <em>Decomposition of Weighted Timed A
 utomata</em></li>
 	<li>Parvaneh Babari : <em>A Nivat Theorem for Weighted
  Picture Automata and Weighted MSO Logics</em></li>
 	<li>Mohamed Abdelaal
  : <em>Fuzzy Compression Refinement via Curvature Tracking</em></li>
 	<li>
 Saifullah Khan : <em>Traffic Data Dissemination in Realistic Urban VANETs En
 vironment</em></li>
 	<li>Andreas Tönnis : <em>Packing Secretaries</em></l
 i>
 </ul>
 </td>
 </tr>
 <tr>
 <td></td>
 <td>Coffee Break</td>
 </t
 r>
 <tr>
 <td>11:40 - 12:40</td>
 <td>
 <ul>
 	<li>Georgel Calin : <em
 >Lazy TSO Reachability</em></li>
 	<li>Veronika Loitzenbauer : <em>A Hiera
 rchical Sparsification Technique for Faster Algorithms in Graphs and Game G
 raphs</em></li>
 	<li>Christina Jansen : <em>Generating Abstract Graph-Bas
 ed Procedure Summaries for Pointer Programs</em></li>
 	<li>Ayrat Khalimov
  : <em>Tight Fair Cutoffs for Conjunctive Guard Systems</em></li>
 	<li>Th
 omas Stroeder : <em>Transformational Termination Analysis of Programs with 
 Pointer Arithmetic</em></li>
 </ul>
 </td>
 </tr>
 <tr>
 <td></td>
 <
 td>
 <h2>Lunch Break</h2>
 </td>
 </tr>
 <tr>
 <td>14:00 - 15:00</td>

 
 <td>
 <ul>
 	<li><a>Azadeh Farzan: <em>Succinct Proofs of Concurrent Pr
 ograms</em></a></li>
 </ul>
 </td>
 </tr>
 <tr>
 <td></td>
 <td>Coffe
 e Break</td>
 </tr>
 <tr>
 <td>15:20 - 16:20</td>
 <td>
 <ul>
 	<li>C
 hristian Dehnert : <em>Fast Debugging of PRISM Models</em></li>
 	<li>Joha
 nnes Hölzl : <em>Probability Theory and Markov Processes in Isabelle/HOL</e
 m></li>
 	<li>René Neumann : <em>A verified LTL model checker</em></li>
 
 	<li>Manuel Gieseking : <em>Trace Refinement of pi-Calculus Processes</em><
 /li>
 	<li>Stefan Schulze Frielinghaus : <em>Inter-procedural Two-Variable
  Herbrand Equalities are in PTIME</em></li>
 </ul>
 </td>
 </tr>
 <tr>

 
 <td></td>
 <td>Coffee Break</td>
 </tr>
 <tr>
 <td>16:40 - 17:40</td>
 
 <td>
 <ul>
 	<li>Markus Teichmann : <em>Regular Context-Free Tree Gram
 mars</em></li>
 	<li>Doreen Heusel : <em>Weighted Unranked Tree Automata o
 ver Tree Valuation Monoids</em></li>
 	<li>Nils Erik Flick : <em>Derivatio
 n Languages of Graph Grammars and Correctness</em></li>
 	<li>Thomas Weidn
 er : <em>Probabilistic Logic and Regular Expressions on Finite Trees</em></
 li>
 	<li>Félix Baschenis : <em>From sweeping transducers to one way trans
 ducers</em></li>
 </ul>
 </td>
 </tr>
 <tr>
 <td>19:30</td>
 <td>Conf
 erence dinner at Tivoli Football Stadium (VIP Lounge)</td>
 </tr>
 </tbod
 y>
 </table>
ORGANIZER:Isabel Jahns
END:VEVENT
BEGIN:VEVENT
UID:20150224T1038Z-1424774291.2055-EO-1556-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20150224T103014Z
LAST-MODIFIED:20150224T103014Z
DTSTART:20150227T080000Z
DTEND:20150227T153000Z
SUMMARY: Young Researchers Conference
DESCRIPTION: 9:00 &#8211\; 10:00 Eric Bodden: SPLlift: statically analyzing
  software product lines in minutes instead of years Coffee Break 10:20 &#82
 11\; 11:20 Bogdan Mihaila : Synthesizing Predicates from Abstract Domain Lo
 sses Suvam Mukherjee : Efficient Shape Analysis of Multithreaded Programs M
 itra Tabaei Befrouei : Abstraction &#8230\; <a href="http://www.algosyn.rwt
 h-aachen.de/events/event/young-researchers-conference-5/">Continue reading 
 <span class="meta-nav">&#8594\;</span></a>
X-ALT-DESC;FMTTYPE=text/html: <table width="700" border="1" cellspacing="5"
  cellpadding="6">
 <tbody>
 <tr>
 <td width="100">9:00 - 10:00</td>
 <t
 d>
 <ul>
 	<li><a>Eric Bodden: <em>SPLlift: statically analyzing software
  product lines in minutes instead of years</em></a></li>
 </ul>
 </td>
 
 </tr>
 <tr>
 <td></td>
 <td>Coffee Break</td>
 </tr>
 <tr>
 <td>10:20
  - 11:20</td>
 <td>
 <ul>
 	<li>Bogdan Mihaila : <em>Synthesizing Predic
 ates from Abstract Domain Losses</em></li>
 	<li>Suvam Mukherjee : <em>Eff
 icient Shape Analysis of Multithreaded Programs</em></li>
 	<li>Mitra Taba
 ei Befrouei : <em>Abstraction and Mining of Traces to Explain Concurrency B
 ugs</em></li>
 	<li>Christian Müller : <em>An Analysis of Universal Inform
 ation Flow based on Self-Compositions</em></li>
 	<li>Björn Engelmann : <e
 m>Formally Verifying Dynamically-typed Programs like Statically-typed Ones 
 – A different perspective</em></li>
 </ul>
 </td>
 </tr>
 <tr>
 <td></
 td>
 <td>Coffee Break</td>
 </tr>
 <tr>
 <td>11:40 - 12:40</td>
 <td>

 
 <ul>
 	<li>Philipp Hoffmann : <em>Negotiations as a concurrency primitiv
 e: Summaries and Games</em></li>
 	<li>Giuseppe Perelli : <em>Strategy Log
 ic: a powerful formalism for game-theoretical issues</em></li>
 	<li>Vadim
  Malvone : <em>Graded Strategy Logic</em></li>
 	<li>Oliver Fernandez Gil 
 : <em>Threshold Concepts in a Lightweight Description Logic</em></li>
 	<l
 i>Andreas Ecke : <em>Relaxing Description Logics Queries using Similarity M
 easures</em></li>
 </ul>
 </td>
 </tr>
 <tr>
 <td></td>
 <td>
 <h2>L
 unch Break</h2>
 </td>
 </tr>
 <tr>
 <td>14:00 - 15:00</td>
 <td>
 <u
 l>
 	<li><a>Joel Ouaknine: <em>Termination of Linear Loops: Algorithmic Ad
 vances and Challenges</em></a></li>
 </ul>
 </td>
 </tr>
 <tr>
 <td></
 td>
 <td>Coffee Break</td>
 </tr>
 <tr>
 <td>15:20 - 16:30</td>
 <td>

 
 <ul>
 	<li>Fabian Immler : <em>Continuous Systems Reachability using Ada
 ptive Runge-Kutta Methods - Formally Verified</em></li>
 	<li>Manuel Eberl
 \, Johannes Hölzl and Tobias Nipkow : <em>A Verified Compiler for Probabili
 ty Density Functions</em></li>
 	<li>Benjamin Lucien Kaminski : <em>Analyz
 ing Expected Outcomes and (Positive) Almost-Sure Termination of Probabilist
 ic Programs is Hard</em></li>
 	<li>Friedrich Gretz : <em>Conditioning in 
 Probabilistic Programming</em></li>
 	<li>Nils Jansen : <em>A Greedy Appro
 ach for the Efficient Repair of Stochastic Models</em></li>
 	<li>Oliver G
 öbel : <em>On Stochastic Input Models in Online Optimization</em></li>
 </
 ul>
 </td>
 </tr>
 </tbody>
 </table>
ORGANIZER:Isabel Jahns
END:VEVENT
BEGIN:VEVENT
UID:20150302T1145Z-1425296737.8026-EO-1559-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20150302T110730Z
LAST-MODIFIED:20150302T111711Z
DTSTART:20150303T160000Z
DTEND:20150303T170000Z
SUMMARY: Vortrag: Die 2 Seiten der Gläsernen Decke
DESCRIPTION: „Die 2 Seiten der Gläsernen Decke“\,  gehalten von Marion Knat
 hs am 03.03 um 17h im SuperC\, Generali Saal &#8211\; Templergraben 55\, 6.
  Etage Frauen in Spitzenpositionen sind immer noch eine Ausnahme. Oftmals w
 ird die berühmte „Gläserne Decke“ als Ursache dafür &#8230\; <a href="http:
 //www.algosyn.rwth-aachen.de/events/event/vortrag-die-2-seiten-der-glaserne
 n-decke/">Continue reading <span class="meta-nav">&#8594\;</span></a>
 
X-ALT-DESC;FMTTYPE=text/html: <p style="text-align: left\;" align="center">
 „<b>Die 2 Seiten der Gläsernen Decke“\,</b>  gehalten von Marion Knaths</p>
 
 <p style="text-align: left\;" align="center"><b>am 03.03 um 17h im Super
 C\, Generali Saal</b> - Templergraben 55\, 6. Etage</p>
 Frauen in Spitzen
 positionen sind immer noch eine Ausnahme. Oftmals wird die berühmte „Gläser
 ne Decke“ als Ursache dafür zitiert. Oben in der Regel die machthabenden Mä
 nner\, unten in der Regel die aufstrebenden Frauen. Was tragen beide Seiten
  dazu bei\, dass die „Gläserne Decke“ immer noch hält? In ihrem Vortrag ent
 larvt Marion Knaths die Spielregeln\, die diese „Gläserne Decke“ immer noch
  bilden und stützen.
 
 Erfahren Sie auf humorvolle und anschauliche Weis
 e mehr über Stereotype und die Spielregeln genderspezifischer Kommunikation
  - und wie Sie dieses Wissen für Ihre eigene Position erfolgreich nutzen kö
 nnen.
 
 <b>Marion Knaths </b>- <a href="http://www.sheboss.de/">www.sheb
 oss.de</a> - gilt als Top-Speaker zum Thema genderspezifische Kommunikation
 . Sie ist Führungskräftetrainerin und Bestsellerautorin des Buches „Spiele 
 mit der Macht“. Marion Knaths coacht und trainiert Frauen in Führungspositi
 onen für viele Top-Unternehmen in Deutschland und Europa.
 
 <b><span sty
 le="text-decoration: underline\;">ANMELDUNG:</span></b> Aus organisatorisch
 en Gründen\, bitten wir Sie\, sich bis zum 22.02 bei <a href="mailto:odile.
 clavery@zhv.rwth-aachen.de">Odile Clavery</a> anzumelden. Vielen Dank!
 

  Wir würden uns besonders freuen\, wenn sich auch zahlreiche Männer zu dies
 em Vortrag anmelden.
 
 &nbsp\;
ORGANIZER:Isabel Jahns
END:VEVENT
BEGIN:VEVENT
UID:20150223T2025Z-1424723124.6201-EO-1551-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20150223T181517Z
LAST-MODIFIED:20150223T181822Z
DTSTART:20150304T170000Z
DTEND:20150304T200000Z
SUMMARY: Kinoabend: The Imitation Game
DESCRIPTION: Wer hat Lust auf Kino? Alle sind herzlich eingeladen mitzukomm
 en! Wir – das ist eine Initiative aus REGINA e.V. und der GI-Regionalgruppe
  Aachen (RIA) &#8211\; haben einen Saal im Apollo-Kino reserviert und gezei
 gt wird: The Imitation Game Am 4. März 2015 &#8230\; <a href="http://www.al
 gosyn.rwth-aachen.de/events/event/kinoabend-the-imitation-game/">Continue r
 eading <span class="meta-nav">&#8594\;</span></a>
X-ALT-DESC;FMTTYPE=text/html: Wer hat Lust auf Kino?
 Alle sind herzlich e
 ingeladen mitzukommen!
 
 Wir – das ist eine Initiative aus REGINA e.V. u
 nd der GI-Regionalgruppe Aachen (RIA) - haben einen Saal im Apollo-Kino res
 erviert und gezeigt wird:
 
 <strong>The Imitation Game</strong>
 Am 4. 
 März 2015 um 18 Uhr
 Im Apollo Kino&Bar\, Pontstraße 141-149\, 52062 Aache
 n
 
 
 Der Film von Morten Tyldum wurde für acht Oscars nominiert. Bened
 ict Cumberbatch spielt den Forscher und britischen Mathematiker Alan Turing
 \, der nicht nur die deutsche Verschlüsselung im Krieg knackte\, sondern au
 ch wegen seiner Homosexualität verfolgt wurde.
 
 Es gibt ein besonderes 
 Bonbon für alle GI-Mitglieder (oder die es bis zum Filmstart geworden sind)
 :
 Reduzierte Kinokarte: 2\,00 €
 
 Aus organisatorischen Grün­den und d
 a die Anzahl der Plätze begrenzt ist\, benötigen wir eine verbindliche Anme
 ldung bis zum 25. Februar 2015 per Email direkt an Helen Bolke Hermanns mit
  der Angabe\, ob eine GI-Mitgliedschaft besteht und man in den Genuss des V
 orzugspreises kommt.
ORGANIZER:Isabel Jahns
END:VEVENT
BEGIN:VEVENT
UID:20150309T1115Z-1425899719.4846-EO-1564-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20150309T110827Z
LAST-MODIFIED:20150309T110945Z
DTSTART:20150309T143000Z
DTEND:20150309T153000Z
SUMMARY: Presentation Arend Rensink
DESCRIPTION: If-Next-Also-Else: Controlling Graph Transformation Abstract: 
 Graph transformation is a declarative\, rule-based formalism. However\, whe
 n using it in practice\, it is convenient to schedule rules explicitly\, an
 d not just rely on their own application conditions\, even though such sche
 duling adds an &#8230\; <a href="http://www.algosyn.rwth-aachen.de/events/e
 vent/presentation-arend-rensink/">Continue reading <span class="meta-nav">&
 #8594\;</span></a>
X-ALT-DESC;FMTTYPE=text/html: <h1>If-Next-Also-Else: Controlling Graph Tran
 sformation</h1>
 Abstract: Graph transformation is a declarative\, rule-ba
 sed formalism. However\, when using it in practice\, it is convenient to sc
 hedule rules explicitly\, and not just rely on their own application condit
 ions\, even though such scheduling adds an imperative flavour. This can be 
 catered for by adding a layer of *control* on top of the rules.
 
 In thi
 s presentation\, I will demonstrate the power of an expressive rule control
  language\, then discuss its semantics. I will argue that the usual\, proce
 ss algebraic concept of operational semantics does not adequately capture t
 he notions of "try-else" and "as-long-as-possible" that are very popular in
  the context of controlled graph transformation\; and I will propose an ext
 ension that replaces CCS-like symmetric choice into a more primitive\, asym
 metric version.
LOCATION:Room 4017 \, Seminarraum i1
GEO:50.778320;6.060860
ORGANIZER:Isabel Jahns
END:VEVENT
BEGIN:VEVENT
UID:20150317T1111Z-1426590684.0471-EO-1568-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20150317T105107Z
LAST-MODIFIED:20150317T105107Z
DTSTART:20150317T130000Z
DTEND:20150317T143000Z
SUMMARY: Seminar: Professor Chris Myers\, University of Utah\, USA
DESCRIPTION: An Integrated Verification Architecture Abstract: Research in 
 formal verification is hampered by a lack of an integrated verification arc
 hitecture. Each verification tool in development typically uses its own lan
 guage for models and properties. This fact means that when a designer &#823
 0\; <a href="http://www.algosyn.rwth-aachen.de/events/event/seminar-profess
 or-chris-myers-university-of-utah-usa/">Continue reading <span class="meta-
 nav">&#8594\;</span></a>
X-ALT-DESC;FMTTYPE=text/html: <h1>An Integrated Verification Architecture</
 h1>
 Abstract:
 Research in formal verification is hampered by a lack of 
 an integrated verification architecture. Each verification tool in developm
 ent typically uses its own language for models and properties. This fact me
 ans that when a designer wants to verify their system using multiple verifi
 cation tools\, it often requires a time-consuming and error-prone recoding 
 of the model. Furthermore\, a system includes both digital and analog hardw
 are\, software\, and a physical operating environment. Each part of the sys
 tem may be better encoded with a different modeling formalism and analyzed 
 using a different methodology. For example\, digital hardware may require a
 ccurate timing\, analog circuits require accurate continuous dynamics\, sof
 tware needs efficient data representation\, and the operating environment m
 ay be stochastic in nature. An integrated verification architecture would e
 nable each part of the system to be represented and analyzed using the appr
 opriate framework. This talk will describe our experiences in verification 
 of heterogeneous systems including asynchronous\, analog/mixed signal\, and
  genetic circuits\, and looking forward to how these methodologies can be u
 nified into an integrated framework.
 
 
LOCATION:Room 4017 \, Seminarraum i1
GEO:50.778320;6.060860
ORGANIZER:Isabel Jahns
END:VEVENT
BEGIN:VEVENT
UID:20150317T1111Z-1426590684.0578-EO-1569-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20150317T110101Z
LAST-MODIFIED:20150317T110101Z
DTSTART:20150324T100000Z
DTEND:20150324T113000Z
SUMMARY: Presentation: Prof. Sriram Sankaranarayanan
DESCRIPTION: Switched Region Stabilization of Polynomial Dynamical Systems 
 Abstract: We consider the problem of automatically synthesizing region stab
 ilizing controllers for polynomial dynamical systems. The goal of our synth
 esis is to produce switching controllers that can switch between finitely m
 any modes to &#8230\; <a href="http://www.algosyn.rwth-aachen.de/events/eve
 nt/presentation-prof-sriram-sankaranarayanan/">Continue reading <span class
 ="meta-nav">&#8594\;</span></a>
X-ALT-DESC;FMTTYPE=text/html: <h1>Switched Region Stabilization of Polynomi
 al Dynamical Systems</h1>
 Abstract: We consider the problem of automatica
 lly synthesizing region stabilizing controllers for polynomial dynamical sy
 stems. The goal of our synthesis is to produce switching controllers that c
 an switch between finitely many modes to ensure that the resulting closed l
 oop dynamics are guaranteed to reach a given small target region around the
  equilibrium (and stay there). Our approach uses the notion of a control Ly
 apunov function\, an extension to standard Lyapunov functions for non-auton
 omous (controlled) systems. We show that a relatively simple modification t
 o the standard control Lyapunov formulation works for the switched system c
 ase\, and yields controllers with guaranteed minimum dwell times\, that can
  be implemented inside a computer. We show how such an implementation can b
 e performed inside a model-predictive control (MPC) scheme.
 
 Next\, we 
 present schemes for automatically discovering control Lyapunov functions by
  reducing the problem to solving a system of quantified constraints over th
 e reals. We examine the solution of these constraints using a procedure cal
 led Counter-Example Guided Inductive Synthesis (CEGIS) driven by nonlinear 
 delta-satisfiability solvers such as dReal\, or through a Linear Matrix Ine
 quality (LMI) relaxation of the nonlinear constraints. We conclude by discu
 ssing the issue of numerical errors in LMI solving and some alternatives in
 volving Bernstein polynomials.
 
 Joint work with Hadi Ravanbakhsh (Unive
 rsity of Colorado\, Boulder) and Amin Ben Sassi (University of Colorado\, B
 oulder)
 
 Bio: Sriram Sankaranarayanan is an assistant professor of Comp
 uter Science at the University of Colorado\, Boulder. His research interest
 s include automatic techniques for reasoning about the behavior of computer
  and cyber-physical systems. Sriram obtained a PhD in 2005 from Stanford Un
 iversity where he was advised by Zohar Manna and Henny Sipma.
 
 Subseque
 ntly he worked as a research staff member at NEC research labs in Princeton
 \, NJ. He has been on the faculty at CU Boulder since 2009. Sriram has been
  the recipient of awards including the President's Gold Medal from IIT Khar
 agpur (2000)\, Siebel Scholarship (2005)\, the CAREER award from NSF (2009)
 \, Dean's award for outstanding junior faculty (2012)\, outstanding teachin
 g (2014)\, and the Provost's faculty achievement award (2014).
LOCATION:Room 9222\, E3
GEO:50.778476;6.059939
ORGANIZER:Isabel Jahns
END:VEVENT
BEGIN:VEVENT
UID:20150320T0951Z-1426845116.9611-EO-1571-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20150320T094753Z
LAST-MODIFIED:20150320T094753Z
DTSTART:20150325T130000Z
DTEND:20150325T143000Z
SUMMARY: Presentation: Prof. Luca Bortolussie (Trieste\, Italy)
DESCRIPTION: Machine Learning meets Formal Verification Abstract: We will d
 iscuss novel applications of state-of-the-art Machine Learning statistical 
 tools to deal with uncertainty in Continuous Time Markov Chains\, combining
  them with classic tools from formal methods\, mainly Model Checking. Uncer
 tain CTMC are &#8230\; <a href="http://www.algosyn.rwth-aachen.de/events/ev
 ent/presentation-prof-luca-bortolussie-trieste-italy/">Continue reading <sp
 an class="meta-nav">&#8594\;</span></a>
X-ALT-DESC;FMTTYPE=text/html: <h1>Machine Learning meets Formal Verificatio
 n</h1>
 
 Abstract: We will discuss novel applications of state-of-the-ar
 t 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 depe
 nd on some fixed parameter\, whose precise value is unknown\, but is assume
 d to lie in a bounded interval. The first problem we face is how to estimat
 e the satisfaction probability of a linear temporal logic property under su
 ch uncertainty. We will show how we can reconstruct the functional dependen
 cy of the satisfaction probability on unknown parameters using Machine Lear
 ning techniques based on Gaussian Processes\, which offer a flexible framew
 ork for regression and classification. We dubbed this approach Smoothed Mod
 el Checking.
 An alternative way to deal with uncertainty is to try to eli
 minate it exploiting available observations of the real system modelled. As
  it is often easier to observe and capture qualitative properties\, rather 
 than performing precise measurements\, we tackled the problem of parameter 
 estimation from observations of truth values of temporal logic formulae.
 
 Also in this case\, Gaussian Processes and Bayesian Optimisation play a cen
 tral role in the solution of this problem.
 In a similar way we can tackle
  the related problem of system design\, which consists in finding optimal p
 arameter values to enforce a certain behaviour. Again\, we consider behavio
 urs specified as linear temporal properties\, combining Bayesian Optimisati
 on with quantitative semantics.
LOCATION:Room 5052
GEO:50.778320;6.060860
ORGANIZER:Isabel Jahns
END:VEVENT
BEGIN:VEVENT
UID:20150327T1311Z-1427461901.7114-EO-1573-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20150327T124328Z
LAST-MODIFIED:20150327T124328Z
DTSTART:20150325T150000Z
DTEND:20150325T163000Z
SUMMARY: Presentation: Roberta Lanciani
DESCRIPTION: Stochastic Approximations and Verifications In this talk\, we 
 discuss the use of stochastic approximations to validate properties of Mark
 ov population models. This type of Markovian models are used to describe th
 e evolution of large systems of interacting entities\, and their &#8230\; <
 a href="http://www.algosyn.rwth-aachen.de/events/event/presentation-roberta
 -lanciani/">Continue reading <span class="meta-nav">&#8594\;</span></a>
X-ALT-DESC;FMTTYPE=text/html: <h1>Stochastic Approximations and Verificatio
 ns</h1>
 In this talk\, we discuss the use of stochastic approximations to
  validate properties of Markov population models. This type of Markovian mo
 dels are used to describe the evolution of large systems of interacting ent
 ities\, and their verification\, using standard stochastic model checking t
 echniques\, is ampered by the large number of possible behavious of the age
 nts in the population\, which leads to the well known curse of the state sp
 ace explosion. To tackle this problem\, we define new model checking proced
 ures based on different types of stochastic approximations\, namely the Flu
 id\, the Central Limit and the Higher Orders Approximations\, which can be 
 used to accurately and efficiently extimate the evolution of large populati
 on models. In this talk\, we introduce these model checking techniques\, re
 viewing the type of properties that can be verified\, the definition of the
  stochastic approximations\, and some results obtained on a simple epidemic
  model.
ORGANIZER:Isabel Jahns
END:VEVENT
BEGIN:VEVENT
UID:20150320T0951Z-1426845116.9721-EO-1572-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20150320T095005Z
LAST-MODIFIED:20150320T095038Z
DTSTART:20150326T090000Z
DTEND:20150326T103000Z
SUMMARY: Presentation: Nils Jansen
DESCRIPTION: Counterexamples in Probabilistic Verification The topic of thi
 s thesis is roughly to be classified into the formal verification of probab
 ilistic systems. In particular\, the generation of counterexamples for disc
 rete-time Markov Models is investigated. A counterexample for discrete-time
  Markov Chains (DTMCs) &#8230\; <a href="http://www.algosyn.rwth-aachen.de/
 events/event/presentation-nils-jansen/">Continue reading <span class="meta-
 nav">&#8594\;</span></a>
X-ALT-DESC;FMTTYPE=text/html: <h1>Counterexamples in Probabilistic Verifica
 tion</h1>
 
 The topic of this thesis is roughly to be classified into th
 e formal verification of probabilistic systems. In particular\, the generat
 ion of counterexamples for discrete-time Markov Models is investigated. A c
 ounterexample for discrete-time Markov Chains (DTMCs) is classically define
 d as a (finite) set of paths. In this work\, this set of paths is represent
 ed symbolically as a critical part of the original system\, a so-called cri
 tical subsystem. This notion is extended to Markov decision processes (MDPs
 ) and probabilistic automata (PAs). The results are introduced in four part
 s:
 
 1. A model checking algorithm for DTMCs based on a decomposition of
  the system’s graph in strongly connected components (SCCs). This approach 
 is extended to parametric discrete-time Markov Chains.
 
 2. The generati
 on of counterexamples for DTMCs and reachability properties based on graph 
 algorithms. A hierarchical abstraction scheme to compute abstract counterex
 amples is presented\, followed by a general framework for both explicitly r
 epresented systems and symbolically represented systems using binary decisi
 on diagrams (BDDs).
 
 3. The computation of minimal critical subsystems 
 using SAT modulo theories (SMT) solving and mixed integer linear programmin
 g (MILP). This is investigated for reachability properties and ω-regular pr
 operties on DTMCs\, MDPs\, and PAs.
 
 4. A new concept of high-level cou
 nterexamples for PAs. Markov models can be specified by means of a probabil
 istic programming language. An approach for computing critical parts of suc
 h a symbolic description of a system is presented\, yielding human-readable
  counterexamples.
 
 All results have been published in conference procee
 dings or journals. A thorough evaluation on common benchmarks is given comp
 aring all methods and also competing with available implementations of othe
 r approaches.
LOCATION:Room 9222\, E3
GEO:50.778476;6.059939
ORGANIZER:Isabel Jahns
END:VEVENT
BEGIN:VEVENT
UID:20150423T0925Z-1429781105.1379-EO-1575-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20150423T090046Z
LAST-MODIFIED:20150423T090046Z
DTSTART:20150422T080000Z
DTEND:20150423T093000Z
SUMMARY: Prof. Lijun Zhang: Polynomial Quantitative Loop Invariants by Lagr
 ange Interpolation
DESCRIPTION: Polynomial Quantitative Loop Invariants by Lagrange Interpolat
 ion &#160\; Abstract: We apply multivariate Lagrange interpolation to synth
 esizing polynomial quantitative loop invariants for probabilistic programs.
  Lagrange interpolation allows to find better constraints for unknown loop 
 invariants. Random sampling furthermore generates constraints to &#8230\; <
 a href="http://www.algosyn.rwth-aachen.de/events/event/prof-lijun-zhang-pol
 ynomial-quantitative-loop-invariants-by-lagrange-interpolation/">Continue r
 eading <span class="meta-nav">&#8594\;</span></a>
X-ALT-DESC;FMTTYPE=text/html: Polynomial Quantitative Loop Invariants by La
 grange Interpolation
 
 &nbsp\;
 
 Abstract:
 
 We apply multivariate
  Lagrange interpolation to synthesizing polynomial quantitative loop invari
 ants for probabilistic programs. Lagrange interpolation allows to find bett
 er constraints for unknown loop invariants. Random sampling furthermore gen
 erates constraints to pin- point quantitative invariants. We evaluate our t
 echnique by several case studies with polynomial quantitative loop invarian
 ts in the experiments.
ORGANIZER:Helen Bolke-Hermanns
END:VEVENT
BEGIN:VEVENT
UID:20150423T0955Z-1429782905.1681-EO-1576-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20150423T091448Z
LAST-MODIFIED:20150423T095201Z
DTSTART:20150423T091400Z
DTEND:20150423T101400Z
SUMMARY: Deni Raco: Umsetzung der formalen Entwicklungsmethodik FOCUS in de
 m Theorembeweiser Isabelle zur Verifikation verteilter Systeme
X-ALT-DESC;FMTTYPE=text/html: 
ORGANIZER:Helen Bolke-Hermanns
END:VEVENT
BEGIN:VEVENT
UID:20150317T1041Z-1426588883.9491-EO-1566-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20150317T103037Z
LAST-MODIFIED:20150317T103728Z
DTSTART;VALUE=DATE:20150506
DTEND;VALUE=DATE:20150510
SUMMARY: AutoMathA 2015
DESCRIPTION: Jewels of Automata: from Mathematics to Applications Leipzig\,
  May 6-9\, 2015 The conference AutoMathA 2015 will survey a wide picture of
  research in automata theory and related mathematical fields. It will consi
 st of 26 invited lectures which will describe significant &#8230\; <a href=
 "http://www.algosyn.rwth-aachen.de/events/event/automatha-2015/">Continue r
 eading <span class="meta-nav">&#8594\;</span></a>
X-ALT-DESC;FMTTYPE=text/html: <h1>Jewels of Automata: from Mathematics to A
 pplications</h1>
 <strong>Leipzig\, May 6-9\, 2015</strong>
 
 The confe
 rence AutoMathA 2015 will survey a wide picture of research in automata the
 ory 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 senior researchers to learn and to disc
 uss about automata theory\, its connections with mathematics and its applic
 ations.
 
 For young researchers the conference will serve as an "Advance
 d Spring School of Automata Theory".
 
 This event is a follow-up of the 
 multidisciplinary programme Automata: from Mathematics to Applications (Aut
 oMathA\, 2005--2010) of the European Science Foundation and of its final co
 nference "Highlights of AutoMathA" in Vienna 2010.
 
 <a href="http://www
 .automatha.uni-leipzig.de">Website</a>
 
 <strong>Invited speakers</stron
 g>
 Jean-Paul Allouche (Paris)
 Mikołaj Bojańczyk (Warsaw)
 Patricia Bou
 yer-Decitre (Cachan)
 Thomas Brihaye (Mons)
 Olivier Carton (Paris)
 Tho
 mas Colcombet (Paris)
 Volker Diekert (Stuttgart)
 Michael Elberfeld (Aac
 hen)
 Uli Fahrenberg (Rennes)
 Nathanaël Fijalkow (Paris)
 Paul Gastin (
 Cachan)
 Artur Jeż (Saarbrücken)
 Ines Klimann (Paris)
 Dexter Kozen (It
 haca)
 Dietrich Kuske (Ilmenau)
 Kim Larsen (Aalborg)
 Ranko Lazic (Warw
 ick)
 Markus Lohrey (Siegen)
 Cyril Nicaud (Marne-la-Vallée)
 Igor Potap
 ov (Liverpool)
 Jacques Sakarovitch (Paris)
 Thomas Schwentick (Dortmund)
 
 Marinella Sciortino (Palermo)
 Ludwig Staiger (Halle)
 Moshe Vardi (Ho
 uston)
 James Worrell (Oxford)
 
 <strong>Program Committee</strong>
 J
 orge Almeida (Porto)
 Véronique Bruyère (Mons)
 Manfred Droste (Leipzig)

 
 Sören Eilers (Copenhagen)
 Zoltan Esik (Szeged)
 Marcin Jurdzinski (War
 wick)
 Juhani Karhumäki (Turku)
 Werner Kuich (Wien)
 Filippo Mignosi (A
 quila)
 Damian Niwinski (Warsaw)
 Jean-Eric Pin (Paris)
 Olivier Serre (
 Paris)
 Jeffrey Shallit (Waterloo)
 Wolfgang Thomas (Aachen)
 Mikhail Vo
 lkov (Ekaterinburg)
 Igor Walukiewicz (Bordeaux)
 Thomas Wilke (Kiel)
 

 
 <strong>Registration</strong>
 Due to support by the German Research Fou
 ndation (DFG)\, this conference is *fee-free*.
 
 However\, registration 
 is mandatory for participation.
 Please send your name\, affiliation and i
 ntended length of stay to:
 automatha@informatik.uni-leipzig.de
 
 Deadl
 ine for registration: March 15\, 2015
 
 <strong>Contact</strong>
 <a hr
 ef="mailto:droste@informatik.uni-leipzig.de">Manfred Droste</a> or
 <a hre
 f="mailto:kuich@tuwien.ac.at">Werner Kuich</a> or
 <a href="mailto:Jean-Er
 ic.Pin@liafa.univ-paris-diderot.fr">Jean-Éric Pin</a> or
 <a href="mailto:
 thomas@automata.rwth-aachen.de">Wolfgang Thomas</a>
ORGANIZER:Isabel Jahns
END:VEVENT
BEGIN:VEVENT
UID:20160106T1443Z-1452091413.0784-EO-25692-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20150511T133120Z
LAST-MODIFIED:20160107T091904Z
DTSTART:20150513T120000Z
DTEND:20150513T150000Z
SUMMARY: Simon Lessenich: Counting Logics and Games with Counters
DESCRIPTION: Referent: Dipl.-Inform. Simon Lessenich Titel: Counting Logics
  and Games with Counters Abstract: In verification and synthesis\, properti
 es or models of interest are often quantitative\, and many quantitative asp
 ects involve counting. For example\, one might be interested in the amount 
 of &#8230\; <a href="http://www.algosyn.rwth-aachen.de/events/event/informa
 tik-oberseminar-lessenich/">Continue reading <span class="meta-nav">&#8594\
 ;</span></a>
X-ALT-DESC;FMTTYPE=text/html: Referent: Dipl.-Inform. Simon Lessenich
 
 
 <strong>Titel: Counting Logics and Games with Counters</strong>
 
 Abstra
 ct:
 In verification and synthesis\, properties or models of interest are 
 often quantitative\, and many quantitative aspects involve counting. For ex
 ample\, one might be interested in the amount of memory required by a syste
 m\, how many simultaneous requests a system has to process along a run\, or
  how many infixes belonging to some regular language a word contains. In th
 is talk\, we present two quantitative counting logics and two models of gam
 es with counter. We first study Qmu[#MSO]\, a counting logic based on the q
 uantitative mu-calculus. This logic is designed specifically for transition
  systems where the states are labeled with finite relational structures. Co
 unting is introduced to Qmu with the help of counting terms of monadic seco
 nd-order logic\, which are evaluated on the relational structures the state
 s are labeled with. We prove that the model-checking problem for Qmu[#MSO] 
 on a generalization of pushdown systems is reducible to solving finite coun
 ter parity games. We then present the model of counter parity games\, which
  are quantitative games in which a finite set of counters is updated along 
 the edges. Payoffs of finite plays are obtained via the counters\, while pa
 yoffs of infinite plays are determined via a parity condition. We show that
  finite counter parity games are effectively solvable\, using games with im
 perfect recall to solve the unboundedness problem for the value. Thus\, it 
 follows that the above model-checking problem for Qmu[#MSO] is decidable. I
 n the last part of the talk\, we discuss a quantitative counting extension 
 of monadic second-order logic called qcMSO and a model of games with counte
 rs where payoffs are obtained via a mean-payoff objective on a special coun
 ter.
 
 Es laden ein: Die Dozenten der Informatik
 
 &nbsp\;
LOCATION:Raum 9U09
GEO:49.529050;9.619220
ORGANIZER:marius voelkel
END:VEVENT
BEGIN:VEVENT
UID:20150505T0833Z-1430814792.3314-EO-1578-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20150505T081457Z
LAST-MODIFIED:20150505T081457Z
DTSTART:20150520T080000Z
DTEND:20150520T093000Z
SUMMARY: Presentation Christian Meirich
X-ALT-DESC;FMTTYPE=text/html: 
LOCATION:Room 5052
GEO:50.778320;6.060860
ORGANIZER:Helen Bolke-Hermanns
END:VEVENT
BEGIN:VEVENT
UID:20150512T1148Z-1431431316.8925-EO-1579-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20150512T112105Z
LAST-MODIFIED:20150512T112105Z
DTSTART:20150520T081500Z
DTEND:20150520T094500Z
SUMMARY: Presentation: Christian Meirich
DESCRIPTION: Optimization of Railway-networks The background of this talk i
 s the motivation to optimize the capacitive load in the field of railway op
 eration research. Especially there are approaches of the strategic network 
 planning in the field of the (German) Federal Transport &#8230\; <a href="h
 ttp://www.algosyn.rwth-aachen.de/events/event/presentation-christian-meiric
 h-3/">Continue reading <span class="meta-nav">&#8594\;</span></a>
X-ALT-DESC;FMTTYPE=text/html: <h1>Optimization of Railway-networks </h1>
 
 The background of this talk is the motivation to optimize the capacitive lo
 ad in the field of railway operation research. Especially there are approac
 hes of the strategic network planning in the field of the (German) Federal 
 Transport Infrastructure Plan. A plan like this is a comprehensive compilat
 ion of the German government for investments in the infrastructure for seve
 ral carriers of traffic. Main topics are generation and restraint of traffi
 c or a detection of bottlenecks. This talk is going to provide an approach 
 for an optimization in railway-networks. For this approach the capacity for
  each railway line and each railway node is going to be used as an input va
 riable. A state of needed capacity depends on the mix ratio of train runs o
 n each infrastructure segment. Due to a rerouting of trains towards the opt
 imization\, the (new) mix ratio of trains must be checked. 
LOCATION:Room 5052
GEO:50.778320;6.060860
ORGANIZER:Isabel Jahns
END:VEVENT
BEGIN:VEVENT
UID:20150609T0958Z-1433843918.6527-EO-1586-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20150609T093024Z
LAST-MODIFIED:20150612T101113Z
DTSTART;VALUE=DATE:20150617
DTEND;VALUE=DATE:20150618
SUMMARY: Abschlussveranstaltung Graduiertenkolleg AlgoSyn
DESCRIPTION: Abschlussveranstaltung Graduiertenkolleg AlgoSyn       10.00 B
 egrüßung 10.15 Präsentation Rückblick auf 9 Jahre AlgoSyn 11.00 Vortrag Sas
 cha Geulen: Learning-based Control Strategies for Hybrid Electric Vehicles 
 12.00 Vortrag Johanna Nellen: simulation results of learning-based control 
 strategies 13.00 Mittagspause 13.30 Koordination der Abschlussarbeiten und 
 &#8230\; <a href="http://www.algosyn.rwth-aachen.de/events/event/presentati
 on-johanna-nellen-and-sascha-geulen/">Continue reading <span class="meta-na
 v">&#8594\;</span></a>
X-ALT-DESC;FMTTYPE=text/html: <i><strong>Abschlussveranstaltung Graduierten
 kolleg AlgoSyn     </strong> </i>
 
 <i> 10.00 Begrüßung</i>
 
 <i>10.1
 5 Präsentation Rückblick auf 9 Jahre AlgoSyn </i>
 
 <i>11.00 Vortrag Sas
 cha Geulen: Learning-based Control Strategies for Hybrid Electric Vehicles

 
 </i>
 
 <i>12.00 Vortrag Johanna Nellen: simulation results of learning
 -based control strategies
 </i>
 
 <i>13.00 Mittagspause</i>
 
 <i>13.
 30 Koordination der Abschlussarbeiten und Einteilung der Untergruppen </i>

 
 
 <i>14.15 Das GK-intere Projekt „Scientific Life“</i>
 
 <i>14.45 Prä
 sentation „Das Modell Graduiertenkolleg als Erfolgsformat für strukturierte
  Promotionen“</i>
 
 <i>15.15 Abschließende Worte durch den Sprecher Prof
 . Dr. Wolfgang Thomas</i>
 
 <i>15.30 Ausklang</i>
 
 &nbsp\;
 
LOCATION:Room 9222\, E3
GEO:50.778476;6.059939
ORGANIZER:Isabel Jahns
END:VEVENT
BEGIN:VEVENT
UID:20150609T0928Z-1433842118.5918-EO-1585-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20150609T092259Z
LAST-MODIFIED:20150609T092259Z
DTSTART:20150619T130000Z
DTEND:20150619T143000Z
SUMMARY: Presentation: Rupak Majumdar
DESCRIPTION: Algorithmic Formal Methods in Continuous Control Abstract: Alg
 orithmic formal methods such as model checking and reactive synthesis were 
 originally developed in the context of discrete systems such as hardware ci
 rcuits and software. Over the last few years\, these techniques have &#8230
 \; <a href="http://www.algosyn.rwth-aachen.de/events/event/presentation-rup
 ak-majumdar/">Continue reading <span class="meta-nav">&#8594\;</span></a>
X-ALT-DESC;FMTTYPE=text/html: <h1>Algorithmic Formal Methods in Continuous 
 Control</h1>
 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 developm
 ent of high assurance cyber-physical systems\, in which discrete components
  interact with continuous physical systems. I will survey some recent resul
 ts applying formal methods to continuous systems\, pointing out how notions
  such as invariants\, variants\, bisimulation\, and trace equivalence can b
 e adapted in the context of continuous systems. Specifically\, I will show 
 two examples of theoretical ideas from formal methods applied to continuous
  control: a deductive system for controller synthesis for continuous system
 s against temporal specifications\, and a semi-formal conformance testing p
 rocedure based on a metric generalization of trace equivalence. I will conc
 lude with some current challenges in the area.
 [Joint work with Jyo Deshm
 ukh\, Rayna Dimitrova\, and Vinayak Prabhu]
LOCATION:Room 9222\, E3
GEO:50.778476;6.059939
ORGANIZER:Isabel Jahns
END:VEVENT
BEGIN:VEVENT
UID:20150826T0803Z-1440576219.4159-EO-6078-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20150826T073629Z
LAST-MODIFIED:20150826T073639Z
DTSTART:20150908T110000Z
DTEND:20150908T123000Z
SUMMARY: Dr. Jan Oliver Ringert\,  Tel Aviv University\, Israel:On Challeng
 es in Reactive Synthesis for Software Engineers:  Support for LTL Specifica
 tion Patterns and a Case Study
DESCRIPTION: Reactive synthesis is an automated procedure to obtain a corre
 ct-by-construction reactive system from a given specification. Despite rece
 nt advancements on the theory and algorithms of reactive synthesis\, many c
 hallenges remain in bringing reactive synthesis technologies to the hands o
 f software &#8230\; <a href="http://www.algosyn.rwth-aachen.de/events/event
 /dr-jan-oliver-ringert-tel-aviv-university-israelon-challenges-in-reactive-
 synthesis-for-software-engineers-support-for-ltl-specification-patterns-and
 -a-case-study/">Continue reading <span class="meta-nav">&#8594\;</span></a>
X-ALT-DESC;FMTTYPE=text/html: Reactive synthesis is an automated procedure 
 to obtain a correct-by-construction reactive system from a given specificat
 ion. Despite recent advancements on the theory and algorithms of reactive s
 ynthesis\, many challenges remain in bringing reactive synthesis technologi
 es to the hands of software engineers. GR(1) is a well-known fragment of li
 near temporal logic introduced by Piterman et al. where synthesis is possib
 le using a polynomial symbolic algorithm. One challenge in making the GR(1)
  fragment useful for software engineers is its restricted syntax.
 Further
  challenges relate to the change from writing code to writing specification
 s\, and the development of tools to support a specification-centric rather 
 than a code-centric development process. We report on our work in progress 
 to investigate whether the well-known high-level specification patterns ide
 ntified by Dwyer et al.\, which are common in industrial specifications and
  make writing specifications easier\, can be supported in GR(1) synthesis. 
 Specifically\, we show that 52 out of the 55 patterns of Dwyer et al. can b
 e supported\, and present an automated\, sound and complete translation of 
 supported patterns to the GR(1) form\, which effectively results in a catal
 ogue and an efficient reactive synthesis procedure for any specification th
 at is written using the patterns. Next\, we report  on a case study we have
  conducted to learn about the challenges of using GR(1) synthesis in the de
 velopment of a reactive robotic system.
 In the case study we developed a 
 specification of a forklift controller\, deployed on a Lego robot. The case
  study employs LTL specification patterns as an extension of the GR(1) spec
 ification language and an examination of two specification variants for exe
 cution scheduling. We present the specifications we developed\, our observa
 tions\, and challenges faced during the case study. Joint work with Shahar 
 Maoz.
 
 Supported by ERC StG SYNTECH.
 S. Maoz and J. O. Ringert. GR(1)
  Synthesis for LTL Specification Patterns. Proc. of ESEC/FSE 2015\, ACM.
 
 
 S. Maoz and J. O. Ringert. Synthesizing a Lego Forklift Controller in GR
 (1): A Case Study. SYNT 2015: 4th Workshop on Synthesis (with CAV).
ORGANIZER:Helen Bolke-Hermanns
END:VEVENT
BEGIN:VEVENT
UID:20160106T1443Z-1452091413.0905-EO-25693-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20150924T133236Z
LAST-MODIFIED:20160107T091745Z
DTSTART:20150925T080000Z
DTEND:20150925T130000Z
SUMMARY: Friedrich Gretz: Semantics and Loop Invariant Synthesis for Probab
 ilistic Programs
DESCRIPTION: Referent: Dipl.-Inform. Friedrich Gretz Titel: Semantics and L
 oop Invariant Synthesis for Probabilistic Programs Abstract: In this thesis
  we consider sequential probabilistic programs. Such programs are a means t
 o model randomised algorithms in computer science. They facilitate the form
 al analysis of &#8230\; <a href="http://www.algosyn.rwth-aachen.de/events/e
 vent/informatik-oberseminar-gretz/">Continue reading <span class="meta-nav"
 >&#8594\;</span></a>
X-ALT-DESC;FMTTYPE=text/html: Referent: Dipl.-Inform. Friedrich Gretz
 
 
 <strong>Titel: Semantics and Loop Invariant Synthesis for Probabilistic Pro
 grams</strong>
 
 Abstract:
 In this thesis we consider sequential proba
 bilistic programs. Such programs are a means to model randomised algorithms
  in computer science. They facilitate the formal analysis of performance an
 d correctness of algorithms or security aspects of protocols. We develop an
  operational semantics for probabilistic programs and show it to be equival
 ent to the expectation transformer semantics due to McIver and Morgan. This
  connection between the two kinds of semantics provides a deeper understand
 ing of the behaviour of probabilistic programs and is instrumental to trans
 fer results between communities that use transition systems such as Markov 
 decision processes to reason about probabilistic behaviour and communities 
 that focus on deductive verification techniques based on expectation transf
 ormers. As a next step\, we add the concept of observations and extend both
  semantics to facilitate the calculation of expectations which are conditio
 ned on the fact that no observation is violated during the program’s execut
 ion. Our main contribution here is to explore issues that arise with non-te
 rminating\, non-deterministic or infeasible programs and provide semantics 
 that are generally applicable. Additionally\, we discuss several program tr
 ansformations to facilitate the understanding of conditioning in probabilis
 tic programming. In the last part of the thesis we turn our attention to th
 e automated verification of probabilistic programs. We are interested in au
 tomating inductive verification techniques. As usual the main obstacle in p
 rogram analysis are loops which require either the calculation of fixed poi
 nts or the generation of inductive invariants for their analysis. This task
 \, which is already hard for standard\, i.e. non-probabilistic\, programs\,
  becomes even more challenging as our reasoning becomes quantitative. We fo
 cus on a technique to generate quantitative loop invariants from user defin
 ed templates. This approach is implemented in a software tool called Prinsy
 s and evaluated on several examples.
 
 Es laden ein: Die Dozenten der In
 formatik
LOCATION:Room 9222\, E3
GEO:50.778476;6.059939
ORGANIZER:marius voelkel
END:VEVENT
BEGIN:VEVENT
UID:20160106T1443Z-1452091413.0652-EO-25691-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20160106T143003Z
LAST-MODIFIED:20160106T145054Z
DTSTART:20160126T090000Z
DTEND:20160126T140000Z
SUMMARY: Ibtissem Ben Makhlouf: Comparative Evaluation and Improvement of C
 omputational Approaches to Reachability Analysis of Linear Hybrid Systems
DESCRIPTION: Referent: Dipl.-Inform. Ibtissem Ben Makhlouf Titel: Comparati
 ve Evaluation and Improvement of Computational Approaches to Reachability A
 nalysis of Linear Hybrid Systems Abstract: Hybrid systems combine discrete 
 events and continuous behaviors in the same framework. The discrete part is
  represented as transitions between &#8230\; <a href="http://www.algosyn.rw
 th-aachen.de/events/event/informatik-oberseminar-makhlouf/">Continue readin
 g <span class="meta-nav">&#8594\;</span></a>
X-ALT-DESC;FMTTYPE=text/html: Referent: Dipl.-Inform. Ibtissem Ben Makhlouf
 
 
 <strong>Titel: Comparative Evaluation and Improvement of Computationa
 l Approaches to Reachability Analysis of Linear Hybrid Systems</strong>
 

 
 Abstract:
 Hybrid systems combine discrete events and continuous behavio
 rs in the same framework. The discrete part is represented as transitions b
 etween locations\, in which the continuous part is described as a different
 ial equation and that generally in a confined invariant domain. The transit
 ions are commonly triggered if the corresponding guard conditions are fulfi
 lled. After an eventually reset condition\, the hybrid automaton springs to
  the next location if its invariant condition is also met. The reachability
  analysis consists in computing all states reached by a hybrid automaton st
 arting with an initial set. We focused in this work on techniques combining
  set mapping theory and geometric set approximations to compute an over-app
 roximation of the reachable sets. Our work began with an exhaustive evaluat
 ion and comparison of already available tools. For this purpose a suite of 
 benchmarks has been collected. Based on the results of this study\, we deci
 ded to implement first the technique using zonotopes as approximating sets.
  Diverse techniques for handling guard conditions described as hyperplanes\
 , halfspaces and polyhedra were considered. We therefore performed a perfor
 mance comparison of different intersection methods. In addition\, we compar
 ed them in combination with many clustering approaches for dealing with the
  bundle of intersecting sets in transitions. In a further step\, we impleme
 nted the support function based techniques in a toolbox allowing users the 
 choice between different approximation methods for the initial set\, the in
 put contribution\, optimization solvers as well as different algorithms for
  computing intersections between reachable sets\, guards and invariants. Th
 is toolbox allows users to configure the reachability analysis by combining
  different available options. In particular\, it offers the possibility to 
 compare their performance and to change the choice if the already chosen me
 thod or optimization solver fails. We finally demonstrated potential applic
 ations of the reachability analysis using a networked platoon of vehicles a
 s case study. We first carried out a reachability analysis to determine the
  shortest safe gaps between vehicles in a platoon controlled using Linear M
 atrix Inequalities. We showed then how reachability can help by the choice 
 of the best performing platoon controller. The controllers were computed us
 ing H2 or H∞ optimal control design. Afterwards\, we considered a platoon a
 pproaching an intersection as application to demonstrate how time and state
  critical conditions can be determined using reachability analysis. These c
 onditions are decisive for a safe and reliable management of the intersecti
 on.
 
 Es laden ein: Die Dozenten der Informatik
LOCATION:Room 9220
GEO:50.778476;6.059939
ORGANIZER:marius voelkel
END:VEVENT
BEGIN:VEVENT
UID:20160202T1001Z-1454407284.3452-EO-27781-1@137.226.35.140
STATUS:CONFIRMED
DTSTAMP:20160219T125452Z
CREATED:20160202T094846Z
LAST-MODIFIED:20160202T123130Z
DTSTART:20160204T081500Z
DTEND:20160204T110000Z
SUMMARY: Oliver Göbel: Online Resource Allocation on Stochastic Input Model
 s
DESCRIPTION: Referent: Dipl.-Inform. Oliver Göbel Titel: Online Resource Al
 location on Stochastic Input Models Abstract: The characteristic of online 
 algorithms is that the input is not given at once but it is revealed stepwi
 se in rounds. An online algorithm must make irrevocable decisions upon &#82
 30\; <a href="http://www.algosyn.rwth-aachen.de/events/event/oliver-gobel-o
 nline-resource-allocation-on-stochastic-input-models/">Continue reading <sp
 an class="meta-nav">&#8594\;</span></a>
X-ALT-DESC;FMTTYPE=text/html: Referent: Dipl.-Inform. Oliver Göbel
 
 <st
 rong>Titel: Online Resource Allocation on Stochastic Input Models</strong>

 
 
 Abstract:
 
 The characteristic of online algorithms is that the inp
 ut is not given at once but it is revealed stepwise in rounds. An online al
 gorithm must make irrevocable decisions upon the arrival of each input requ
 est and thus before the entire input is known. As these decisions are made 
 under uncertainty about future requests\, they may turn out as not optimal 
 in the end. The established method is to analyze online algorithms under wo
 rst-case assumptions in terms of the competitive ratio. This is the relatio
 n of the optimal solution and the worst output of the online algorithm. For
  many online combinatorial optimization problems\, however\, there exist lo
 wer bounds which indicate that no online algorithms with non-trivial compet
 itive ratio can be derived when all assumptions are worst-case. To cope wit
 h these optimization problems in a less restrictive and more realistic way\
 , it is promising to relax various worst-case assumptions via including sto
 chastic components into the model. As a consequence\, several stochastic in
 put models exist. They all ease single worst-case assumptions\, but all in 
 a different manner: where one model assumes a stochastic arrival of a worst
 -case input\, another lets the input be stochastically but revealed in wors
 t-case order. We continue with this approach and consider online optimizati
 on problems with stochastic inputs in this thesis. To this end\, we do neit
 her focus on one single optimization problem nor on one single input model.
 
 
 Instead\, we introduce a new unifying input model that allows us to b
 ridge between several input models\, and we consider different problems the
 n. The first algorithm we design considers the online independent set probl
 em\, where the nodes of a graph arrive one after another and an edge appear
 s when both nodes have been revealed. Our algorithm achieves a constant com
 petitive factor. For the weighted problem statement\, we can give a Ο(log n
 ) competitive algorithm and complement this result by a lower bound showing
  that our algorithm is almost optimal. Possible applications of the indepen
 dent set problem can be found in scheduling when a subset of jobs needs to 
 be selected. Other problems in scheduling aim at sorting the jobs according
  to their significance. One of these settings is the online appointment sch
 eduling problem\, where the aim is to order online incoming jobs such that 
 the weighted completion time is minimized. We also derive constant and Ο(lo
 g n)-competitive algorithms for different variants of this problem. Since t
 he minimization objective does not allow to apply the unifying model immedi
 ately\, we first consider the problem in the random-order model and draw co
 nnections to the other input models afterwards. In the secretary leasing pr
 oblem that we investigate in the last chapter of this thesis\, it is necess
 ary to consider the problem over time. In the problem statements described 
 so far\, the input was revealed stepwise and the constraints were with resp
 ect to the global instance. This is significantly different in the secretar
 y leasing problem\, since there exist additional constraints regarding also
  the rounds where the input appears in. Among other results\, we present a 
 constant competitive online algorithm for this problem.
 
 Es laden ein: 
 Die Dozenten der Informatik
LOCATION:Room 4017 \, Seminarraum i1
GEO:50.778320;6.060860
ORGANIZER:marius voelkel
END:VEVENT
END:VCALENDAR