2018/06/29 by Diego Calvanese, Silvio Ghilardi, Calvanese, Diego +7
Business, Management and Accounting · Computer Science · #Business Process Modeling and Analysis #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Security and Verification in Computing #Semantic Web and Ontologies
paper · pdf · doi:10.48550/arxiv.1806.11459
openalex publication_date 2018/06/29 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We study verification over a general model of artifact-centric systems, to\nassess (parameterized) safety properties irrespectively of the initial database\ninstance. We view such artifact systems as array-based systems, which allows us\nto check safety by adapting backward reachability, establishing for the first\ntime a correspondence with model checking based on\nSatisfiability-Modulo-Theories (SMT). To do so, we make use of the\nmodel-theoretic machinery of model completion, which surprisingly turns out to\nbe an effective tool for verification of relational systems, and represents the\nmain original contribution of this paper. In this way, we pursue a twofold\npurpose. On the one hand, we reconstruct (restricted to safety) the essence of\nsome important decidability results obtained in the literature for\nartifact-centric systems, and we devise a genuinely novel class of decidable\ncases. On the other, we are able to exploit SMT technology in implementations,\nbuilding on the well-known MCMT model checker for array-based systems, and\nextending it to make all our foundational results fully operational.\n