2009 | OriginalPaper | Buchkapitel
Runtime Verification Using a Temporal Description Logic
verfasst von : Franz Baader, Andreas Bauer, Marcel Lippmann
Erschienen in: Frontiers of Combining Systems
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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 behavior 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 behavior, which at any time point yields a finite prefix of a trace. The task is then to check whether all continuations of this prefix to 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
$\mathcal{ALC}$
-LTL, which can use axioms of the description logic
$\mathcal{ALC}$
instead of propositional variables to describe properties of single states of the system. Second, instead of assuming that the observed system behavior 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
$\mathcal{ALC}$
-ABoxes.