Source-linked AI summary
Declarative Event-Based Workflow as Distributed Dynamic Condition Response Graphs
Thomas T. Hildebrandt, Raghava Rao Mukkamala
TL;DR
Imperative workflow descriptions can over-constrain process execution, motivating more flexible declarative models for case management and ad hoc business processes. The paper develops Dynamic Condition Response Graphs by generalizing prime event structures with repeated execution, dynamic inclusion and exclusion, and runtime markings, then characterizes finite and infinite runs through Büchi automata.
Problem
Imperative workflow descriptions can over-constrain executions, while declarative models aim to permit any execution that fulfills workflow constraints.
Method
The paper develops distributed Dynamic Condition Response Graphs by generalizing prime event structures with repeated execution, dynamic inclusion and exclusion, runtime markings, and event distribution via roles.
Results
The authors prove that the generalizations conservatively contain the previous model and provide a Büchi-automata mapping characterizing acceptance for finite and infinite runs.
Takeaways & Limitations
DCR Graphs provide a declarative workflow model demonstrated on a Danish hospital example, with graphical runtime-state annotations and a relatively simple execution-state basis.
Abstract
from arXiv · showhide
We present Dynamic Condition Response Graphs (DCR Graphs) as a declarative, event-based process model inspired by the workflow language employed by our industrial partner and conservatively generalizing prime event structures. A dynamic condition response graph is a directed graph with nodes representing the events that can happen and arrows representing four relations between events: condition, response, include, and exclude. Distributed DCR Graphs is then obtained by assigning roles to events and principals. We give a graphical notation inspired by related work by van der Aalst et al. We exemplify the use of distributed DCR Graphs on a simple workflow taken from a field study at a Danish hospital, pointing out their flexibility compared to imperative workflow models. Finally we provide a mapping from DCR Graphs to Buchi-automata.
1 Introduction
The paper motivates declarative workflows as constraint-based models that preserve execution flexibility and are easier to adapt than imperative descriptions. It introduces Distributed Dynamic Condition Response Graphs as a graph-based model extending prime event structures with progress, dynamic behavior, distribution, and runtime visualization.
- Declarative process languages define control flow implicitly through constraints, whereas imperative languages define it explicitly through flows or state-changing commands.
- Declarative models allow any execution satisfying workflow constraints, avoiding the over-constrained control flows that can arise when all possibilities are explicitly modeled.
- Declarative models also support process changes by adding constraints, while imperative descriptions may require rewriting process code.
- The hospital example shows that a simple prescribe;sign sequence loses repeated prescriptions and signatures that a more general imperative model must encode with loops and termination conditions.
- The proposed model seeks an expressive declarative language whose constraints and runtime state are visualizable and directly executable through graph-marking transitions rather than LTL translation.
- Distributed DCR Graphs generalize prime event structures through response relations, repeated execution with dynamic inclusion and exclusion, and role-based distribution of events.
- The paper extends prior work by mapping DCR Graphs to Büchi automata that characterize acceptance for finite and infinite runs using silent transitions.
2 Condition Response Event Structures
Condition response event structures extend prime event structures with response-based progress requirements. The paper shows that these structures preserve ordinary event-structure behavior while also characterizing weakly fair executions.
- The response-based generalization provides an extensional event-based model of progress and elegantly characterizes weakly fair runs.
- A prime event structure contains events, action labels, a partial-order causality relation, and an irreflexive symmetric conflict relation.
- Configurations are event sets satisfying the event-structure conditions, and runs are sequences whose executed-event prefixes form configurations.
- A condition response event structure adds a response relation requiring related events to occur later or become conflicted, plus initially required responses.
- Accepting runs require every pending or initial response eventually to occur or become in conflict.
- With an empty response relation, a prime event structure embeds into a condition response event structure with the same runs and universal acceptance.
- Treating every condition as a response and conditionless events as initial responses yields the same runs and identifies accepting runs with maximal runs, capturing weak fairness.
3 Distributed Dynamic Condition Response Graphs
DCR Graphs generalize event-structure models with repeatable events, dynamic inclusion and exclusion, and markings that capture runtime state. Distributed DCR Graphs add role-based execution, graphical notation, transition semantics, acceptance conditions, and a hospital workflow example.
- Dynamic Condition Response Graphs: DCR Graphs allow events to execute multiple times and use dynamic inclusion and exclusion instead of symmetric conflict.These features support finite representations of infinite behavior and can model skipping events or constraints.
- Dynamic Condition Response Graphs: A DCR Graph marking records executed events, pending responses, and currently included events.The marking is M = (Ex, Re, In), where the three sets capture execution history, required responses, and event inclusion.
- Dynamic Condition Response Graphs: The model uses condition, response, inclusion, and exclusion relations to define graph behavior and runtime updates.Only currently included events are considered when evaluating constraints; transition semantics update markings after event execution.
- Execution Semantics: Runs are accepting when no response event remains continuously included and pending, with finite runs accepted when no pending response is included at termination.Infinite-run acceptance can be represented by mapping DCR Graphs to Büchi automata with τ-events.
- Distributed DCR Graphs: Distributed DCR Graphs assign roles to principals and events, restricting execution to principals assigned a role associated with the event.The distributed transition system preserves the underlying graph states while adding principal, action, and role labels to transitions.
- Hospital Workflow Example: The hospital workflow models prescribe medicine, sign, and give medicine with doctor and nurse roles, while distrust can exclude giving medicine until a new signature.The graphical example permits repeated prescriptions and signatures and uses dynamic exclusion to represent the nurse’s distrust scenario.
4 From DCRGraphs to B¨uchi-automata
The paper maps finite distributed DCR Graphs to Büchi automata with τ-events, preserving both runs and accepting runs. The construction tracks graph markings, ranks pending responses to guarantee progress, and marks accepting states accordingly.
- A Büchi automaton with τ-events represents finite or infinite runs while accepting runs visit accepting states infinitely often.τ-events act as silent delays, allowing finite accepting behavior to be represented by infinite automaton runs.
- A fixed ordering of events ranks pending responses so the construction can enforce their eventual execution or exclusion.The rank mechanism addresses executions with several pending responses by selecting an ordered response obligation.
- The mapping uses graph markings together with a rank index and an acceptance flag to form automaton states.Markings record included, executed, and pending-response events; the index supports progress through pending responses.
- A state is accepting when no included pending responses remain, or when the relevant minimal-ranked pending response is executed or excluded.The acceptance flag is updated from the resulting included and pending-response sets.
- The automaton construction is illustrated for the graph in Fig. 3(a), with state annotations and a stratified view highlighting rank-based progress.The stratified presentation groups states by rank, while the example shows how different pending responses lead to accepting or non-accepting states.
- Theorem 1 states that, for every finite distributed DCR Graph, the corresponding Büchi automaton has the same runs and accepting runs.
5 Related Work
The related-work discussion situates DCRGraphs among logic-based workflow formalisms, Petri nets, and declarative artifact-centric models. It emphasizes differences in verification capabilities, workflow expressiveness, and treatment of pending responses.
- Event Calculus supports workflow enactment and activity iteration but does not support verification of global and temporal workflow constraints.The discussed approach is also limited to imperative or procedural workflow modeling languages.
- Concurrent Transaction Logic and its constraint-based variant express, analyze, schedule, and verify local and global workflow properties.CCTR integrates Concurrent Transaction Logic with Constraint Logic Programming for workflow scheduling.
- Standard Petri nets are widely used for workflows, but they cannot directly express pending responses.The discussion notes established correspondence between event structures and Petri nets while distinguishing DCRGraphs' response semantics.
- Guard-Stage-Milestone models use a declarative life-cycle specification for data-driven, artifact-centric business processes.Their operational semantics are based on Event-Condition-Action rules.
6 Conclusion and Future Work
The paper presents DCRGraphs as a progressively generalized declarative workflow model with distribution, graphical runtime-state notation, and automata-theoretic semantics. It demonstrates flexibility and identifies extensions and compositional verification as future work.
- Conclusion: DCRGraphs extend prime event structures through progress relations, multiple execution, and dynamic inclusion and exclusion of events.The first generalization introduces condition and response relations; the next supports finite representations of infinite behaviours.
- Conclusion: Distributed DCRGraphs assign roles to events and principals, enabling event distribution while retaining graphical runtime-state annotations.The graphical notation is inspired by related work and extended to include markings.
- Conclusion: The authors prove conservative containment of previous models and map DCRGraphs to Büchi automata characterizing acceptance for finite and infinite runs.The mapping provides an automata-theoretic characterization of both finite and infinite executions.
- Conclusion: A stated advantage is that DCRGraphs support relatively simple, directly visualizable runtime-state information compared with more complex logic-based approaches.The authors also report a prototype engine and a mapping to the SPIN model checker.
- Future Work: Future work includes time, exceptions, nesting, data, expressiveness comparisons, interfaces, simulations, and compositional design and verification.The authors also plan to study adaptations and additions of interacting workflow processes.
Acknowlegments
The research was supported by the TrustCare and CosmoBiz projects through Danish Research Agency grants.
- Acknowledgments: The research received support from the TrustCare and CosmoBiz projects and Danish Research Agency grants #2106-07-0019 and #274-06-0415.The acknowledgments provide the associated project websites.