第29回先端ソフトウェア科学・工学に関するGRACEセミナー

参加をご希望の方は、セミナー前日までに下記よりご登録をお願いします。
http://grace-center.jp/regist/seminar

– – – – – – – – – – – – – – – – – – – – – – – – – – – – – – – – –
Details:
Speaker: Franz Weitl, visiting researcher at the NII
http://researchmap.jp/weitl

Title: Document Verification with Temporal Description Logics

Abstract:
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.

Biography:
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.