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.
How to Formalize it? | 01:31:36 | |
---|---|---|
Example: Timer Event | 00:14:25 | |
Event-based XOR Revisited | 00:08:23 | |
How to Formalize it? | 00:07:33 | |
What is Formalization? | 00:13:46 | |
Operational Semantics | 00:15:25 | |
Case Study: BPMN | 00:17:18 | |
Translational Semantics for BPMN | 00:14:46 |
Modelling Concurrent Systems | 01:09:07 | |
---|---|---|
What next? | 00:08:35 | |
Motivation | 00:08:06 | |
Process Models and States | 00:12:31 | |
Modeling Systems | 00:17:59 | |
Definition of Path | 00:07:21 | |
State Transitions | 00:14:35 |
Linear Temporal Logic | 01:15:19 | |
---|---|---|
Recap | 00:10:55 | |
Temporal Logic | 00:15:09 | |
Linear Temporal Logic | 00:21:55 | |
Linear Temporal Logic 2 | 00:19:59 | |
What can be expressed in LTL | 00:07:21 |
Computation Trees & Model Checking | 01:17:40 | |
---|---|---|
Computation Trees | 00:15:06 | |
CTL Expressions | 00:17:04 | |
Model Checking | 00:20:16 | |
Büchi Automaton for LTL Formula | 00:14:14 | |
Büchi Automata Composition | 00:11:00 |
Pragmatic Model Checking: From Theory to Implementation | 01:23:51 | |
---|---|---|
Model Checking | 00:11:08 | |
Reduction Techniques | 00:22:13 | |
Effective Model Checking | 00:22:56 | |
Petri Net Model Checking | 00:17:40 | |
How To Use A Model Checker | 00:09:54 |
LTL Model Checking & Compliance Checking | 01:30:52 | |
---|---|---|
LTL Model Checking Example | 00:20:54 | |
LTL Model Checking Example 2 | 00:18:38 | |
Business Process Compliance | 00:11:21 | |
BPMN-Q | 00:18:25 | |
BPMN-Q Patterns | 00:21:34 |
Compliance Checking | 01:22:43 | |
---|---|---|
Exam | 00:07:55 | |
Composition of Patterns | 00:13:49 | |
Process Models to Kripke Structures | 00:13:12 | |
Efficient Compliance Checking | 00:10:41 | |
Reduction of Candidates | 00:10:58 | |
Example Revisited | 00:09:43 | |
Anti-Pattern | 00:16:25 |
Data Aware Compliance Checking | 00:44:58 | |
---|---|---|
Tackling Infinite Domains of Data | 00:12:36 | |
Formalization of Data Access Semantic | 00:15:59 | |
Data Aware Compliance Rules | 00:16:23 |
Conditional Execution Patterns & Consistency of Compliance Rules | 00:57:04 | |
---|---|---|
Conditional Execution Patterns | 00:17:17 | |
Counter Examples | 00:07:19 | |
Consistency of Compliance Rules | 00:11:03 | |
Conflicts | 00:11:52 | |
Vacuous Satisfiability | 00:09:33 |