OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Dynamic Logic for Data-aware Systems: Decidability Results

Belardinelli, Francesco and Herzig, Andreas Dynamic Logic for Data-aware Systems: Decidability Results. (2017) In: 26th International Joint Conference on Artificial Intelligence (IJCAI 2017), 19 August 2017 - 25 August 2017 (Melbourne, Australia).

(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader

Official URL: 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 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.

Item Type:Conference or Workshop Item (Paper)
Additional Information:https://www.ijcai.org/proceedings/2017/114
HAL Id:hal-03658133
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE)
Other partners > Université Paris-Saclay (FRANCE)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Other partners > Université d'Évry-Val-d'Essonne - UEVE (FRANCE)
Laboratory name:
Deposited On:08 Nov 2018 10:05

Repository Staff Only: item control page