OPUS - Passau

Bibliographische Daten und PDF-Volltexte aus der Universität Passau
... die Wissenschaft der Hochschule sichtbar machen!

Home

Suchen

Melden

Veröffentlichen

Hilfe

Kontakt

OPUS-Frontdoor

Weitl, Franz

Document Verification with Temporal Description Logics

Dokumentverifikation mit Temporaler Beschreibungslogik

Open Access: Freier Zugang zum Volltext!

pdf-Format:

Dokument 1.pdf (1.445 KB)

SWD-Schlagwörter:		Verifikation , Model Checking , Temporale Logik , Terminologische Logik , Schlussfolgern , Formale Ontologie , Konsistenz <Informatik> , Widerspruchsfreiheit , Textkohärenz
Freie Schlagwörter (Deutsch):		Dokumentprüfung, Dokumentvalidierung, Dokumentverifikation, CTL, computation tree logic, Dokumentmodell, pfadbasierte Konsistenz
Freie Schlagwörter (Englisch):		document verification, path-based consistency, coherence, temporal description logic, model checking
Beteiligte Einrichtung:		Mitarbeiter Lehrstuhl/Einrichtung der Fakultät für Informatik und Mathematik
Fakultät:		Fakultät für Informatik und Mathematik
DDC-Sachgruppe:		Informatik
Dokumentart:		Dissertation
Hauptberichter:		Freitag, Burkhard (Prof. Dr.)
Sprache:		Englisch
Tag der mündlichen Prüfung:		10.06.2008
Erstellungsjahr:		2007
Publikationsdatum:		21.10.2008
Kurzfassung auf Englisch:		The thesis proposes a new formal framework for checking the content of web documents along individual reading paths. It is vital for the readability of web documents that their content is consistent and coherent along the possible browsing paths through the document. Manually ensuring the coherence of content along the possibly huge number of different browsing paths in a web document is time-consuming and error-prone. Existing methods for document validation and verification are not sufficiently expressive and efficient. The innovative core idea of this thesis is to combine the temporal logic CTL and description logic ALC for the representation of consistency criteria. The resulting new temporal description logics ALCCTL can - in contrast to existing specification formalisms - compactly represent coherence criteria on documents. Verification of web documents is modelled as a model checking problem of ALCCTL. The decidability and polynomial complexity of the ALCCTL model checking problem is proven and a sound, complete, and optimal model checking algorithm is presented. Case studies on real and realistic web documents demonstrate the performance and adequacy of the proposed methods. Existing methods such as symbolic model checking or XML-based document validation are outperformed in both expressiveness and speed.
Kurzfassung auf Deutsch:		Die Dissertation stellt ein neues formales Framework für die automatische Prüfung inhaltlich-struktureller Konsistenzkriterien an Web-Dokumente vor. Viele Informationen werden heute in Form von Web-Dokumenten zugänglich gemacht. Komplexe Dokumente wie Lerndokumente oder technische Dokumentationen müssen dabei vielfältige Qualitätskriterien erfüllen. Der Informationsgehalt des Dokuments muss aktuell, vollständig und in sich stimmig sein. Die Präsentationsstruktur muss unterschiedlichen Zielgruppen mit unterschiedlichen Informationsbedürfnissen genügen. Die Sicherstellung grundlegender Konsistenzeigenschaften von Dokumenten ist angesichts der Vielzahl der Anforderungen und Nutzungskontexte eines elektronischen Dokuments nicht trivial. In dieser Arbeit werden aus der Hard-/Softwareverifikation bekannte Model-Checking-Verfahren mit Methoden zur Repräsentation von Ontologien kombiniert, um sowohl die Struktur des Dokuments als auch inhaltliche Zusammenhänge bei der Prüfung von Konsistenzkriterien berücksichtigen zu können. Als Spezifikationssprache für Konsistenzkriterien wird die neue temporale Beschreibungslogik ALCCTL vorgeschlagen. Grundlegende Eigenschaften wie Entscheidbarkeit, Ausdruckskraft und Komplexität werden untersucht. Die Adäquatheit und Praxistauglichkeit des Ansatzes werden in Fallstudien mit eLearning-Dokumenten evaluiert. Die Ergebnisse übertreffen bekannte Ansätze wie symbolisches Model-Checking oder Methoden zur Validierung von XML-Dokumenten in Performanz, Ausdruckskraft hinsichtlich der prüfbaren Kriterien und Flexibilität hinsichtlich des Dokumenttyps und -formats.
Lizenz:		Veröffentlichungsvertrag für Publikationen mit Print on Demand

Lizenz

URN: http://nbn-resolving.de/urn:nbn:de:bvb:739-opus-12528
URL dieser Seite: http://www.opus-bayern.de/uni-passau/volltexte/2008/1252/