Generic, relational transition systems form an interesting class of infinite-state transition systems that naturally captures the execution semantics of a variety of formalisms expressing processes operating over (relational) data. Examples of such data-aware processes include action theories in the situation calculus in AI and data-centric business processes in BPM. In this extended abstract, we summarize the main body of results produced in a decade-long research program focused on the verification of generic, relational transition systems against properties specified using variants of first-order temporal logics.