The 29th GRACE Seminar on Advanced Software Science and Engineering主催：NII 先端ソフトウェア工学国際研究センター（GRACEセンター）
場所：国立情報学研究所(NII) 19階プレセンテーション室(1904) （地図）
お問い合わせ：鄭 顕志 (tei_AT_nii.ac.jp)_AT_を＠に書き換えてください。
– – – – – – – – – – – – – – – – – – – – – – – – – – – – – – – – –
Speaker: Franz Weitl, visiting researcher at the NII
Title: Document Verification with Temporal Description Logics
A novel approach to document verification based on temporal description logics and model checking is presented.
Technical documentations or e-learning documents are usually authored in teams, compiled of different resources, and updated frequently. The parts of such documents are interrelated in terms of topics, terminology, and presentation style. Keeping them consistent is an ongoing challenge. Web documents complicate matters further because they can be read along many different paths and their content needs to be coherent and consistent on each path of reading.
For the representation of content- and path-related consistency criteria, the description logic ALC and the temporal logic CTL are combined. The resulting new temporal description logic ALCCTL remains decidable and is, in contrast to existing formalisms, sufficiently expressive for representing coherence criteria on paths. Verification of documents is modeled as an ALCCTL model checking problem. Results on the complexity of ALCCTL model checking are discussed along with experimental results obtained in case studies with web documents.
An outlook on counterexample generation spotlights our current focus of research.
Franz Weitl (ワイテル フランツ) is a postdoctoral research fellow of the German Academic Exchange Service (DAAD) at the NII. His current research aims at increasing the effectiveness and usability of model checking by generating structured counterexamples on different abstraction levels.
Franz started his academic career as a mathematical assistant at the research center of Juelich, Germany. He studied informatics at the Universities of Passau (Germany), Glasgow (Scotland), and Lund (Sweden), and worked as a software engineer in Kyoto. In 2008, he received a doctoral degree from the University of Passau. His thesis on “Document Verification with Temporal Description Logics” was nominated for the national dissertation award of the GI (German Society for Informatics) and was granted the dissertation award of the CommuniGate Communication Service Ltd.