PhD defence by Mai Lise Ajspur
Invitation to PhD defense
Thursday October 31, 2013 at 9.00 – 12.00 in room 43-3.29
Mai Lise Ajspur
defends her thesis:
Tableau-based decision procedure for epistemic and temporal epistemic logics
Abstract:
The dissertation is concerned with decision procedures for epistemic and temporal epistemic logics. Epistemic logic is a modal logic where the modalities - represented by the epistemic operators - formalize various concepts relating to knowledge. On the other hand, the temporal logics LTL and CTL are used to reason about computational states changing over time. Combining the two types of logics results in temporal epistemic logics which are useful for formalizing and reasoning about knowledge changing over time in for instance distributed or multiagent systems. However, certain properties of the relationship between knowledge and time of such systems cannot be captured by the syntax of the corresponding logics but is described by properties - referred to as temporal-epistemic interaction properties - of the semantical models for the logics. By restricting the semantics to models satisfying various interaction properties, other temporal epistemic logics emerge.
To be useful in practice for tasks such as specifying, designing and verifying distributed or multiagent systems, the logics must be equipped with reasoning procedures. The focus of this dissertation is the development of tableau-based decision procedures for the satisfiability problem of a number of these epistemic and temporal epistemic logics with operators from LTL, with and without temporal-epistemic interaction properties..
Assessment Committee
Torben Braüner, Associate Professor CBIT, Roskilde University (chairman)
Renate Schmidt, Associate Professor, School of Computer Science, University of Manchester
Thomas Bolander, Associate Professor, DTU Compute, Technical University of Denmark
Head of defense
Keld Bødker, Associate professor, CBIT, Roskilde University
Supervisor
John Gallagher, Professor, CBIT, Roskilde University
Thesis is available for examination here soon.
After the defense CBIT will host a reception.