Runtime Verification Using a Temporal Description Logic

Franz BaaderFranz Baader, Andreas BauerAndreas Bauer, Marcel LippmannMarcel Lippmann

Download

Franz Baader, Andreas Bauer, Marcel Lippmann
Runtime Verification Using a Temporal Description Logic
In Silvio Ghilardi and Roberto Sebastiani, eds., Proceedings of the 7th International Symposium on Frontiers of Combining Systems (FroCoS 2009), volume 5749 of Lecture Notes in Computer Science, 149-164, 2009. Springer

Details
Bibtex

KurzfassungAbstract
Formulae of linear temporal logic (LTL) can be used to specify (wanted or unwanted) properties of a dynamical system. In model checking, the system's behaviour is described by a transition system, and one needs to check whether all possible traces of this transition system satisfy the formula. In runtime verification, one observes the actual system behaviour, which at any time point yields a finite prefix of a trace. The task is then to check whether all continuations of this prefix into a trace satisfy (violate) the formula. In this paper, we extend the known approaches to LTL runtime verification in two directions. First, instead of propositional LTL we use ALC-LTL, which can use axioms of the description logic ALC instead of propositional variables to describe properties of single states of the system. Second, instead of assuming that the observed system behaviour provides us with complete information about the states of the system, we consider the case where states may be described in an incomplete way by ALC ABoxes.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

The final publication is available at Springer.

@inproceedings{ BaBaLi-FroCoS09,
  author = {Franz {Baader} and Andreas {Bauer} and Marcel {Lippmann}},
  booktitle = {Proceedings of the 7th International Symposium on Frontiers of Combining Systems (FroCoS 2009)},
  editor = {Silvio {Ghilardi} and Roberto {Sebastiani}},
  pages = {149--164},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  title = {Runtime Verification Using a Temporal Description Logic},
  volume = {5749},
  year = {2009},
}