In this course we look at the problem of business process compliance. Generally, business processes describe the working procedures within an organization.in the mean time, these organizations have to make sure that working procedures follows certain policies and regulations, i.e., compliance rules. Here, we study how to reason about the compliance of business processes with such compliance rules. We base our reasoning on temporal logic. The following topics are covered in the lecture
Business Process Technology | 01:31:30 | |
---|---|---|
BPC Primer | 00:16:50 | |
Petri Nets | 00:11:30 | |
Event-Driven Process Chains | 00:18:07 | |
Business Process Model and Notation | 00:11:35 | |
Sequence Flow - Uncontrolled Flow | 00:18:05 | |
Attached Intermediate Events | 00:15:23 |
Formalizations and Task Structures | 01:31:29 | |
---|---|---|
Big Picture | 00:14:05 | |
Semantics of Formalizations | 00:14:30 | |
Formalization Principles | 00:20:17 | |
Case Study: Task Structures | 00:11:39 | |
Syntax of Task Structures | 00:08:39 | |
Semantics of Task Structures | 00:17:45 | |
Mapping Applied | 00:04:34 |
Modeling Concurrent Systems & Temporal Logics | 01:33:39 | |
---|---|---|
Translational Semantics | 00:13:04 | |
Modeling Concurrent Systems | 00:19:23 | |
Modeling Systems | 00:17:03 | |
Definition of Path | 00:11:20 | |
Derive Kripke Structure | 00:07:59 | |
Temporal Logics | 00:13:39 | |
Temporal Logic: LTL | 00:11:11 |
Temporal Logics | 01:25:00 | |
---|---|---|
Temporal Logics | 00:07:50 | |
Definition of Double Turnstile Relation 1/10 | 00:16:44 | |
Definition of Double Turnstile Relation 7/10 | 00:15:22 | |
What Can be Expressed in LTL? | 00:08:41 | |
Temporal Logic CTL | 00:10:09 | |
AG and EF | 00:09:43 | |
Sample CTL Properties | 00:16:31 |
LTL Model Checking | 01:22:39 | |
---|---|---|
Role of Model Checker | 00:17:50 | |
Next Steps | 00:05:30 | |
Büchi Automaton | 00:08:06 | |
Büchi Automaton for Kripke Structure | 00:10:38 | |
Büchi Automata Composition | 00:10:20 | |
Overall Idea LTL Model Checking | 00:15:05 | |
Immediate Acknowledgement for Every Request? | 00:15:10 |
Compliance Checking | 00:55:50 | |
---|---|---|
CTL Model Checking, Idea | 00:04:50 | |
Compliance Checking | 00:13:10 | |
Patterns for Finite State Verification | 00:08:06 | |
BPMN-Q | 00:14:31 | |
From Petri Net to Kripke Structure | 00:15:13 |
Reduction Rules, Anti Patterns & Data Aware Compliance Checking | 01:14:19 | |
---|---|---|
Handling Large State Space | 00:17:19 | |
Reduction Rules (Cont.) | 00:11:30 | |
Patterns and Anti Patterns | 00:16:41 | |
Matching Anti Patterns to Process | 00:05:26 | |
Data Aware Compliance Checking | 00:09:23 | |
Formalization of Data Access Semantics | 00:14:00 |
Recapitulation and Summary | 01:02:35 | |
---|---|---|
Formalization of Data Access Semantics | 00:14:38 | |
Sample Process 1 | 00:21:29 | |
Sample Process 2 | 00:21:41 | |
Violation Explaination for Data Rules | 00:04:47 |