We describe an approach to modelling and reasoning about data-centric business processes and present a form of general model checking. Our technique extends existing approaches, which explore systems only from concrete initial states.

Specifically, we model business processes in terms of smaller fragments, whose possible interactions are constrained by first-order logic formulae. In turn, process fragments are connected graphs annotated with instructions to modify data. Correctness properties concerning the evolution of data with respect to processes can be stated in a first-order branching-time logic over built-in theories, such as linear integer arithmetic, records and arrays.

Solving general model checking problems over this logic is considerably harder than model checking when a concrete initial state is given. To this end, we present a tableau procedure that reduces these model checking problems to first-order logic over arithmetic. The resulting proof obligations are passed on to appropriate “off-the-shelf” theorem provers. We also detail our modelling approach, describe the reasoning components and report on first experiments.

Model Evolution is a lifted version of the propositional DPLL procedure for first-order logic with equality. This paper combines and extends the essentials of the latest Model Evolution variants with and without theory reasoning into a new calculus. The new calculus is described in detail. The main results reported here are the calculus' completeness under (unavoidable) conditions, and its application as a decison procedure for the quantifier-free fragment of the combined theory of free function symbols with equality and linear integer arithmetic.