Dynamic Logic for Data-aware Systems: Decidability Results

Authors: Francesco Belardinelli, Andreas Herzig

IJCAI 2017 | Conference PDF | Archive PDF | Plain Text | LLM Run Details

Reproducibility Variable Result LLM Response
Research Type Theoretical Most importantly, we develop an abstraction-based verification procedure, thus proving that the model checking problem for Da S against FO-DL is decidable, provided some mild assumptions on the interpretation domain.
Researcher Affiliation Academia Francesco Belardinelli Laboratoire IBISC, UEVE IRIT Toulouse belardinelli@ibisc.fr Andreas Herzig IRIT Toulouse Universit e de Toulouse CNRS herzig@irit.fr
Pseudocode Yes tmp := a; a := b; b := tmp;...α = max := a0; if max < a1 then max := a1; ... if max < an then max := an;
Open Source Code No The paper does not provide any statements about open-source code availability or links to code repositories for the described methodology.
Open Datasets No The paper describes theoretical work and does not use datasets in the context of empirical training or evaluation. The interpretation domain U=Q (rational numbers) is a theoretical construct, not a publicly available dataset for empirical evaluation.
Dataset Splits No The paper describes theoretical work and does not refer to empirical dataset splits for training, validation, or testing.
Hardware Specification No The paper describes theoretical work and does not mention any specific hardware used for experiments.
Software Dependencies No The paper describes theoretical work and does not specify any software dependencies with version numbers.
Experiment Setup No The paper describes theoretical work and does not include details about an experimental setup, hyperparameters, or training configurations.