#1 16.07.2008 21:29:38

Coolcat
ProGuru
Ort: Aachen, NRW
Registriert: 24.01.2005
Beiträge: 2780
Web-Seite

Seminar-Arbeit: Komplementierung von Büchi-Automaten

Ist ziemlich Offtopic, aber vielleicht gibt es ja hier angehende Informatik-Studenten wink

Hier meine Ausarbeitung im Rahmen eines Seminars über Automatentheorie. Das Thema lautet "Komplementierung von Büchi-Automaten", das ganze liegt also ziemlich tief im Bereich der theoretischen Informatik. Ich behandle primär einen Ansatz von Wilke und Vardi (2008) auf Basis von reduzierten Akzeptanzbäumen. Neben der Ausarbeitung habe ich einen etwa einstündigen Vortrag über das Thema gehalten.

http://www-users.rwth-aachen.de/martin. … 6-2246.pdf
http://www-users.rwth-aachen.de/martin. … slides.pdf

Was bitte ist ein Büchi-Automat?
Nun, viele kennen sicher gewöhnliche endliche Automaten, vielleicht auch ohne zu wissen, dass es sich um einen "Automaten" handelt. Jeder der schon mal einen Parser geschrieben oder was von regulären Ausdrücken gehört hat, hat mit Automaten gearbeitet. Ich denke die http://de.wikipedia.org/wiki/Automat_(Informatik) ist ganz gut.
Ein Büchi-Automat ist im Prinzip das gleiche, nur das dieser auf unendlichen Wörtern arbeitet. Der Automat akzeptiert, wenn unendlich oft Endzustände erreicht werden. Ich behandele in meiner Ausarbeitung nicht-deterministische Büchi-Automaten.

Was ist das Komplement?
Der Komplementautomat zu einem Automaten ist der Automat der genau das Gegenteil akzeptiert. Er akzeptiert ein Wort immer dann, wenn es vom anderen Automaten nicht akzeptiert wird.

Aha, und wozu braucht man das?
Nun, theoretische Informatik ist halt theoretisch, aber beispielsweise kann man das für reaktive Systeme gebrauchen. Man kann damit also beispielsweise Netzwerkprotokolle verifizieren. Dabei wären die Daten die aus dem Netzwerk kommen das Eingabewort. Modelliert man das Protokoll als Automat kann man dann bestimmte Dinge beweisen, beispielsweise das der Computer immer in einen gültigen Zustand (=Endzustand) zurückkehrt. Dazu würde man den Automaten komplementieren und diesen dann auf Leerheit testen. Ist der Komplementautomat leer, er akzeptiert also kein einziges Wort, dann kehrt unser Protokoll immer in einen gültigen Zustand zurück. Die Leerheit eines Automaten kann man ganz einfach mit einer Tiefensuche testen.


Lasst euch hier durch nicht von einem Informatik-Studium abschrecken, sowas macht man sicher nicht im ersten Semester wink


My software never has bugs. It just develops random features.

Offline

 

#2 17.07.2008 06:48:21

artzuk
GodlikeMember
Ort: Leipzig
Registriert: 24.01.2005
Beiträge: 1164

Re: Seminar-Arbeit: Komplementierung von Büchi-Automaten

Ui, für einen Nicht-Studenten ist das ein ziemlich hartes Ding! Soll heißen: ich verstehe nichts von deinen Folien ^^ Werde mir bestimmt mal die Ausarbeitung ansehen, mal sehen wie weit ich komm smile


Mein kleiner .NET Blog: http://artzuk-interactive.de/

Offline

 

#3 17.07.2008 17:17:38

Lotipats
UltraMember
Registriert: 17.05.2005
Beiträge: 395

Re: Seminar-Arbeit: Komplementierung von Büchi-Automaten

Nachdem ich über die ersten Folien weg war, erschien es mir verständlich (ob ich es "anwenden" kann, ist eine andere Sache), mit Ausnahme von Folie 40 wink Aber ich habe auch nur schnell rüber gesehen.
Zugleich muss ich sagen, dass ich das auch (g.T.) nur Aufgrund der Schulbildung verstehe, Automaten kommen (soweit ich weiß) erst nächstes Semester mir "Grundlagen der theoretischen Informatik". (Das Sigma kenne ich allerdings wegen Logik, 1.Semester). cool

Wenn (oder während) wir Automaten hatten, werde ich mir das vllt. nochmal ansehen.

[quote=Coolcat]Lasst euch hier durch nicht von einem Informatik-Studium abschrecken, sowas macht man sicher nicht im ersten Semester wink

Das unterschreibe ich (nach Regelstudienplan)!

LOTIPATS

Offline

 

Brett Fußzeile

Powered by PunBB
© Copyright 2002–2005 Rickard Andersson