Abstract
We introduce a first-order extension of dynamic
logic (FO-DL), suitable to represent and reason
about the behaviour of Data-aware Systems (DaS),
which are systems whose data content is explicitly
exhibited in their description. We illustrate the expressivity of the formal framework by modelling
English auctions as DaS and by specifying relevant properties in FO-DL. Most importantly, we develop an abstraction-based verification procedure,
thus proving that the model checking problem for
DaS against FO-DL is decidable, provided some
mild assumptions on the interpretation domain