Download The LTL Checker Plugins a (reference) manual

Chapter 3
The Language to specify
LTL Properties: a reference
3.1
Introduction
Using the Default LTL Checker plugin or the LTL Checker plugin with LTL
Template files created by others is easy as you have read in the previous chapter.
Writing your own LTL Template files is another matter. This chapter tries to
give a full and complete overview of the LTL Language, so that you can specify
your own LTL properties.
Before the language itself is explained, the environment the language operates in is given.
3.2
The Environment in which the Language operates
The LTL Language specifies properties of workflow logs of processes. A process
can be seen as a list of N process instances. Every process instance itself is a
list of M ordered audit trail entries ( Figure 3.1). Actual M can be different
for any process instance. Both audit trail entries and process instances can
have data fields. About audit trail entries we know that there are always a
WorkflowModelElement and an EventType data field, other fields are permitted
too.
17