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
Organisation and Introduction | 01:30:49 | |
---|---|---|
Organisation and Introduction | 00:16:55 | |
Modeling Systems | 00:10:42 | |
Specification of Property I | 00:16:45 | |
Detailed Outline | 00:14:34 | |
Petri Net 1 | 00:12:23 | |
Kripke Structures | 00:08:14 | |
Definition of Path | 00:11:16 |
Kripke Structure | 01:29:11 | |
---|---|---|
Big Picture | 00:17:39 | |
State Space | 00:19:04 | |
Derive Kripke Structure | 00:19:09 | |
Paths in transition systems | 00:18:38 | |
Notation | 00:14:41 |
Exercise: Business Process in BPMN | 01:27:36 | |
---|---|---|
Derive Kripke Structure | 00:15:35 | |
Kripke Structures: Next Step | 00:14:52 | |
Kripke Structures: Task C | 00:08:58 | |
LTL (1) | 00:15:33 | |
LTL (2) | 00:17:08 | |
Assignment 3 | 00:15:30 |
Model Checking | 01:26:19 | |
---|---|---|
Model Checking Problem | 00:17:08 | |
Büchi Automata | 00:15:36 | |
Büchi Automata Composition | 00:10:47 | |
Example | 00:20:34 | |
Intersection Automata | 00:22:14 |
Compliance Checking | 01:23:26 | |
---|---|---|
Reaction to New Compliance Rule | 00:17:18 | |
BPMN-Q | 00:21:54 | |
Mapping BPMN to Kripke Structures | 00:12:01 | |
Process Subject to Checking | 00:14:17 | |
Handling Large State Space | 00:17:56 |
Anti Patterns | 01:31:22 | |
---|---|---|
More than Yes/No Answer | 00:21:02 | |
Anti-Patterns | 00:14:55 | |
Matching Anti Patterns to Process | 00:22:10 | |
Data Aware Compliance Checking | 00:17:23 | |
Data Flow Patterns in BPMN-Q | 00:15:52 |
Practice Model Checking | 01:29:30 | |
---|---|---|
Mapping from Kripke Structure to Büchi Automata | 00:12:02 | |
Properties in LTL | 00:19:08 | |
Properties in LTL(2) | 00:16:20 | |
Model Checking | 00:19:08 | |
BPMN-Q | 00:22:52 |
Practise Violation Explanation | 01:26:40 | |
---|---|---|
Refreshing last unit | 00:15:47 | |
Using process knowledge to enhance the performance of TLQ solving | 00:19:33 | |
Generating anti patterns | 00:17:42 | |
Explaining violation to conditional precedence | 00:17:54 | |
Abstracted process | 00:15:44 |
Consistency of Compliance Rules | 01:17:46 | |
---|---|---|
Consistency of Compliance Rules | 00:18:27 | |
Domain Knowledge | 00:18:58 | |
Example | 00:14:49 | |
Process Synthesis | 00:16:11 | |
Precedence Graph | 00:09:21 |
Practice: Data Abstraction | 01:33:39 | |
---|---|---|
Conditions | 00:20:00 | |
Status of Compliance | 00:21:06 | |
Assignment 2 | 00:11:54 | |
Assignment 3 | 00:18:23 | |
Compliance Checker | 00:22:16 |
Checking Approach | 01:15:05 | |
---|---|---|
Checking Approach | 00:18:17 | |
Split | 00:17:52 | |
Precedence Graph | 00:17:07 | |
Joins | 00:14:27 | |
Summary of The BPC Lecture | 00:07:22 |
Exercise | 01:39:04 | |
---|---|---|
Kripke Strukture | 00:21:07 | |
Assignment 1 | 00:14:11 | |
Assignment 2 | 00:11:53 | |
Assignment 2c | 00:15:57 | |
Assignment 3 | 00:16:49 | |
Assignment 4 | 00:19:07 |