A first-order temporal logic is introduced and argued to be suitable for modelling business processes and security policies for Android. The monitoring problem in such logic is introduced and argued to be undecidable under specific and reasonable assumptions underlying any proper monitor. Although no one can hope for a complete monitoring algorithm, a construction based on a novel automata model is depicted and its correctness demonstrated. Concrete examples taking root in the business process and Android framework are laid out and shown in detail.
A digression on the model checking problem displays the difference of our approach from propositional LTL and other work.