  Formal properties represent a cornerstone of the system-correctness proofs
based on formal verification techniques such as model checking. Formalizing
requirements into temporal properties may be very complex and error prone, due
not only to the ambiguity of the textual requirements but also to the
complexity of the formal language. Finding a property specification language
that balances simplicity, expressiveness, and tool support remains an open
problem in many real-world contexts.
  In this paper, we propose a new temporal logic, which extends First-Order
Linear-time Temporal Logic with Past adding two operators "at next" and "at
last", which take in input a term and a formula and represent the value of the
term at the next state in the future or last state in the past in which the
formula holds. We consider different models of time (including discrete, dense,
and super-dense time) and Satisfiability Modulo Theories (SMT) of the
first-order formulas. The "at next" and "at last" functions can be seen as a
generalization of Event-Clock operators and can encode some Metric Temporal
operators also with counting. They are useful to formalize properties of
component-based models because they allow to express constraints on the data
exchanged with messages at different instants of time. We provide a simple
encoding into equisatisfiable formulas without the extra functional symbols. We
implement a prototype tool support based on SMT-based model checking.
