Dynamic Logic for Data-aware Systems: Decidability Results

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 ex-pressivity of the formal framework by modelling English auctions as DaS and by specifying rele-vant properties in FO-DL. Most importantly, we de-velop 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.