---
# System prepended metadata

title: (Old) Mail til Jiri and Peter (05/10-20)

---

# (Old) Mail til Jiri and Peter (05/10-20)

## Hvat hava vit gjørt seinastu vikuna?

### Hvat er longu gjørt í feltinum?

### Hvørji features supportera forskellig WFMS tól (feature tabell)?

* YAWL (Yet Another Workflow Language) extends Petri nets with concepts for multiple instances (where at runtime a task may have multiple instances active at the same time), the generalised OR-join (where a construct only waits for further triggers if these can indeed arrive) and cancellation (where a collection of activities can be terminated through the execution of a certain task).
* Van der Aalst's open source platform for process mining (small application, plug-in architecture)
* Aris Process Performance Manager
* Celonis Discovery: Big commercial process mining product suite
* BAB (Best Analytics of Big Data): Doesn't seem relevant to us
* rapidProM: Extends rapidminer with features from ProM
* SNP Business Process Analysis: iPad app, didn't research more

| |Games|Timed|Soundness|Process Mining|
|-|--------|-----|-----|---------|--------------|
|YAWL|Probably not|Probably|Don't know|Think so|
|ProM|Not the platform itself|Not the platform itself|Not the platform itself|Not the platform itself|
|Aris Process Performance Manager||yes||yes|

| #                                | Petri nets | Games | Timed | Soundness | PD | PM |
|:---------------------------------|:----------:|:-----:|:-----:|:---------:|:--:|:--:|
| YAWL                             |      ✔️     |   ❓  |   ⁉️   |     ❓    | ❓ |  ⁉️ |
| ProM                             |      ✔️     |   ❌  |   ⁉️   |     ❓    | ❓ |  ⁉️ |
| Aris Process Performance Manager |     ❓     |   ✔️   |   ⁉️   |      ✔️    | ❓ | ❓ |
| Celonis Discovery                |     ❓     |   ❓  |   ✔️   |      ⁉️    |  ✔️ |  ✔️ |
| BAB (Best Analytics of Big Data) |     ❓     |   ❓  |   ❓  |     ❓    | ❓ | ❓ |
| Myivenio                         |      ⁉️     |   ❓  |   ⁉️   |      ⁉️    |  ✔️ |  ✔️ |
| Perceptive Process Mining        |      ⁉️     |   ❓  |   ⁉️   |      ⁉️    |  ✔️ |  ✔️ |
| Process Gold                     |      ⁉️     |   ❓  |   ⁉️   |      ⁉️    |  ✔️ |  ✔️ |
| QPR ProcessAnalyzer              |      ⁉️     |   ❓  |   ⁉️   |      ⁉️    |  ✔️ |  ✔️ |
| rapidProM                        |      ⁉️     |   ❓  |   ⁉️   |      ⁉️    |  ✔️ |  ✔️ |
| SNP Business Process Analysis    |
| Signavio Process Intelligence    |      ✔️     |
| UpFlux                           |      ✔️     |

Where:
* ❓: We don't know'
* ⁉️: We're not completely sure, but propbably
* ❌: Negative
* ✔️: Affirmative
* PD: Process Discovery
* PM: Process Mining

| # | Environment | Soundness | Time | Stochastic | Resources | Free Choice |
|:-------- |:------------------:|:------------------:|:-:|:-:|:-:|:-:|
| Eshuis03 | :heavy_check_mark: | :heavy_check_mark:  | :heavy_multiplication_x: | :heavy_multiplication_x: | :heavy_multiplication_x: | :heavy_check_mark: |
| Lehrstuhl I7 | :heavy_check_mark: | :heavy_check_mark: | :heavy_multiplication_x: | :heavy_multiplication_x: | :heavy_multiplication_x: |:heavy_check_mark: |
 
 
 ||Short description|Workflow analysis|Timed|Games|Stochasticity|Soundness|Other soundness?|Any process mining/BPM functionality?|
 |-|-|-|-|-|-|-|-|-|
|TAPAAL|yee|:heavy_check_mark:|:heavy_check_mark:|:heavy_check_mark:|:heavy_multiplication_x:|:heavy_check_mark:|Soundness wrt time (strong soundness)|:heavy_multiplication_x:|
|enPAC|PN model checker for LTL primarily|:heavy_multiplication_x:|:heavy_multiplication_x:|:heavy_multiplication_x:|:heavy_multiplication_x:|:heavy_multiplication_x:|:heavy_multiplication_x:|:heavy_multiplication_x:|
|GreatSPN|Mainly focused on timed and stochastic PN analysis|:heavy_multiplication_x:|:heavy_check_mark:|:heavy_multiplication_x:|:heavy_check_mark:|:heavy_multiplication_x:|:heavy_multiplication_x:|:heavy_multiplication_x:|
|LoLA|PN model checker. Supports CTL*|:heavy_multiplication_x:|Don't think so. Not 100% sure|:heavy_multiplication_x:|:heavy_multiplication_x:|Think so|Don't know|:heavy_multiplication_x:|
|ITS-Tools|Model checker that can take a lot of different formalisms in (e.g., UPPAAL timed automata). Converts it to GAL (Guarded Action Language).|Don't know|:heavy_check_mark:|Don't know|Don't know|Don't know|Don't know|:heavy_multiplication_x:|
|LTSMin|Structurally similar to ITS-Tools|Not from what i can see|Not timed PNs|Supports parity games (however don't know in which formalism)|Not for PNs|:heavy_check_mark:|Don't think so|:heavy_multiplication_x:|
|Tina|Model checker for Timed PNs|:heavy_multiplication_x:|:heavy_check_mark:|:heavy_multiplication_x:|:heavy_multiplication_x:|Don't think so|Don't think so|:heavy_multiplication_x:|
 
### Hvørja nichè'u kunnu vit útfulla sum resulterar frá omanfyristandandi?

### Hvørja case study hava vit (upp)funnið sum motivation fyri projektið?

#### Hvussu hava vit (upp)funnið tað?
_(logs db -> process mining tool -> wf net við games)_

## Hvat forvanta vit at snakka um í vegleiðarafundinum?

## Og hvat forvanta vit at fáa burturúr vegleiðarafundinum?
