Paper Info
Title
Runtime verification using a temporal description logic
Abstract
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 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 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 ALC-ABoxes.
Year
DOI
Venue
2009
10.1007/978-3-642-04222-5_9
FroCos
Keywords
Field
DocType
description logic alc,possible trace,linear temporal logic,runtime verification,dynamical system,observed system behavior,propositional ltl,actual system behavior,temporal description logic,transition system,finite prefix,satisfiability,model checking,description logic,dynamic system
Transition system,Model checking,Programming language,Axiom,Computer science,Description logic,Linear temporal logic,Theoretical computer science,Discrete mathematics,Algorithm,Runtime verification,Dynamical systems theory,Propositional variable
Conference
Volume
ISSN
ISBN
5749
0302-9743
3-642-04221-X
Citations 
PageRank 
References 
18
0.78
11
Authors
3
Name
Order
Citations
PageRank
Franz Baader18123646.64
Andreas Bauer2261.97
Marcel Lippmann31126.98