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\, …\; Continue reading →\;
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 here.
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 –\; 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?!
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 …\; Continue reading <
span class="meta-nav">→\;
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.
Schedule
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 –\; 25th\, associated w
ith SAGT 2013) \; Part A: Algorithmic Game Theory\, Mechanism Design\,
Auction Systems Lectures on Computational Complexity in Games and Auctions
by Constantinos Daskalakis (Massachusetts Institute of Technology) Lecture
s on Linear programming and …\; Continue reading →\;
X-ALT-DESC;FMTTYPE=text/html:
 \;
Part
A: Algorithmic Game Theory\, Mechanism Design\, Auction Systems
 \;
 \;
Part B: Games and Software Synthesis\, Automata and Learning\, Softwar
e Verification
Re
gister and more information: here
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’\;s Modal mu-Calculus\, designed for expressing properties of pr
obabilistic-nondeterministic transition systems. Two type of semantics can
be defined for these logics: …\; Continue reading →\;
X-ALT-DESC;FMTTYPE=text/html: First Talk: Game Semantics for Probab
ilistic mu-Calculi
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 ̶
0\;Upper-Expectation bisimilarity”\; …\; Continue readin
g →\;
X-ALT-DESC;FMTTYPE=text/html: Second Talk: Semantic Foundations of
Quantitative (real-valued) Logics based on Functional Analysis
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. …\;
Continue reading →\;
X-ALT-DESC;FMTTYPE=text/html: Abstract:
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>
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 …\;
Continue reading →\;
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 “\;Mechanisms of scientific life”\;
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) …\; Continue reading →\;
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
 \;
1 Adressen
Ho
tel Acora\, www.acora.de
Westpreußenstraße 20-30
D-53119 Bonn
T
el.: +49 (0) 228 / 66 86-0
E-Mail: bonn@ac
ora.de
Arithmeum
Lennéstrasse 2\, 53113 Bonn\, Tel: 02 28 - 7
3 87 90
Öffnungszeiten: Dienstag - Sonntag\, 11:00 - 18:00
 \;
B-IT Zentrum
Dahlmannstraße 2\, 53113 Bonn
 \;
Risto
rante - Pizzeria "Tuscolo"
Kaiser-Karl-Ring 63
53111 Bonn
0228
694665
www.tuscolo.de
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: “\;Synthesizing Structured Reactive Pro
grams: How Much Memory Do They Need?”\;. Abstract: Existing approaches
to the synthesis of controllers in reactive systems typically involve the
construction of transition systems such as Mealy automata. In 2011\, Madhus
udan proposed structured programs …\; Continue reading →\;
X-ALT-DESC;FMTTYPE=text/html: Be
nedikt Brütsch: "S
ynthesizing Structured Reactive Programs: How Much Memory Do They Need?".
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.
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. “\;Synthesizing Structured Reactive Programs: How Muc
h Memory Do They Need?”\;. 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 R
30\; Continue reading →\;
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.
 \;
 \;
The Railway Signalling Lab of RWTH Aachen University
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.
Interlocking
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.
Operation
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 …\; Continue reading →\;
X-ALT-DESC;FMTTYPE=text/html: 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.
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 …\; Continue reading →\;
X-ALT-DESC;FMTTYPE=text/html:
Ibtissem Ben Makhlouf: Reachability Analysis of Hybrid Systems Using Geomet
ric Approximations
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.
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.
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.
Sarah Winter: Synthesis
of Deterministic Top-down Tree Transducers from Automatic Tree Relations
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.
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.
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 \; 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 …\; Continue reading <
span class="meta-nav">→\;
X-ALT-DESC;FMTTYPE=text/html: Generating Inductive Predicates for Symbolic
Execution of Pointer-Manipulating Programs
 \;
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.
 \;
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 …\; Continue
reading →\;
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\; Continue reading →\;
X-ALT-DESC;FMTTYPE=text/html: Johanna Nellen: A CEGAR Approach for the R
eachability Analysis of Sequential Function Charts
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 “\;design+verify”\; approach to “\;specify+synt
hesize”\; in model-based engineering. I then discuss our …\; Continue reading →\;
X-ALT-DESC;FMTTYPE=text/html: Ufuk Topcu: Correct-By-Construction Contro
l Synthesis for Autonomous Systems
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 –\; 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 …\; Con
tinue reading →\;
X-ALT-DESC;FMTTYPE=text/html: Präsentation von Christian Meirich: Erhöhu
ng der Leistungsfähigkeit durch eine optimale Ausnutzung von Kapazitäten de
s Eisenbahnnetzen
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.
 \;
Der Vortrag erläutert den aktuellen Arb
eitsstand und stellt noch offene Probleme vor\, welche anschließend gemeins
am diskutiert werden sollen.
 \;
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
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: Agenda
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 \; 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 …\;
Continue reading →\;
X-ALT-DESC;FMTTYPE=text/html: Symbolic Approximation of the Bounded Reachab
ility Probability in Large Markov Chains
 \;
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.
 \;
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.
 \;
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 …\; Continue reading →\;
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.
http://arxiv.org/abs/1408.5752<
/a>
 \;
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.
http://arxiv.org/
abs/1412.3701
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 …\; Continue reading →\;
X-ALT-DESC;FMTTYPE=text/html: Fast detection of cycles in timed aut
omata
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 …\; Continue reading →\;
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.
Vorläufiges Programm |
Donnerstag\, 5. Februar 2015 |
12:00 - 13:00 |
Come together |
13:00
- 13:25 |
Friedhelm Meyer auf der Heide -- Berthold's First Theor
em |
13:25 - 13:40 |
Christian Scheideler
-- Meine Forschung mit Berthold - ein Glücksfall! |
13:40 - 13:55 |
Matthias Westermann -- Von Katzen und Autos - Wie
uns Katzenstreu wieder auf die Spur brachte |
13:5
5 - 14:10 |
Petra Berenbrink -- Berthold und das Always-Go-Left Pr
otokoll |
14:10 - 14:25 |
Bruce Maggs -- .
.. |
14:25 - 14:45 |
Pause |
14:45 - 15:10 |
Kurt Mehlhorn -- Bertholds Jahre am MPI
für Informatik |
15:10 - 15:25 |
Peter Sa
nders -- Parallelism and Much More |
15:25 - 15:35<
/td>
| Christian Schindelhauer -- Rumor Spreading in Berkeley |
tr>
15:35 - 15:50 |
Christian Sohler -- Von Hasen und
Jägern |
15:50 - 16:20 |
Pause |
16:20 - 16:45 |
Artur Czumaj -- On Random Choices<
/td>
|
16:45 - 17:00 |
Heiko Röglin -- Berthold
s Beiträge zur Smoothed Analysis |
17:00 - 17:30
| Matthias Englert und Harald Räcke -- First Contact - How Berthold
introduced us to Research |
Freitag\, 6
. Februar 2015 |
10:15 - 10:30 |
Ernst Sch
machtenberg\, Rektor der RWTH University |
10:00 -
10:15 |
Thomas Seidl\, Fachgruppe Informatik |
10:30 - 10:40 |
Christel Baier\, Deutsche Forschungsgemeinsch
aft |
10:40 - 10:50 |
Martin Dietzfelbinge
r\, Gesellschaft für Informatik |
10:50 - 11:00 |
Studierende der Informatik\, Fachschaft |
1
1:15 - 12:15 |
Bruce Maggs -- The Internet at the Speed of Light
td>
|
12:15 - 13:00 |
Ausklang |
<
/tbody>
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 –\; 21:30 Welcome (with drinks and snacks) at ̶
0\;SuperC”\;\, RWTH Aachen (6th Floor)
X-ALT-DESC;FMTTYPE=text/html:
19:00 - 21:30 |
<
td>Welcome (with drinks and snacks) at "SuperC"\, RWTH Aachen (6th Floor)
td>
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 “\;Frontiers of Formal Metho
ds”\; Aachen\, Germany February 25 –\; 27\, 2015 \; 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 …\; Continue
reading →\;
X-ALT-DESC;FMTTYPE=text/html:
 \;
organized by the DFG Research Training Groups
AlgoSyn (Algorithmic Synthesis of
Reactive and Discrete-Continuous Systems)\, Aachen
PUMA (Program and Model Analysis)\, München<
/a>
QuantLA (Quantitative
Logics and Automata)\, Dresden &\; Leipzig
SCARE (System Correctness under Adverse Conditons)\,
Oldenburg
and the Austrian Research Ne
twork ARiSE (Rigorous System Engineering)
 \;
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:
Sub
mission: |
December 15\, 2014 |
Notificati
on: |
January 15\, 2015 |
Conference: |
February 25 - 27\, 2015 |
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 –\; 9:15 Welcome 9:15 –\; 10:15 Moshe Vardi: Th
e Rise and fall of Linear Temporal Logic Coffee Break 10:30 –\; 11:30
Shiguang Feng : Path-Checking for MTL and TPTL over Data Words Claudia Cara
pelle : Satisfiability of ECTL* with constraints Sascha …\; Continue reading →\;
X-ALT-DESC;FMTTYPE=text/html:
9:00 - 9:15 |
Welcome |
9:15 - 10:15 |
- M
oshe Vardi: The Rise and fall of Linear Temporal Logic
|
|
Coffee Break |
10
:30 - 11:30 |
- Shiguang Feng : Path-Checking for
MTL and TPTL over Data Words
- Claudia Carapelle : Sati
sfiability of ECTL* with constraints
- Sascha Wunderlich : <
em>Weight Monitoring with Linear Temporal Logic
- Normann De
cker : On an Extension of Freeze LTL Part I - Decidability
- Daniel Thoma : On an Extension of Freeze LTL: Part II - Complexity
|
|
Coffee Break
|
11:45 - 12:45 |
- Edon Kelmen
di : Two-player shift-invariant and submixing stochastic games are half
-positional
- Pierre Carlier : Composition of Stochastic
Timed Automata
- David Müller : Are Good-for-games Auto
mata Good for Probabilistic Model Checking?
- Dennis Guck :
Markov Reward Automata in Railway Engineering
- Yang Gao
: Decision Procedure for Stochastic Satisfiability Modulo Theories wit
h Continuous Domain
|
|
Lunch Break
|
14:00 - 15:00 |
|
|
Coffee Break |
15:20 - 16:20 |
- Jan Oliver Rin
gert : Extensible Support for Specification Patterns in GR(1) Synthesis
-- Work in Progress
- Mickael Randour : Games with Wind
ow Quantitative Objectives
- Loredana Sorrentino : On Pr
omptness in Parity Games
- Benedikt Brütsch : Synthesizi
ng Structured Reactive Programs via Deterministic Tree Automata
- Florian Corzilius : SMT-RAT: An SMT-Compliant Nonlinear Real and
Integer Arithmetic Toolbox
|
<
/td>
| Coffee Break |
16:40 - 17:40 |
- Dmitriy Traytel : Derivatives of WS1S Formulas
- Stephan Barth : Deciding Monadic Second Order Logic over omega-
words by Specialized Finite Automata
- Simon Leßenich :
A Quantitative Counting Monadic Second-Order Logic
- Sarah W
inter : Uniformization of Automatic Tree Relations by Top-down Tree Tra
nsducers
- Frederic Reinhardt : Automatic Structures wit
h Parameters
|
19:00 |
Optional: Guided tour through the city\, Fischpüddelchen
<
/tbody>
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 –\; 10:00 Jean-Francois Raskin: Variations on the st
ochastic shortest path problem Coffee Break 10:20 –\; 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 …\; Continue reading →\;
X-ALT-DESC;FMTTYPE=text/html:
9:00 - 10:00 |
td>
| Coffee Break |
10:20 - 11:20 |
- Vitaly Perevoshchikov : Decomposition of Weighted Timed A
utomata
- Parvaneh Babari : A Nivat Theorem for Weighted
Picture Automata and Weighted MSO Logics
- Mohamed Abdelaal
: Fuzzy Compression Refinement via Curvature Tracking
-
Saifullah Khan : Traffic Data Dissemination in Realistic Urban VANETs En
vironment
- Andreas Tönnis : Packing Secretaries
|
|
Coffee Break |
11:40 - 12:40 |
- Georgel Calin : Lazy TSO Reachability
- Veronika Loitzenbauer : A Hiera
rchical Sparsification Technique for Faster Algorithms in Graphs and Game G
raphs
- Christina Jansen : Generating Abstract Graph-Bas
ed Procedure Summaries for Pointer Programs
- Ayrat Khalimov
: Tight Fair Cutoffs for Conjunctive Guard Systems
- Th
omas Stroeder : Transformational Termination Analysis of Programs with
Pointer Arithmetic
|
|
<
td>
Lunch Break
14:00 - 15:00 |
|
|
Coffe
e Break |
15:20 - 16:20 |
- C
hristian Dehnert : Fast Debugging of PRISM Models
- Joha
nnes Hölzl : Probability Theory and Markov Processes in Isabelle/HOL
- René Neumann : A verified LTL model checker
- Manuel Gieseking : Trace Refinement of pi-Calculus Processes<
/li>
- Stefan Schulze Frielinghaus : Inter-procedural Two-Variable
Herbrand Equalities are in PTIME
|
|
Coffee Break |
16:40 - 17:40 |
- Markus Teichmann : Regular Context-Free Tree Gram
mars
- Doreen Heusel : Weighted Unranked Tree Automata o
ver Tree Valuation Monoids
- Nils Erik Flick : Derivatio
n Languages of Graph Grammars and Correctness
- Thomas Weidn
er : Probabilistic Logic and Regular Expressions on Finite Trees
li>
- Félix Baschenis : From sweeping transducers to one way trans
ducers
|
19:30 |
Conf
erence dinner at Tivoli Football Stadium (VIP Lounge) |
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 –\; 10:00 Eric Bodden: SPLlift: statically analyzing
software product lines in minutes instead of years Coffee Break 10:20 R
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 …\; Continue reading
→\;
X-ALT-DESC;FMTTYPE=text/html:
9:00 - 10:00 |
|
Coffee Break |
10:20
- 11:20 |
- Bogdan Mihaila : Synthesizing Predic
ates from Abstract Domain Losses
- Suvam Mukherjee : Eff
icient Shape Analysis of Multithreaded Programs
- Mitra Taba
ei Befrouei : Abstraction and Mining of Traces to Explain Concurrency B
ugs
- Christian Müller : An Analysis of Universal Inform
ation Flow based on Self-Compositions
- Björn Engelmann : Formally Verifying Dynamically-typed Programs like Statically-typed Ones
– A different perspective
|
td>
| Coffee Break |
11:40 - 12:40 |
- Philipp Hoffmann : Negotiations as a concurrency primitiv
e: Summaries and Games
- Giuseppe Perelli : Strategy Log
ic: a powerful formalism for game-theoretical issues
- Vadim
Malvone : Graded Strategy Logic
- Oliver Fernandez Gil
: Threshold Concepts in a Lightweight Description Logic
Andreas Ecke : Relaxing Description Logics Queries using Similarity M
easures
|
|
L
unch Break
|
14:00 - 15:00 |
Joel Ouaknine: Termination of Linear Loops: Algorithmic Ad
vances and Challenges
|
td>
| Coffee Break |
15:20 - 16:30 |
- Fabian Immler : Continuous Systems Reachability using Ada
ptive Runge-Kutta Methods - Formally Verified
- Manuel Eberl
\, Johannes Hölzl and Tobias Nipkow : A Verified Compiler for Probabili
ty Density Functions
- Benjamin Lucien Kaminski : Analyz
ing Expected Outcomes and (Positive) Almost-Sure Termination of Probabilist
ic Programs is Hard
- Friedrich Gretz : Conditioning in
Probabilistic Programming
- Nils Jansen : A Greedy Appro
ach for the Efficient Repair of Stochastic Models
- Oliver G
öbel : On Stochastic Input Models in Online Optimization
ul>
|
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 –\; 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 …\; Continue reading →\;
X-ALT-DESC;FMTTYPE=text/html:
„Die 2 Seiten der Gläsernen Decke“\, gehalten von Marion Knaths
am 03.03 um 17h im Super
C\, Generali Saal - Templergraben 55\, 6. Etage
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.
Marion Knaths - www.sheb
oss.de - 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.
ANMELDUNG: Aus organisatorisch
en Gründen\, bitten wir Sie\, sich bis zum 22.02 bei Odile Clavery anzumelden. Vielen Dank!
Wir würden uns besonders freuen\, wenn sich auch zahlreiche Männer zu dies
em Vortrag anmelden.
 \;
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) –\; haben einen Saal im Apollo-Kino reserviert und gezei
gt wird: The Imitation Game Am 4. März 2015 …\; Continue r
eading →\;
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:
The Imitation Game
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ünden 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 …\; Continue reading &
#8594\;
X-ALT-DESC;FMTTYPE=text/html: If-Next-Also-Else: Controlling Graph Tran
sformation
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 ̷
0\; Continue reading →\;
X-ALT-DESC;FMTTYPE=text/html: 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 …\; Continue reading →\;
X-ALT-DESC;FMTTYPE=text/html: Switched Region Stabilization of Polynomi
al Dynamical Systems
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 …\; Continue reading →\;
X-ALT-DESC;FMTTYPE=text/html: Machine Learning meets Formal Verificatio
n
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 …\; <
a href="http://www.algosyn.rwth-aachen.de/events/event/presentation-roberta
-lanciani/">Continue reading →\;
X-ALT-DESC;FMTTYPE=text/html: Stochastic Approximations and Verificatio
ns
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) …\; Continue reading →\;
X-ALT-DESC;FMTTYPE=text/html: Counterexamples in Probabilistic Verifica
tion
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 \; 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 …\; <
a href="http://www.algosyn.rwth-aachen.de/events/event/prof-lijun-zhang-pol
ynomial-quantitative-loop-invariants-by-lagrange-interpolation/">Continue r
eading →\;
X-ALT-DESC;FMTTYPE=text/html: Polynomial Quantitative Loop Invariants by La
grange Interpolation
 \;
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 …\; Continue r
eading →\;
X-ALT-DESC;FMTTYPE=text/html: Jewels of Automata: from Mathematics to A
pplications
Leipzig\, May 6-9\, 2015
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.
Website
Invited speakers
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)
Program Committee
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)
Registration
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
Contact
Manfred Droste or
Werner Kuich or
Jean-Éric Pin or
Wolfgang Thomas
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 …\; Continue reading →\
;
X-ALT-DESC;FMTTYPE=text/html: Referent: Dipl.-Inform. Simon Lessenich
Titel: Counting Logics and Games with Counters
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
 \;
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 …\; Continue reading →\;
X-ALT-DESC;FMTTYPE=text/html: Optimization of Railway-networks
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
…\; Continue reading →\;
X-ALT-DESC;FMTTYPE=text/html: Abschlussveranstaltung Graduierten
kolleg AlgoSyn
10.00 Begrüßung
10.1
5 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 Einteilung der Untergruppen
14.15 Das GK-intere Projekt „Scientific Life“
14.45 Prä
sentation „Das Modell Graduiertenkolleg als Erfolgsformat für strukturierte
Promotionen“
15.15 Abschließende Worte durch den Sprecher Prof
. Dr. Wolfgang Thomas
15.30 Ausklang
 \;
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 …
\; Continue reading →\;
X-ALT-DESC;FMTTYPE=text/html: Algorithmic Formal Methods in Continuous
Control
Abstract: Algorithmic formal methods such as model checking
and reactive synthesis were originally developed in the context of discrete
systems such as hardware circuits and software. Over the last few years\,
these techniques have played an increasingly important role in the 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 …\; Continue reading →\;
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 …\; Continue reading →\;
X-ALT-DESC;FMTTYPE=text/html: Referent: Dipl.-Inform. Friedrich Gretz
Titel: Semantics and Loop Invariant Synthesis for Probabilistic Pro
grams
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 …\; Continue readin
g →\;
X-ALT-DESC;FMTTYPE=text/html: Referent: Dipl.-Inform. Ibtissem Ben Makhlouf
Titel: Comparative Evaluation and Improvement of Computationa
l Approaches to Reachability Analysis of Linear Hybrid Systems
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 R
30\; Continue reading →\;
X-ALT-DESC;FMTTYPE=text/html: Referent: Dipl.-Inform. Oliver Göbel
Titel: Online Resource Allocation on Stochastic Input Models
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