---
title: "Decidability of Model Checking Non-Uniform Artifact-Centric Quantified Interpreted Systems"
authors:
  - "Francesco Belardinelli"
  - "Alessio Lomuscio"
doi: ""
url: "https://ijcai.org/proceedings/2013/114"
pdf: "https://ijcai.org/proceedings/2013/0114.pdf"
venue: "Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence"
year: 2013
pages: "725-730"
track: ""
keywords:
---

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

Francesco Belardinelli, Alessio Lomuscio

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