LTL Checker

LTL Checking is the verification of logical-temporal properties on event logs/dataframes. In PM4Py, some parametric rules are made available to check interesting situations, e.g., four eyes principle.

The instructions of this page, when not differently specified, are valid for applications on both logs and Pandas dataframes.

A preliminary step for both applications on logs and Pandas dataframes is the importing of the log/dataframe and of the LTL Checking package. In order to do so for logs:

import os
from pm4py.objects.log.importer.xes import factory as xes_importer
from pm4py.algo.filtering.log.ltl import ltl_checker
log = xes_importer.apply(os.path.join("..", "tests", "input_data", "running-example.xes"))

and for Pandas dataframes:

import os
from pm4py.objects.log.adapters.pandas import csv_import_adapter
from pm4py.algo.filtering.pandas.ltl import ltl_checker
df = csv_import_adapter.import_dataframe_from_path(os.path.join("..", "tests", "input_data", "running-example.csv"))

Warning: this feature is available for logs/Pandas dataframes only in the “ltlCheckerIntegrationBranch”.

Rules

Four Eyes Principle

This rule checkes whether a case has occurrences of A and B done by different resources. This is very important when, by process specification, the two activities shall indeed have different performers.

The rule accepts an optional attribute key, specifying which attribute (activity, resource) shall be considered, and a parameter “positive” that:

  • When True, filters cases having occurrences of A and B done by different resources (non-critical case).
  • When False, filters cases having occurrences of A and B done by the same resource (critical cases).

Example of application of the rule (the cases of the imported dataframe where check ticket and pay compensation are done by the same resource are filtered).

filt_foureyes_neg = ltl_checker.four_eyes_principle(df, "check ticket", "pay compensation", parameters={"positive": False})
A eventually B

This rule checkes whether a case has an occurrences of A followed somewhen in the caseby an occurrence of B.

The rule accepts an optional attribute key, specifying which attribute (activity, resource) shall be considered, and a parameter “positive” that:

  • When True, filters cases that have an occurrence of A followed somewhen in the case by an occurrence of B
  • When False, filters cases that do not have an occurrence of A followed somewhen in the caseby an occurrence of B.

Example of application of the rule (the cases of the imported dataframe having check ticket followed somewhen by pay compensation are filtered):

filt_A_ev_B_pos = ltl_checker.A_eventually_B(df, "check ticket", "pay compensation", parameters={"positive": True})
A eventually B EVENTUALLY C

This rule checkes whether a case has an occurrences of A followed somewhen in the case by an occurrence of B that is followed somewhen in the case by an occurrence of C.

The rule accepts an optional attribute key, specifying which attribute (activity, resource) shall be considered, and a parameter “positive” that:

  • When True, filters cases that have an occurrence of A followed somewhen in the case by an occurrence of B followed somewhen by C
  • When False, filters cases that do not have an occurrence of A followed somewhen in the case by an occurrence of B followed somewhen in the case by an occurrence of C.

Example of application of the rule (the cases of the imported dataframe having check ticket followed somewhen by decide followed somewhen by pay compensation are filtered):

filt_A_ev_B_ev_C_pos = ltl_checker.A_eventually_B_eventually_C(df, "check ticket", "decide", "pay compensation", parameters={"positive": True})
A NEXT B NEXT C

This rule checkes whether a case has an occurrences of A followed directly in the case by an occurrence of B that is followed directly in the case by an occurrence of C.

The rule accepts an optional attribute key, specifying which attribute (activity, resource) shall be considered, and a parameter “positive” that:

  • When True, filters cases that have an occurrence of A followed directlyin the case by an occurrence of B followed directly by C
  • When False, filters cases that do not have an occurrence of A followed directly in the case by an occurrence of B followed directly in the case by an occurrence of C.

Example of application of the rule (the cases of the imported dataframe having check ticket followed directly by decide followed directly by pay compensation are filtered):

filt_A_next_B_next_C_pos = ltl_checker.A_next_B_next_C(df, "check ticket", "decide", "pay compensation", parameters={"positive": True})
Attribute value assumed in events done by different persons

This rule checks whether a case has occurrences of A that are done by different persons (resources).

The rule accepts an optional attribute key, specifying which attribute shall be considered, and a parameter “positive” that:

  • When True, filters cases that have occurrences of A that are done by different persons.
  • When False, filters cases that do not have occurrences of A that are done by different persons.

Example of application of the rule (the cases of the imported dataframe having check ticket done by different persons are filtered):

attr_value_different_persons_pos = ltl_checker.attr_value_different_persons(log, "check ticket",
                                                                          parameters={"positive": True})

.