Bauer, AndreasKuester, Jan-ChristophVegliach, Gil2015-12-10September9783642407864http://hdl.handle.net/1885/66310The 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 boilsFrom Propositional to First-Order Monitoring201310.1007/978-3-642-40787-1_42015-12-10