LTL Checker

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

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})

.