2012/07/10 by Andreas Bauer, Bauer, Andreas, Peter Baumgartner +3
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) #Service-Oriented Architecture and Web Services
paper · pdf · doi:10.48550/arxiv.1207.2461
openalex publication_date 2012/07/10 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.