  The main purpose of this paper is to introduce a first-order temporal logic,
LTLFO, and a corresponding monitor construction based on a new type of
automaton, called spawning automaton.
  Specifically, we show that monitoring a specification in LTLFO boils down to
an undecidable decision problem. The proof of this result revolves around
specific ideas on what we consider a "proper" monitor. As these ideas are
general, we outline them first in the setting of standard LTL, before lifting
them to the setting of first-order logic and LTLFO. Although due to the above
result one cannot hope to obtain a complete monitor for LTLFO, we prove the
soundness of our automata-based construction and give experimental results from
an implementation. These seem to substantiate our hypothesis that the
automata-based construction leads to efficient runtime monitors whose size does
not grow with increasing trace lengths (as is often observed in similar
approaches). However, we also discuss formulae for which growth is unavoidable,
irrespective of the chosen monitoring approach.
