Imperial College London


Faculty of EngineeringDepartment of Computing

Professor of Logic for Multiagent Systems



+44 (0)20 7594 8414a.lomuscio Website




569Huxley BuildingSouth Kensington Campus






BibTex format

author = {Lomuscio, AR and Michaliszyn, J},
pages = {488--497},
publisher = {AAAI Press},
title = {Model Checking Unbounded Artifact-Centric Systems},
url = {},
year = {2014}

RIS format (EndNote, RefMan)

AB - Artifact-centric systems are a recent paradigm for represent-ing and implementing business processes. We present furtherresults on the verification problem of artifact-centric systemsspecified by means of FO-CTL specifications. While the gen-eral problem is known to be undecidable, results in the lit-erature prove decidability for artifact systems with infinitedomains under boundedness and conditions such as unifor-mity. We here follow a different approach and investigate thegeneral case with infinite domains. We show decidability ofthe model checking problem for the class of artifact-centricsystems whose database schemas consist of a single unaryrelation, and we show that that the problem is undecidable ifartifact systems are defined by using one binary relation ortwo unary relations.
AU - Lomuscio,AR
AU - Michaliszyn,J
EP - 497
PB - AAAI Press
PY - 2014///
SP - 488
TI - Model Checking Unbounded Artifact-Centric Systems
UR -
UR -
ER -