=Paper=
{{Paper
|id=Vol-1612/paper1
|storemode=property
|title=Plausibility Checking of Formal Business Process Specifications in Linear Temporal Logic
|pdfUrl=https://ceur-ws.org/Vol-1612/paper1.pdf
|volume=Vol-1612
|authors=Christoph Czepa,Huy Tran,Uwe Zdun,Thanh Tran Thi Kim,Erhard Weiss,Christoph Ruhsam
|dblpUrl=https://dblp.org/rec/conf/caise/CzepaTZKWR16
}}
==Plausibility Checking of Formal Business Process Specifications in Linear Temporal Logic==
https://ceur-ws.org/Vol-1612/paper1.pdf
Plausibility Checking of Formal Business Process
Specifications in Linear Temporal Logic
Christoph Czepa1 , Huy Tran1 , Uwe Zdun1 ,
Thanh Tran Thi Kim2 , Erhard Weiss2 , and Christoph Ruhsam2
1
University of Vienna, Faculty of Computer Science, Software Architecture Research Group,
Währingerstraße 29, 1090 Vienna, Austria
{christoph.czepa,huy.tran,uwe.zdun}@univie.ac.at
2
Isis Papyrus Europe AG, Alter Wienerweg 12, 2344 Maria Enzersdorf, Austria
{thanh.tran,erhard.weiss,christoph.ruhsam}@isis-papyrus.com
Abstract. Many approaches for keeping business processes in line with con-
straints stemming from various sources (such as laws and regulations) are based
on Linear Temporal Logic (LTL). Creating LTL specifications is an error-prone
task which entails the risk that the formula does not match the intention of its cre-
ator. This paper proposes a plausibility checking approach for LTL-based spec-
ifications. The proposed approach can provide confidence in an LTL formula
if plausibility checking is passed. If the formula does not pass the plausibility
checks, a counterexample trace and the truth values of both the LTL formula and
the plausibility specification are generated and can be used as a starting point for
correction.
1 Introduction
Keeping business processes in line with requirements stemming from various sources
(e.g., laws, regulations, standards, internal policies, best practices) has become an im-
portant research field due to increasing flexibility demands in business process manage-
ment, especially in knowledge-intensive environments. In recent years, both academia
and industry are working towards solutions for enabling the flexible handling of busi-
ness processes while providing support to meet necessary requirements. Two closely
related categories of such supporting approaches have been extensively investigated.
Firstly, there are compliance enabling approaches developed for checking semantic con-
straints (also called compliance rules) at runtime (e.g., [13]) and design time (e.g., [3])
of business processes. Secondly, constraint-based business processes models (also called
declarative workflows) are defined in which a set of constraints is used to describe the
business process and these constraints become the basis for the enactment of the pro-
cess. A prominent example for the declarative workflow approach is Declare [16] which
provides a graphical front end with mappings to Linear Temporal Logic (LTL) [17]
as underlying formalism3 . Temporal logics, such as LTL and CTL (Computation Tree
3
The graphical notations of Declare can also be translated to other formalisms, such as Event
Calculus [15].
Copyright c by the paper’s authors. Copying permitted only for private and academic pur-
poses.
In: S. España, M. Ivanović, M. Savić (eds.): Proceedings of the CAiSE’16 Forum at the 28th
International Conference on Advanced Information Systems Engineering, Ljubljana, Slovenia,
13-17.6.2016, published at http://ceur-ws.org
CEUR
ceur-ws.org
Workshop ISSN 1613-0073
Proceedings
2 Christoph Czepa et al.
Logic), are established ways to describe desired system properties for verification. Es-
pecially LTL has become a de facto standard for defining system specifications due to its
extensive use in model checking (e.g., [18]) and the possibility to automatically trans-
late LTL formulas to nondeterministic finite automata (NFA) for runtime verification
on finite traces [6].
The creation of LTL formulas is a challenging and error-prone task that requires
considerable knowledge of and experience with LTL. It is hardly surprising that higher
levels of abstraction, such as the property specification patterns proposed by Dwyer
et al. [7], are often preferred over authoring new LTL formulas. There are two major
issues when solely trying to rely on a pattern-based approach. Firstly, formal patterns
that precisely match the intention of the user might not be available. Hence, manually
defining the constraint by modifying or combining existing patterns or by creating a new
specialized LTL formula might be required. Secondly, if an existing candidate pattern
has been identified, how can the user be sure that her or his intention is really met
by the pattern? Either the meaning of the pattern could be misinterpreted or the LTL
formula might contain errors. Such problems in the specifications could result in severe
consequences (e.g., legal issues due to the violation of compliance requirements). Thus,
it is highly important to provide better support for creating correct specifications.
Plausibility checking aims at supporting technical users during the creation process
of LTL formulas and at increasing the confidence in LTL formulas by ensuring that
an LTL specification matches the user’s intention. Whenever an LTL formula is cre-
ated or modified, the user also creates a plausibility specification which is used to check
whether an LTL formula is contradictory to this plausibility specification. The approach
performs reasoning on finite traces by Complex Event Processing (CEP)—with plau-
sibility specifications encoded as Temporal Queries (TQs) on top of Event Processing
Language (EPL)—and Nondeterministic Finite Automata (NFA)—representing LTL
formulas. We discuss the practical use of our approach by the following scenario: The
implementation of a new constraint pattern stemming from an EPA (Environmental
Protection Agency) compliance document [9].
2 Related Work
To the best of our knowledge, only very few studies exist on keeping LTL formulas in
line with the users’ understanding of the formula. Salamah et al. [19] propose to use a
set of manually created test cases to check the plausibility of pattern-generated LTL for-
mulas. However, this involves the user in the generation process of all the sample traces
and the expected truth values at the end of this traces. As a result, the count of test cases
remains marginal because the manual specification of test cases is time-consuming.
Yan et al. [23] claim to keep natural language requirements and their corresponding
formulas consistent by translating specifications in structured English grammar to LTL,
mainly by mapping English words to LTL operators. While the approach provides relief
for specifying discrete time properties, the direct mapping of LTL operators to words
does not really simplify the creation process of LTL specifications. Thus, there is still
the risk to create formulas that contradict the actual intention of the creator.
Plausibility Checking of LTL Specifications 3
Other plausibility checking approaches do not focus on the consistency between
the users’ intention and its actual formal representation in LTL, but check the internal
consistency of LTL formulas (e.g., Barnat et al. [5]). Vacuity detection is concerned
with avoiding tautologies and subformulas that are not relevant for the satisfaction of
the formula (e.g., Simmonds et al. [20]). Consistency checking of LTL formulas means
finding contradicting parts of a formula or contradictions in sets of formulas (e.g., com-
pliance rule collections) that are generally unsatisfiable (e.g., Awad et al. [4]). While
these plausibility checking approaches are also very important, their focus is entirely
different from the approach presented in this paper.
3 Temporal Queries (TQs)
We devise Temporal Queries (TQs) as an abstraction layer on top of EPL (Event Pro-
cessing Language) [10]—an event query language— for supporting plausibility check-
ing. A temporal query is of the form e V r where e is an temporal expression and r is
a truth value. The expression formed by the operator V implies that there is a change
of the truth value caused by the temporal expression e and the resulting truth value is r
which has one of the following states:
– ⊥ stands for temporarily violated,
– > stands for temporarily satisfied,
– ⊥P stands for permanently violated,
– >P stands for permanently satisfied.
The aforementioned set of states is used in Declare [14] and other automata-based
approaches [6] and also proposed for runtime verification of LTL formulas on finite
traces in general [12]. Thus, we adopt these states as they are sufficient for our plausi-
bility checking approach. Once a permanent state is reached for a constraint instance, it
cannot be left anymore.
A temporal expression e can contain events and the following expressions:
– e1 e2 , where both e1 and e2 contain at least one non-negated event, means e1
eventually leads to e2 (‘ ’ is equivalent to the ‘->’ operator in EPL),
– ¬e1 U e2 , where both e1 and e2 contain at least one non-negated event, means e1
does not occur until e2 eventually occurs (‘U’ is equivalent to the ‘until’ operator
in EPL).
Furthermore, a temporal expression e can contain the following boolean operators
and quantifiers:
– ¬e is a negation (not e), initialized as true and changing to false once e occurs,
– e1 ∧ e2 is a logical conjugation (e1 and e2 ),
– e1 ∨ e2 is a logical disjunction (e1 or e2 ),
– ∀e means for every e (‘∀’ is equivalent to the ‘every’ operator in EPL).
For example, the query ∀(a b) V > implies a truth value change to temporarily
satisfied for every time event a is followed by event b. Without the ∀ quantifier, the query
4 Christoph Czepa et al.
(a b) V > observes just the first occurrence where a leads to b and stops thereafter.
The following query a ∀(b c) V > will denote a change to temporarily satisfied
for every occurrence of b leads to c after the first occurrence of a. Another query ∀(a
¬d ∧ ¬b U c d) V ⊥P indicates a change to permanently violated when c is not
preceded by b in between every occurrence of a and d.
4 Plausibility Checking Approach
Authoring LTL formulas usually starts with thinking about some kind of constraint or
requirement in natural language. In this case, the user intends to create an LTL formula
that matches the description in natural language. Alternatively, a natural language de-
scription and the corresponding LTL formula could already be existent and the business
user is interested in finding out whether the LTL formula is a plausible representation of
the natural language description. For the creation of plausibility specifications, we pro-
pose to use Temporal Queries (TQs) which are a way for specifying truth value changes
while observing finite traces, like the execution trace of a business process instance.
Additionally to the creation of the TQs, it is necessary to define the initial truth value of
the specification (i.e., temporarily satisfied or temporarily violated) otherwise the truth
value of the plausibility specification would be undefined until a TQ causes a truth value
change. Up to four TQs, namely one for each possible truth value state (⊥, >, ⊥P , and
>P ), and an initial truth value (either > or ⊥) are defined to represent a plausibility
specification.
Specification PLAUSIBILITY CHECKING
is initially Reference
creates Initial Truth Value
set to Truth Value
Temporal Queries
‹‹transform››
may not
COMPLEX EVENT PROCESSING
deviate
Statements Listeners
creates fire Finite
or Traces
reuses
LTL LTL2NFA NFA Truth Value
Formula determines
‹‹transform››
Fig. 1. Approach Overview
An overview of Plausibility Checking is shown in Figure 1. Plausibility checking
requires two inputs, namely an LTL formula and its corresponding plausibility specifi-
cations. The LTL formula is then transformed into a nondeterministic finite automaton
(NFA). The plausibility specifications consist of an initial truth value and TQs. The TQs
are transformed to event query statements and listeners that can be used by a Complex
Event Processing (CEP) engine.
Plausibility Checking of LTL Specifications 5
In particular, there can be up to four listeners, namely, one for each runtime verifica-
tion state. Once a permanent state is reached, the truth value becomes immutable. Both
the NFA and CEP receive inputs which are the elements of finite traces. These inputs
will lead to changes of both the Truth Value and the Reference Truth Value. A change
of the Reference Truth Value of the plausibility specification occurs once a listener is
triggered because the temporal query matches the current trace. The Truth Value reflects
the current acceptance state of the automaton.
In order to achieve a positive plausibility checking result, there must not be any de-
viation between the Truth Value and the Reference Truth Value for all inputs. A large set
of test cases can be created and checked automatically. There are two options: Option 1:
All words over the alphabet of the NFA having sufficient length can be used as inputs.
A moderate maximum trace length between 7 and 10 is in most cases we encountered
so far already sufficient. Option 2: Only a subset of traces with greater maximum size
is created randomly and checked automatically as well. The alphabet of the automaton
always consists of the variables of the LTL formula and a single additional variable that
functions as a surrogate for all other variables that are not part of the LTL formula. If
the formula does not meet the plausibility specifications, a counterexample trace and
the truth values of both the LTL formula and the plausibility specification are being
made available as a starting point for the correction of the LTL formula. The approach
has been fully implemented in a prototype which makes use of the open source CEP
engine Esper [11] and the LTL2NFA algorithm [6].
In this way, the plausibility checking can be leveraged for aiding users during the
creation of a new constraint patterns as well as for analyzing existing patterns to gain
confidence in the proposed LTL representation of the pattern.
5 Running Example
Pattern collections, most notably the Property Specification Patterns by Dwyer et al. [7],
contain a large number of patterns that fit in many cases. However, such collections are
far from being complete. If no suitable pattern is available to realize a certain constraint,
a new formula must be created. We are now going to illustrate this scenario by a practi-
cal example extracted from our prior research work related to capturing and formalizing
real-world compliance requirements [21].
Let us consider a compliance guidance document [9] published by the United States
Environmental Protection Agency (EPA) regarding buildings built before or after 1978—
since then lead-based paints are prohibited residential and public buildings in USA—
that states “In housing built before 1978, you must: Distribute EPA’s lead pamphlet [...]
to the owner and occupants before renovation starts.”. This rule involves three tasks,
namely, checking whether the house is built before 1978, distributing EPA’s lead pam-
phlets, and starting the renovation process. It makes sense to distribute the lead pam-
phlet in case the house was built before 1978. Hence, a confirmation that the housing
was built before 1978 must coexist with the distribution of lead pamphlets in the same
process instance before the renovation is started. Now we are facing the problem that
the pattern catalog by Dwyer et al. [7] does not introduce Coexistence patterns. The
declarative workflow approach Declare [16], as another important source of patterns,
6 Christoph Czepa et al.
does offer a Coexistence pattern but only in the global- instead of the needed before-
scoped variant. To the best of our knowledge, the Coexistence Before pattern does not
exist, thus it must be newly created. During this process, we will leverage the proposed
plausibility checking approach.
A brief description of the pattern in natural language, such as before c: a coexists
with b, outlines what we aim for. At first, we create appropriate Temporal Queries (TQs)
for the pattern. On the one hand, we need a TQ (a b c) ∨ (b a c) V >P
that turns the truth value to permanently satisfied and another TQ (¬c ∧ ¬b U a
¬b U c) ∨ (¬c ∧ ¬a U b ¬a U c) V ⊥P that turns the truth value to permanently
violated. Creating these formulas is relatively straightforward. The pattern becomes
permanently satisfied when a and b, in any order, occur before c. A permanent violation
of the pattern occurs if one of the following conditions is satisfied.
– there is no c and no b until a occurs and thereafter is again no b until c occurs.
– there is no c and no a until b occurs and thereafter is again no a until c occurs.
On the other hand, we need to create the LTL formula. As soon as we believe that
the LTL formula corresponds to the meaning of the pattern, we can run the plausibility
check. For example, when we perform plausibility checking on F c → ((¬c U a) ∧
(¬c U b)), our approach reports a plausibility issue in relation with the trace [c]. The
plausibility specification is still in its initial state, namely temporarily satisfied while
the LTL formula indicates already a violation. We intended that the formula becomes
only violated if either a exists before c but b does not, or b exists before c but a does not.
Since this is not the case for the trace [c], the plausibility checking approach correctly
identifies an issue. Hence, we must revise the LTL formula. Eventually, we come up
with the formula (F c → ((¬c U a) → (¬c U b))) ∧ (F c → ((¬c U b) → (¬c U a)))
that passes the plausibility checks. Therefore, we have found a plausible representation
of the pattern in LTL. Now, we can encode the compliance requirement in LTL as
(F “Renovation started” → ((¬“Renovation started” U “Housing build before 1978
confirmed”) → (¬“Renovation started” U “Distribute pamphlet finished”)))
∧ (F “Renovation started” → ((¬“Renovation started” U “Distribute pamphlet
finished”) → (¬“Renovation started” U “Housing build before 1978 confirmed”))).
To complete the formalization of the compliance rule, it is additionally required
that an execution of the Housing build before 1978 task happens before the start of
the renovation process. This can be realized by using the already existing Precedence
Global pattern [1].
6 Discussion
Although the motivation and reason for proposing plausibility checking is related to
business process management, the approach is applicable to other domains, such as the
verification of software in general. The current plausibility checking approach assumes
a single state per instant of time which has been sufficient for plausibility checking
Plausibility Checking of LTL Specifications 7
problems that we encountered by now. Multiple states per instant are currently not con-
sidered due to the resulting exponential blowup of traces. Even if working with a single
state per instant, the main drawback of the approach is the exponential growth of the
number of traces. It is, however, in the scenarios we encountered so far, sufficient to
work with moderate maximum trace lengths because the count of propositional vari-
ables that are present in most semantic constraints is usually low (cf. [8]) and most
issues are already discoverable in short traces (cf. Section 6). Alternatively, if LTL for-
mulas involve a high count of propositional variables, the proposed approach still can
perform a large quantity of plausibility checks with randomly generated longer traces,
which is an improvement over generating only a few test cases manually.
7 Conclusion and Future Work
This paper proposes an approach for plausibility checking of LTL specifications based
on Nondeterministic Finite Automata (NFA) and Complex Event Processing (CEP).
The approach has been discussed in the context of a practical scenario, namely the
creation of a new constraint pattern stemming from a compliance document. Existing
pattern-based approaches, such as Declare, can benefit from our approach. Whenever it
becomes necessary to extend the set of supported constraints, our approach can enable
support. Not only runtime verification or declarative workflow techniques can benefit
but also design time approaches since specifications for model checking are often en-
coded in LTL. In our future work, we plan to further evaluate the approach through
performance, scalability and user experiments and to apply our approach to other for-
malisms that have, for example, a notion of quantitative time [2].
Acknowledgement. The research leading to these results has received funding from the FFG
project CACAO, no. 843461 and the Wiener Wissenschafts-, Forschungs- und Technologiefonds
(WWTF), Grant No. ICT12-001. This paper contains an image licensed under CC [22].
References
[1] Property Pattern Mappings for LTL. http://patterns.projects.cis.ksu.
edu/documentation/patterns/ltl.shtml, last accessed: May 18, 2016
[2] Autili, M., Grunske, L., Lumpe, M., Pelliccione, P., Tang, A.: Aligning qualita-
tive, real-time, and probabilistic property specification patterns using a structured
english grammar. Software Engineering 41(7), 620–638 (July 2015)
[3] Awad, A., Decker, G., Weske, M.: Efficient Compliance Checking Using BPMN-
Q and Temporal Logic. In: 6th International Conference on Business Process Man-
agement (BPM). pp. 326–341. Springer, Berlin, Heidelberg (2008)
[4] Awad, A., Weidlich, M., Weske, M.: Consistency checking of compliance rules.
In: Business Information Systems, vol. 47, pp. 106–118. Springer (2010)
[5] Barnat, J., Bauch, P., Brim, L.: Checking sanity of software requirements. In: Soft-
ware Engineering and Formal Methods, LNCS, vol. 7504, pp. 48–62. Springer
(2012)
8 Christoph Czepa et al.
[6] De Giacomo, G., De Masellis, R., Montali, M.: Reasoning on ltl on finite traces:
Insensitivity to infiniteness. In: AAAI. pp. 1027–1033. AAAI Press (2014)
[7] Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for
finite-state verification. In: 21st International Conference on Software Engineering
(ICSE). pp. 411–420. ACM (1999)
[8] Elgammal, A., Turetken, O., van den Heuvel, W.J., Papazoglou, M.: Formalizing
and applying compliance patterns for business process compliance. Software &
Systems Modeling pp. 1–28 (2014)
[9] EPA: Small Entity Compliance Guide to Renovate Right. http://www2.epa.
gov/sites/production/files/documents/sbcomplianceguide.pdf, last
accessed: May 18, 2016
[10] EsperTech Inc.: EPL Reference. http://www.espertech.com/esper/
release-5.1.0/esper-reference/html/event_patterns.html, last
accessed: May 18, 2016
[11] EsperTech Inc.: Esper. http://www.espertech.com/esper/, last accessed:
May 18, 2016
[12] Lichtenstein, O., Pnueli, A., Zuck, L.: The glory of the past. In: Logics of Pro-
grams. pp. 196–218. Springer (1985)
[13] Ly, L.T., Maggi, F.M., Montali, M., Rinderle-Ma, S., van der Aalst, W.M.: Com-
pliance monitoring in business processes: Functionalities, application, and tool-
support. Information Systems 54, 209 – 234 (2015)
[14] Maggi, F.M., Westergaard, M., Montali, M., van der Aalst, W.M.P.: Runtime ver-
ification of ltl-based declarative process models. In: Second International Confer-
ence on Runtime Verification (RV). pp. 131–146. Springer (2012)
[15] Montali, M., Maggi, F.M., Chesani, F., Mello, P., van der Aalst, W.M.P.: Monitor-
ing business constraints with the event calculus. ACM Trans. Intell. Syst. Technol.
5(1), 17:1–17:30 (Jan 2014)
[16] Pesic, M., van der Aalst, W.M.P.: A declarative approach for flexible business
processes management. In: BPM Workshops. pp. 169–180. Springer (2006)
[17] Pnueli, A.: The temporal logic of programs. In: Foundations of Computer Science,
1977., 18th Annual Symposium on. pp. 46–57 (Oct 1977)
[18] Rozier, K.Y.: Survey: Linear temporal logic symbolic model checking. Comput.
Sci. Rev. 5(2), 163–203 (May 2011)
[19] Salamah, S., Gates, A., Roach, S., Mondragon, O.: Verifying pattern-generated
ltl formulas: A case study. In: Model Checking Software, LNCS, vol. 3639, pp.
200–220. Springer (2005)
[20] Simmonds, J., Davies, J., Gurfinkel, A., Chechik, M.: Exploiting resolution proofs
to speed up ltl vacuity detection for bmc. International Journal on Software Tools
for Technology Transfer 12(5), 319–335 (2010)
[21] Tran, T., Weiss, E., Ruhsam, C., Czepa, C., Tran, H., Zdun, U.: Embracing process
compliance and flexibility through behavioral consistency checking in acm: A
repair service management case. In: AdaptiveCM 15 (August 2015)
[22] Wikiphoto: http://www.wikihow.com/Become-a-Software-Engineer, li-
censed under: http://creativecommons.org/licenses/by-nc-sa/3.0/
Last accessed: May 18, 2016
[23] Yan, R., Cheng, C.H., Chai, Y.: Formal consistency checking over specifications
in natural languages. In: DATE ’15. pp. 1677–1682 (2015)