Marcel Lippmann

Temporalised Description Logics for Monitoring Partially Observable Events

Dokumente und Dateien


Bitte nutzen Sie beim Zitieren immer folgende Url:

Kurzfassung in Englisch

Inevitably, it becomes more and more important to verify that the systems surrounding us have certain properties. This is indeed unavoidable for safety-critical systems such as power plants and intensive-care units. We refer to the term system in a broad sense: it may be man-made (e.g. a computer system) or natural (e.g. a patient in an intensive-care unit). Whereas in Model Checking it is assumed that one has complete knowledge about the functioning of the system, we consider an open-world scenario and assume that we can only observe the behaviour of the actual running system by sensors. Such an abstract sensor could sense e.g. the blood pressure of a patient or the air traffic observed by radar.

Then the observed data are preprocessed appropriately and stored in a fact base. Based on the data available in the fact base, situation-awareness tools are supposed to help the user to detect certain situations that require intervention by an expert. Such situations could be that the heart-rate of a patient is rather high while the blood pressure is low, or that a collision of two aeroplanes is about to happen.

Moreover, the information in the fact base can be used by monitors to verify that the system has certain properties. It is not realistic, however, to assume that the sensors always yield a complete description of the current state of the observed system. Thus, it makes sense to assume that information that is not present in the fact base is unknown rather than false. Moreover, very often one has some knowledge about the functioning of the system. This background knowledge can be used to draw conclusions about the possible future behaviour of the system. Employing description logics (DLs) is one way to deal with these requirements. In this thesis, we tackle the sketched problem in three different contexts: (i) runtime verification using a temporalised DL, (ii) temporalised query entailment, and (iii) verification in DL-based action formalisms.

weitere Metadaten

Temporalisierte Beschreibungslogiken, Verifikation, Komplexität
Temporalised Description Logics, Verification, Complexity
DDC Klassifikation004
RVK KlassifikationST 125
HochschuleTechnische Universität Dresden
FakultätFakultät Informatik
ProfessurProfessur für Automatentheorie
BetreuerProf. Dr.-Ing. Franz Baader
GutachterProf. Dr.-Ing. Franz Baader
Prof. Dr. rer. nat. habil. Frank Wolter
Tag d. Einreichung (bei der Fakultät)24.04.2014
Tag d. Verteidigung / Kolloquiums / Prüfung01.07.2014
Veröffentlichungsdatum (online)09.07.2014
persistente URNurn:nbn:de:bsz:14-qucosa-147977

Hinweis zum Urheberrecht

Diese Website ist eine Installation von Qucosa - Quality Content of Saxony!
Sächsische Landesbibliothek Staats- und Universitätsbibliothek Dresden