University of Konstanz
Graduiertenkolleg / PhD Program
Computer and Information Science

Guest Talks


Runtime Monitoring of Metric First-order Temporal Properties


Dr. Felix Kaedtke, ETH Zürich
Zurich, Switzerland

date & place

Thursday, 16.07.2009, 14:00 h
Room D247


In this talk I will present a novel approach to the runtime monitoring of complex system properties. In particular, I will introduce an online algorithm for a safety fragment of metric first-order temporal logic that is considerably more expressive than the logic supported by prior monitoring methods. The presented approach, based on automatic structures, allows the unrestricted use of negation, universal and existential quantification over infinte domains, and the arbitrary nesting of both past and bounded future operators. Moreover, I will show how to optimize our approach for the common case where structures consist of only finite relations, over possibly infinite domains. Under an additional restriction, I will show that the space consumed by the monitor is polynomially bounded by the cardinality of the data appearing in the processed prefix of the temporal structure being monitored. This is joint work with David Basin, Samuel Mueller and Birgit Pfitzmann.