To prevent spam users, you can only post on this forum after registration, which is by invitation. If you want to post on the forum, please send me a mail (h DOT m DOT w DOT verbeek AT tue DOT nl) and I'll send you an invitation in return for an account.

Using LTL model checker to define our reliability properties

glauciamelissa
glauciamelissa
in - Usage
Dear, I would like to create some properties to define reliability properties. I want to know how many times the task has happened and how many times the task has completed successfully. For example, I have the following event log:

(1) task T1, eventtype start
(1) task T1, eventtype complete
(1) task T2, eventtype start
(1) task T2, eventtype complete
(2) task T1, eventtype start
(2) task T1, eventtype complete
(2) task T2, eventtype start
(2) task T2, eventtype complete
(3) task T1, eventtype start
(3) task T1, eventtype complete
(3) task T2, eventtype start
(3) task T2, eventtype complete
(4) task T1, eventtype start
(5) task T1, eventtype start
(6) task T1, eventtype start
(6) task T1, eventtype complete
(6) task T2, eventtype start

task T1 happened 6 times, but it only has finished in 4 times
task T2 happened 4 times, but it only has finished in 1 once

Could I represent these information in some properties LTL?

Thank you for your attention.

Comments

  • JBuijs
    JBuijs
    Hi,

    You could create a simple model that says when T1 starts, it should also end (same for T2), and then calculate the conformance of the event log to this model.
    In this case you could even create a Petri net that expresses this, and calculate an alignment on this.
    Joos Buijs

    Senior Data Scientist and process mining expert at APG (Dutch pension fund executor).
    Previously Assistant Professor in Process Mining at Eindhoven University of Technology
Sign In or Register to comment.

Howdy, Stranger!

It looks like you're new here. If you want to get involved, click one of these buttons!

Sign In Register

Categories

In this Discussion