Runtime Verification Using a Temporal Description Logic Revisited

Franz BaaderFranz Baader, Marcel LippmannMarcel Lippmann

Download

Franz Baader, Marcel Lippmann
Runtime Verification Using a Temporal Description Logic Revisited
Technical Report, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, volume 14-01, 2014. LTCS-Report

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 point in time 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. More precisely, one wants to construct a monitor, i.e., a finite automaton that receives the finite prefix as input and then gives the right answer based on the state currently reached. In this paper, we extend the known approaches to LTL runtime verification in two directions. First, instead of propositional LTL we use the more expressive temporal logic ALC-LTL, which can use axioms of the Description Logic (DL) 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 assume that states are described in an incomplete way by ALC-knowledge bases. We show that also in this setting monitors can effectively be constructed. The (double-exponential) size of the constructed monitors is in fact optimal, and not higher than in the propositional case. As an auxiliary result, we show how to construct Büchi automata for ALC-LTL-formulae, which yields alternative proofs for the known upper bounds of deciding satisfiability in ALC-LTL.
Bemerkung: Note: See http://lat.inf.tu-dresden.de/research/reports.html.
Forschungsgruppe:Research Group: Automatentheorie

@techreport{ BaLi-LTCS-14-01,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Marcel {Lippmann}},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See \url{http://lat.inf.tu-dresden.de/research/reports.html}.},
  number = {14-01},
  title = {Runtime Verification Using a Temporal Description Logic Revisited},
  type = {LTCS-Report},
  year = {2014},
}