TY - CPAPER AB - Artifact-centric systems are a recent paradigm to model and implementbusiness workflows. They describe data, processes, internal and external agents and include mechanisms for data hiding and access control. GSM is a language for the implementation of artifact-centric systems. Since GSM programs have infinitely many states, their verification is challenging. We here present a predicate abstraction technique that enables us to verify GSM programs against richspecifications built on an epistemic, first-order variant of the µ-calculus. We give the theoretical underpinnings of the technique and presentGSMC, the first model checker for GSM that implements SMT-based, three-valued abstraction for GSM. AU - Lomuscio,AR AU - griesmayer,A AU - gonzalez DO - 10.1007/978-3-662-48616-0_16 EP - 268 PB - Springer PY - 2015/// SN - 0302-9743 SP - 253 TI - Verification of GSM-based Artifact-centric Systems by Predicate Abstraction UR - http://dx.doi.org/10.1007/978-3-662-48616-0_16 UR - http://hdl.handle.net/10044/1/25996 ER -