@TechReport{	  basin.ea:runtime:2008,
  abstract	= {We introduce a novel approach to the runtime monitoring of
		  complex system properties.In particular, we present an
		  online algorithm for a safety fragment of metric
		  first-order temporal logic(MFOTL) that is considerably more
		  expressive than the logics supported by prior monitoring
		  methods.Our approach, based on automatic structures, allows
		  the unrestricted use of negation, universal andexistential
		  quantification over infinite domains, and the arbitrary
		  nesting of both past and boundedfuture operators. Moreover,
		  we show how to use and optimize our approach for the common
		  case wherestructures consist of only finite relations, over
		  possibly infinite domains. Under an additional
		  restriction,we prove that the space consumed by our monitor
		  is polynomially bounded by the cardinality of thedata
		  appearing in the processed prefix of the temporal structure
		  being monitored.},
  author	= {David Basin and Felix Klaedtke and Samuel M{\"u}ller and
		  Birgit Pfitzmann},
  institution	= {IBM Research & ETH Zurich},
  language	= {USenglish},
  month		= {February},
  number	= {RZ 3702},
  pdf		= {papers/2008/rz3702.pdf},
  title		= {Runtime Monitoring of Metric First-order Temporal
		  Properties},
  year		= 2008,
  user		= {sml}
}