ML Anthology

Decidability of Model Checking Non-Uniform Artifact-Centric Quantified Interpreted Systems

Francesco Belardinelli, Alessio Lomuscio
IJCAI 2013 pp. 725-731
/ijcai/2013/belardinelli2013ijcai-decidability/

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.

PDF IJCAI Semantic Scholar

Cite

Text

Belardinelli and Lomuscio. "Decidability of Model Checking Non-Uniform Artifact-Centric Quantified Interpreted Systems." International Joint Conference on Artificial Intelligence, 2013.

Markdown

[Belardinelli and Lomuscio. "Decidability of Model Checking Non-Uniform Artifact-Centric Quantified Interpreted Systems." International Joint Conference on Artificial Intelligence, 2013.](https://mlanthology.org/ijcai/2013/belardinelli2013ijcai-decidability/)

BibTeX

@inproceedings{belardinelli2013ijcai-decidability,
  title     = {{Decidability of Model Checking Non-Uniform Artifact-Centric Quantified Interpreted Systems}},
  author    = {Belardinelli, Francesco and Lomuscio, Alessio},
  booktitle = {International Joint Conference on Artificial Intelligence},
  year      = {2013},
  pages     = {725-731},
  url       = {https://mlanthology.org/ijcai/2013/belardinelli2013ijcai-decidability/}
}