You are here: Foswiki>Inf Web>InformatikKolloquium>InformatikKolloquiumSoSe2010>InformatikKolloquiumWiSe2010 (03 Mar 2011, GesineMilde)Edit

Informatik-Kolloquium WiSe 2010/2011

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
Februar
Vorlage
- Fr, xx.xx.2010: Titel
Kolloquium in anderen Semestern
Kommentare

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.