004 Datenverarbeitung; Informatik
Refine
Year of publication
- 2007 (1) (remove)
Document Type
- Doctoral Thesis (1)
Language
- English (1)
Has Fulltext
- yes (1)
Is part of the Bibliography
- no (1)
Keywords
- CTL (1)
- Dokumentmodell (1)
- Dokumentprüfung (1)
- Dokumentvalidierung (1)
- Dokumentverifikation (1)
- Formale Ontologie (1)
- Konsistenz <Informatik> (1)
- Model Checking (1)
- Schlussfolgern (1)
- Temporale Logik (1)
Institute
- Mitarbeiter Lehrstuhl/Einrichtung der Fakultät für Informatik und Mathematik (1) (remove)
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.