Termine, Vortragende, Titel und Zusammenfassungen für das
Kolloquium im Wintersemester 2010/2011.
Die Vorträge finden in unregelmäßigen Abständen in der Regel
Freitags um 14:00 Uhr im Seminarraum 049 in der Takustr. 9 statt.
Vorläufige Terminreservierungen ohne Gastname sind als
"(reserviert von [Einladende/r])"
einzutragen; Termine noch ohne Gewähr als
"(wahrscheinlich)"
o.ä. zu markieren. Im Rumpf des Eintrags steht jeweils, wer den Vortrag organisiert. (Zur technischen Notation siehe
ShortHand.)
Ab spätestens einen Tag vor dem Vortrag sollte auch eine Zusammenfassung dabeistehen.
Information zum Anlegen von Kolloquiumseiten pro Semester findet man unter
KolloWeitereInfos
September
Oktober
November
Dezember
Fr, 10.12.2010: reserviert / Prof. Schweppe
Fr, 17.12.2010: reserviert / Prof. Prechelt für Dissertation Oezbek
Januar
Fr, 28.01.2011: Quantitative Analyse randomisierter Systeme und probabilistische Automaten
Christel Baier, TU Dresden, (Marcel Kyas)
Takustr. 9, Raum 049, 14:15 bis ca. 15:45
Zusammenfassung
Automaten-basierte Modellprüfung
ist eine elegante Verifikationsmethode für
parallele Systeme und Pfadeigenschaften, die
- zusammen mit Heuristiken, die das Problem der Zustandsexplosion einzudämmen versuchen -
in zahlreichen Werkzeugen realisiert wurde.
Die Grundidee besteht darin, das zu verifizierende System und
die nachzuweisende Eigenschaft durch nichtdeterministische
Automaten darzustellen und das Produkt der beiden Automaten
zu analysieren.
Ein analoger automaten-basierter Ansatz ist auch für
die Berechnung von Wahrscheinlichkeiten von Pfadeigenschaften
in probabilistischer Systemen einsetzbar,
jedoch werden dann deterministische Automaten für die
Eigenschaften benötigt.
Der Vortrag stellt diesen Ansatz für Markov Entscheidungsprozesse
vor und erläutert kurz die Idee der Partial Order Reduction,
welche versucht Redundanzen, die sich aus der Kommutativität
unabhängiger Aktionen ergeben, zu erkennen und ein reduziertes
Systemmodell zu erstellen.
Weiter geht der Vortrag auf die Beobachtung ein, dass
die übliche Semantik von Markov Entscheidungsprozessen
keinerlei Einschränkungen an die Auflösung des Nichtdeterminismus
im Systemmodell macht und daher zu unrealistischen Analyseergebnissen
führen kann.
Das Modell von partiell-observierbaren Markov Entscheidungsprozessen
behebt zwar diese Anomalie, jedoch werden viele Verifikationsprobleme
unentscheidbar, was auf die Verwandtschaft von
partiell-observierbaren Markov Entscheidungsprozessen und
probabilistischen Automaten als Sprachakzeptoren zuruckzufuhren ist.
Februar
Vorlage
Fr, xx.xx.2010: Titel
Vortragende/r, Herkunftsorganisation, (eingeladen von Einladende/r)
Takustr. 9, Raum xx, 14:15 bis ca. 15:45
Zusammenfassung
Kolloquium in anderen Semestern
Nächstes Semester
InformatikKolloquiumSoSe2011
Frühere Semester
InformatikKolloquiumSoSe2010
InformatikKolloquiumWiSe2009
InformatikKolloquiumSoSe2009
InformatikKolloquiumSoSe2008
InformatikKolloquiumWiSe2008
InformatikKolloquiumSoSe2007
InformatikKolloquiumWiSe2006
InformatikKolloquiumSoSe2006
InformatikKolloquiumWiSe2005
InformatikKolloquiumSoSe2005
Kommentare