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 of PROM to define our own properties

[Deleted User]
[Deleted User]
edited March 2014 in - Usage

Hello everybody,

I want to define my own LTL properties or LTL templates for new properties (using the LTL language) when using the LTL default checker plug in of PROM 6.3. I read the LTL checker manual of Prom, but I don't understand how can we upload the LTL templates we define in PROM. 

 

Can you help me about this ? 

Thank you.

Best regards. 

Answers

  • JBuijs
    JBuijs

    If I recall correctly the LTL checker comes in 2 plug-in variants: one that uses the standard definitions and one that uses LTL definitions loaded from a file in ProM.
    Using the second variant you can create an .ltl file, load it in ProM and apply the LTL checker on an event log.

    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