Decidability of Model Checking Non-Uniform Artifact-Centric Quantified Interpreted Systems
Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence. Pages 725-730.
Abstract
Artifact-Centric Systems are a novel paradigm in service-oriented computing. In the present contribution we show that model checking bounded, non-uniform artifact-centric systems is undecidable. We provide a partial model checking procedure for artifact-centric systems against the universal fragment of a first-order version of the logic CTL. We obtain this result by introducing a counterpart semantics and developing an abstraction methodology operating on these structures. This enables us to generate finite abstractions of infinite artifact-centric systems, hence perform verification on abstract models.
@inproceedings{ijcai2013p114,
title = {Decidability of Model Checking Non-Uniform Artifact-Centric Quantified Interpreted Systems},
author = {Belardinelli, Francesco and Lomuscio, Alessio},
booktitle = {Proceedings of the Twenty-Third International Joint Conference on
Artificial Intelligence, {IJCAI-13}},
publisher = {AAAI Press / International Joint Conferences on Artificial Intelligence},
editor = {Francesca Rossi},
pages = {725--730},
year = {2013},
month = {8},
url = {https://ijcai.org/proceedings/2013/114},
}
TY - CPAPER TI - Decidability of Model Checking Non-Uniform Artifact-Centric Quantified Interpreted Systems AU - Belardinelli, Francesco AU - Lomuscio, Alessio T2 - Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence, IJCAI-13 PB - AAAI Press / International Joint Conferences on Artificial Intelligence PY - 2013 SP - 725 EP - 730 UR - https://ijcai.org/proceedings/2013/114 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
