Dynamic Logic for Data-aware Systems: Decidability Results

Dynamic Logic for Data-aware Systems: Decidability Results

Francesco Belardinelli, Andreas Herzig

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence
Main track. Pages 821-827. https://doi.org/10.24963/ijcai.2017/114

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 the system’s 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 actually decidable, provided some mild assumptions on the interpretationdomain.
Keywords:
Knowledge Representation, Reasoning, and Logic: Geometric, Spatial, and Temporal Reasoning
Knowledge Representation, Reasoning, and Logic: Non-classical logics for Knowledge Representation
Agent-based and Multi-agent Systems: Formal verification, validation and synthesis