Imperial College London

ProfessorAlessioLomuscio

Faculty of EngineeringDepartment of Computing

Professor of Logic for Multiagent Systems
 
 
 
//

Contact

 

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

 
 
//

Location

 

504Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@inproceedings{Lomuscio,
author = {Lomuscio, AR and Michaliszyn, J},
pages = {488--497},
publisher = {AAAI Press},
title = {Model Checking Unbounded Artifact-Centric Systems},
url = {http://www.aaai.org/Press/Proceedings/kr14.php},
}

RIS format (EndNote, RefMan)

TY  - CPAPER
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
SP - 488
TI - Model Checking Unbounded Artifact-Centric Systems
UR - http://www.aaai.org/Press/Proceedings/kr14.php
UR - http://hdl.handle.net/10044/1/26815
ER -