Solving reachability problems on data-aware workflows
Recent advances in the field of Business Process Management have brought about several suites able to model complex data objects along with the traditional control flow perspective. Nonetheless, when it comes to formal verification there is still the lack of effective verification tools on imperative data-aware process models and executions: the data perspective is often abstracted away and verification tools are often missing. In this paper we provide a concrete framework for formal verification of reachability properties on imperative data-aware business processes. We start with an expressive, yet empirically tractable class of data-aware process models, an extension of Workflow Nets, and we provide a rigorous mapping between the semantics of such models and that of three important paradigms for reasoning about dynamic systems: Action Languages, Classical Planning, and Model Checking. Then we perform a comprehensive assessment of the performance of three popular tools supporting the above paradigms in solving reachability problems for imperative data-aware business processes, which paves the way for a theoretically well founded and practically viable exploitation of formal verification techniques on data-aware business processes.
Code (0)
등록된 구현이 없습니다.
Tasks
ManagementSimilar Papers 제목 키워드 기반
Modeling and Solving Graph Synthesis Problems Using SAT-Encoded Reachability Constraints in Picat
Many constraint satisfaction problems involve synthesizing subgraphs that satisfy certain reachability constraints. This paper presents programs in Picat for four problems selected from the recent LP/CP programming compe…
A Novel Unified Framework for Solving Reachability, Viability and Invariance Problems
The level set method is a widely used tool for solving reachability and invariance problems. However, some shortcomings, such as the difficulties of handling dissipation function and constructing terminal conditions for …
On Grid Graph Reachability and Puzzle Games
Many puzzle video games, like Sokoban, involve moving some agent in a maze. The reachable locations are usually apparent for a human player, and the difficulty of the game is mainly related to performing actions on objec…
SokobanContingency-Aware Planning via Certified Neural Hamilton-Jacobi Reachability
Hamilton-Jacobi (HJ) reachability provides formal safety guarantees for dynamical systems, but solving high-dimensional HJ partial differential equations limits its use in real-time planning. This paper presents a contin…
Time-to-reach Bounds for Verification of Dynamical Systems Using the Koopman Spectrum
In this work, we present a novel Koopman spectrum-based reachability verification method for nonlinear systems. Contrary to conventional methods that focus on characterizing all potential states of a dynamical system ove…