ML Anthology

Dynamic Logic for Data-Aware Systems: Decidability Results

Francesco Belardinelli, Andreas Herzig
IJCAI 2017 pp. 821-827
doi:10.24963/IJCAI.2017/114 /ijcai/2017/belardinelli2017ijcai-dynamic/

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 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.

PDF IJCAI Semantic Scholar

Cite

Text

Belardinelli and Herzig. "Dynamic Logic for Data-Aware Systems: Decidability Results." International Joint Conference on Artificial Intelligence, 2017. doi:10.24963/IJCAI.2017/114

Markdown

[Belardinelli and Herzig. "Dynamic Logic for Data-Aware Systems: Decidability Results." International Joint Conference on Artificial Intelligence, 2017.](https://mlanthology.org/ijcai/2017/belardinelli2017ijcai-dynamic/) doi:10.24963/IJCAI.2017/114

BibTeX

@inproceedings{belardinelli2017ijcai-dynamic,
  title     = {{Dynamic Logic for Data-Aware Systems: Decidability Results}},
  author    = {Belardinelli, Francesco and Herzig, Andreas},
  booktitle = {International Joint Conference on Artificial Intelligence},
  year      = {2017},
  pages     = {821-827},
  doi       = {10.24963/IJCAI.2017/114},
  url       = {https://mlanthology.org/ijcai/2017/belardinelli2017ijcai-dynamic/}
}