Modelling History-Dependent Business Processes

Kees van Hee, Olivia Oanea

⋆

, Alexander Serebrenik,

Natalia Sidorova and Marc Voorhoeve

Department of Mathematics and Computer Science

Eindhoven University of Technology

P.O. Box 513, 5600 MB Eindhoven, The Netherlands

Abstract. Choices in business processes are often based on the process history

saved as a log-ﬁle listing events and their time stamps. In this paper we intro-

duce a ﬁnite-path variant of the timed propositional logics with past for speci-

fying guards in business process models. The novelty is due to the introduction

of boundary points start and now corresponding to the starting and current ob-

servation points. Reasoning in presence of boundary points requires three-valued

logics as one needs to distinguish between temporal formulas that hold, those

that do not hold and “unknown” ones corresponding to “open cases”. Finally, we

extend a sub-language of the logics to take uncertainty into account.

1 Introduction

In this paper we consider case management systems, an important and generic class of

Enterprise Information Systems. An important part of a case management system is a

workﬂow management system (WfMS) that takes care of the distribution of work to

agents, which can be either human or application software.

Routing decisions taken by a WfMS can depend on previous observations. For in-

stance, a bank can propose more interesting loan conditions to those customers who

paid off the previous loans on time. We call processes executed by such a WfMS history-

dependent processes. Importance of history-based decisions in workﬂow management

has been recognised in the past [10, 12]. In history-dependent processes actions can be

guarded by conditions on the process history. In this paper we propose a temporal logic

for specifying history-based guards in models of history-dependent processes that we

call LogLogics.

At any given moment of time, history is a ﬁnite object. The inherent incompleteness

of our observations should be taken into account. Consider for example a guard saying

that every bill was paid within four weeks where we would like to obtain true in case

every bill was indeed paid within four weeks, false if there is a bill that was not paid

within four weeks and unknown in case there is a bill issued not later than four weeks

ago which is not paid yet, while the bills issued more than four weeks ago are paid on

time. In some cases the decision on the continuation of the process is made giving the

beneﬁt of the doubt, i.e. unknown leads to the same choice as true in other cases it leads

⋆

Supported by the NWO Open Competitie project MoveBP, Project number 612.000.315

van Hee K., Oanea O., Serebrenik A., Sidorova N. and Voorhoeve M. (2006).

Modelling History-Dependent Business Processes.

In Proceedings of the 4th International Workshop on Modelling, Simulation, Veriﬁcation and Validation of Enterprise Information Systems, pages 76-85

DOI: 10.5220/0002499500760085

 SciTePress

to the same choice as false, and in a number of cases evaluating a guard to unknown

leads to enabling a special procedure to handle the case.

A number of three-valued (untimed) temporal logics, including L-TL, have been

proposed by Nakamura [9] and investigated in [8]. Similarly to L-TL, if a LogLogics-

formula is evaluated to true or false at a given time point, this value cannot be changed

in the future (i.e., when now increases), while unknown can become true or false. Unlike

L-TL, not every LogLogics-formula has to be eventually evaluated to true or false. In-

deed, as we are going to see, there exist LogLogics-formulas φ such that φ will always

be evaluated to unknown.

Since history is a ﬁnite linear sequence of timed events, we consider linear timed

temporal logics (deﬁned on inﬁnite sequences) that have been the subject of intensive

research in the past, starting with [1–3,6]. More recent works on the subject include [4,

13]. Due to the nature of history we need to consider not only future but also past

temporal operators. Therefore, we have chosen to extend timed propositional logic with

past (TPTL+Past) [1–3].

An alternative to TPTL+Past might have been the metric timed logic (MTL) [6,13].

The reasons for opting for TPTL+Past rather than for MTL are twofold. First of all,

TPTL is “more temporal”: it uses real clocks to express timed constraints. This allows

to express such common for EIS constraints as “event p occurred between January 1,

2005 and January 1, 2006”. Unlike TPTL, MTL reasons in terms of distances between

events. Hence, in order to express the same constraint we need to introduce a special

event q that occurred on January 1, 2005 and require that p followed q within one year.

Second, as recently shown in [4] TPTL+Past is strictly more expressive than MTL+Past.

Two different semantics for timed temporal logics can be considered: point-wise

semantics, where formulas are evaluated over discrete sequences of timed events, and

interval-based semantics, where formulas are evaluated over continuous time line [11].

We believe that discrete sequences of timed events are better suited for specifying

history-based guards in business processes and we choose the point-wise semantics.

Although processes we consider are in general not probabilistic processes and his-

tory is not always a reliable source for forecasting the future behaviour (the client who

always paid his bills on time can suddenly go bankrupt), statistical data on history are

still widely used to make choices. Following the observations of [5], we deﬁne a num-

ber of guard patterns for our logic. For these patterns we extend our framework by

introducing certainty values that allow us to check, for instance, whether issued bills

paid on time in 95% of cases.

2 LogLogics

In this section we present LogLogics. LogLogics aims at the modelling of history-

dependent processes based on log-ﬁles. Log-ﬁles usually record series of events such

as “withdraw 100 euro” or “drug A has been administered”. However, when making

decisions, we sometimes would like to reason on states rather than on events, e.g. “the

balance is negative” or “the temperature is higher than 39 degrees”. Therefore, given

an initial state and a series of events presented in a log, we extend the log by replacing

events by pairs (e, s) where e is an event and s is a state after the occurrence of e. For

the initial state, the event is empty. For the sake of readability we refer to these pairs as

states. The set of all states is denoted Σ.

LogLogics is an adaptation of the Timed Propositional Temporal Logic with past [1,

4] to ﬁnite sequences of events limited by two special time points: start and now. The

start point refers to the beginning of observations rather than to the absolute begin.

While such an absolute begin is well-suited for modelling the behaviour of software

systems that have been invoked at some moment of time, it is less appropriate for busi-

ness processes, where the observations could be available for a recent period of time

only. Similarly, now is the last time point where observations are available.

Due to the ﬁniteness of observations, the values of traditional temporal operators can

become unknown. Consider, for instance, a predicate p that is true is a given apple is

green. However, as some apples change colour with time, the fact that during the entire

period of observations the apple stayed green does not necessary imply that “always

green” is true. Nor, in fact does it imply that “always green” is false. In such a situation

we would like to say that the value of “always green” is unknown. To formalise this

intuition we make use of the three-valued logics with truth values false, unknown and

true such that false ≺ unknown ≺ true, min(S) and max(S) are deﬁned for a set S with

respect to ≺, and

false true

unknown

true false

(x∧ y)

def

= min{x, y}

(∃x : x ∈ S : φ(x))

def

= max{φ(x) | x ∈ S}

(∀x : x ∈ S : φ(x))

def

= min{φ(x) | x ∈ S}

Next we introduce the syntax of LogLogics. We assume that a countable set P of

atomic prepositions and a countable set V of clock variables are given. Then, LogLog-

ics-formulas φ are built from atomic propositions, boolean connectives, “until” U and

“since” S operators, clock constraints and clock resets. Intuitively, φ

Uφ

means that at

some point of time in the future φ

holds and till then φ

holds. Similarly, φ

S φ

means

that at some point of time in the past φ

holds and from that point onwards φ

holds.

Finally, clock reset x.φ, also known as “freeze”, sets the value of clock x to the current

time.

Formally, LogLogics-formulas φ are inductively deﬁned as: φ := p | x ∼ y+ c | x ∼

c | x.φ | false | unknown | ¬φ | φ

∧ φ

| φ

Uφ

| φ

S φ

, where x, y ∈ V, p ∈ P, ∼ is one

of <, >, ≤, ≥,=,6= and c ∈ N. We also assume that the abbreviations ∨, ⇒, ⇔, true are

deﬁned as usual.

In order to deﬁne the formal semantics of LogLogics we introduce time sequences

and timed words.

Deﬁnition 1. A time sequence τ = τ

. . . τ

is a ﬁnite sequence of times τ

∈ N, i ∈ N

such that τ

≤ τ

i+1

for all i.

A state sequence σ = σ

. . . σ

is a ﬁnite sequence of states σ

∈ Σ, i ∈ N. For any

atomic proposition p ∈ P and any i ∈ {0, . . . , n}, σ

⊢ p is either true or false.

A ﬁnite timed word ρ = (σ, τ) is a pair consisting of a state sequence σ and a time

sequence τ of the same length n. We also write a timed word as a sequence of pairs

(σ

, τ

). . . (σ

, τ

We assume that start, now ∈ N are two special points such that start ≤ now. Using

the notion of timed state sequences we can introduce the semantics of LogLogics. The

semantics of TPTL+Past has to be adapted to take start and now into account. For the

sake of simplicity, we deﬁne the semantics in the same way it is done for inﬁnite timed

words. For that purpose, for any ﬁnite timed word (σ

start

, τ

start

). . . (σ

now

, τ

now

) we

deﬁne a corresponding inﬁnite timed word . . . (σ

start−1

, τ

start−1

), (σ

start

, τ

start

). . .

(σ

now

, τ

now

), (σ

now+1

, τ

now+1

). . . such that τ

= τ

now

+ (i − now) for i ≥ now and

= τ

start

+ (i − start) for i ≤ start. It should be noted that for a given ﬁnite timed

word there exist inﬁnitely many corresponding inﬁnite timed words. Moreover, σ

⊢ p

is deﬁned to be unknown for any p ∈ P, i 6∈ {start, . . . , now}.

Deﬁnition 2. Let ρ be an inﬁnite timed word. Let i ∈ Z and α : V → R be a partial

valuation for the clock variables. Then

– hρ, i, αi |= p is equal to σ

⊢ p.

– hρ, i, αi |= false is always false;

– hρ, i, αi |= unknown is always unknown;

– hρ, i, αi |= x ∼ c is trueif α(x) ∼ c, and false, otherwise;

– hρ, i, αi |= x ∼ y+ c is true if α(x) ∼ α(y) + c, and false, otherwise;

– hρ, i, αi |= x.φ is equivalent to hρ, i, α[x 7→ τ

]i |= φ;

– hρ, i, αi |= ¬φ is

• true if hρ, i, αi |= φ is false;

• false if hρ, i, αi |= φ is true ;

• unknown, otherwise;

– hρ, i, αi |= φ

∧ φ

• true if hρ, i, αi |= φ

and hρ, i, αi |= φ

are true;

• false if hρ, i, αi |= φ

or hρ, i, αi |= φ

is false;

• unknown, otherwise;

– hρ, i, αi |= φ

Uφ

is equivalent to ∃ j : i ≤ j : (hρ, j, αi |= φ

∧ ∀k : i ≤ k < j :

hρ, k, αi |= φ

);

– hρ, i, αi |= φ

S φ

is equivalent to ∃ j : j ≤ i : (hρ, j, αi |= φ

∧∀k : j ≤ k : hρ, k, αi |=

);

We say that a LogLogics-formula is closed if any occurrence of a clock variable x

is in the scope of a freeze operator “x.”. For instance, x.(x > y+ 1∧ p) is not a closed

formula since y does not appear in the scope of “y.”. One can show that the truth value of

a closed LogLogics-formula is completely deﬁned by the timed word and the time point,

i.e., if φ is a closed LogLogics-formula, then hρ, i, αi |= φ is equivalent to hρ, i, βi |= φ for

any timed word ρ, time point i and clock valuations α and β. From here on we restrict

our attention to closed LogLogics-formulas and write ρ |= φ whenever hρ, now, εi |= φ

where ε is the empty valuation function.

Intuitively, hρ, i, αi |= φ

Uφ

is evaluated to true in the same cases as in the tra-

ditional two-valued logics. It is evaluated to false when either φ

is evaluated to false

everywhere starting from i, or, whenever φ

is evaluated to unknown or true, φ

gets

evaluated to false before. In particular, hρ, i, αi |= pU unknown evaluates to false if and

only if σ

⊢ p is false for some j < i. In all other cases, hρ, i, αi |= pU unknown evaluates

to unknown.

It is evident that although for a given ﬁnite timed word there exist inﬁnitely many

inﬁnite timed words corresponding to it, the truth value of a LogLogics-formula depends

only on the ﬁnite timed word itself:

Lemma 1. Let (σ

start

, τ

start

). . . (σ

now

, τ

now

) be a ﬁnite timed word and let ρ

′

. . . (σ

′

start−1

, τ

start−1

), (σ

start

, τ

start

). . .(σ

now

, τ

now

), (σ

′

now+1

, τ

now+1

). . . and let

′′

= . . . (σ

′′

start−1

, τ

start−1

), (σ

start

, τ

start

). . . (σ

now

, τ

now

), (σ

′′

now+1

, τ

now+1

). . . be

two corresponding inﬁnite timed words. Then, ρ

′

|= φ is equivalent to ρ

′′

|= φ for any

LogLogics-formula φ.

Based on the temporal operators S and U we introduce additional temporal op-

erators “eventually” (♦φ := trueUφ), “always in the future” (φ := ¬(♦¬φ)), “once

in the past” (♦- φ := trueS φ) and “always in the past” (- := ¬(♦- ¬φ)). The following

proposition provides a more direct way to evaluate LogLogics-formulas using the four

additional temporal operators.

Proposition 1. The following statements hold:

– hρ, i, αi |= ♦φ is equivalent to ∃ j i ≤ j ∧ hρ, j, αi |= φ;

– hρ, i, αi |= φ is equivalent to ∀ j i > j ∨ hρ, j, αi |= φ;

– hρ, i, αi |= ♦- φ is equivalent to ∃ j j ≤ i∧ hρ, j, αi |= φ;

– hρ, i, αi |= - φ is equivalent to ∀ j j > i∨ hρ, j, αi |= φ;

Example 1. Let us evaluate the formula - x.(p ⇒ ♦y.(q∧y ≤ x+4)) on the ﬁnite timed

word ρ = ((σ

, 0), (σ

, 1), (σ

, 2), (σ

, 5), (σ

, 8)) such that start = 0, now = 5,

⊢ p is true for i = 1 and i = 4, and false for i ∈ {0, 2, 3, 5}; σ

⊢ q is true for i = 3

and false for i ∈ {0, 1, 2, 4, 5} (see Fig. 1). Intuitively, this formula says that whenever p

was encountered in the past, q was encountered not later than four time units after that.

We need to evaluate this formula with respect to hρ, 5, εi. First, we observe that we

need to minimise hρ, i, εi |= x.(p ⇒ ♦y.(q∧ y ≤ x+ 4)) for all i ≤ 5. This is equivalent

to minimising the value of hρ, i, [x 7→ τ

]i |= p ⇒ ♦y.(q∧ y ≤ x+ 4) for i ≤ 5. For i =

0, 2, 3, 5, hρ, i, [x 7→ τ

]i |= p is false and therefore the implication is true. The cases left

are:

– i = 4.

Since σ

⊢ p is true, the truth value of the implication coincides with the truth value

of hρ, 4, [x 7→ 5]i |= ♦y.(q ∧ y ≤ x + 4). To determine the latter value we need to

maximise the value of hρ, j, [x 7→ 5]i |= y.(q∧ y ≤ x+ 4) for j ≥ 4, i.e., the value of

hρ, j, [x 7→ 5, y 7→ τ

]i |= (q∧y ≤ x+4). For each j ≥ 4 the value of the conjunction

1 2 3 4 5

0 1

2 5 8

f f

f f f t f f

u u

Fig.1. Finite timed word.

1 2 3 4 5

0 1

2 5 8

f f

f f f t f f

u u

Fig.2. Finite timed word.

is the smaller value of hρ, j, [x 7→ 5, y 7→ τ

]i |= q and hρ, j, [x 7→ 5, y 7→ τ

]i |= y ≤

x+ 4.

If j = 4 or j = 5, σ

⊢ q is false and, hence, the value of the conjunction always

coincides with it. If j ≥ 6, σ

⊢ q is unknown. Recall that since j >= now, τ

8+ ( j −5). If j = 6, then τ

= 9 and hρ, j, [x 7→ 5, y 7→ τ

]i |= y ≤ x+ 4 evaluates to

true. Hence, the value of the conjunction in this case is unknown. If j > 6, τ

> 9

and hρ, j, [x 7→ 5, y 7→ τ

]i |= y ≤ x+ 4 evaluates to false. Hence, the smaller value

in this case is false. To determine the value of the implication for i = 4 we should

take the maximal value, which is unknown, obtained for j = 6.

– i = 1. As above, since σ

⊢ p is true, the truth value of the implication coincides

with the truth value of the maximum (on j ≥ 1) of the smaller of the two following

values: hρ, j, [x 7→ 1, y 7→ τ

]i |= q and hρ, j, [x 7→ 1, y 7→ τ

]i |= y ≤ x+ 4.

If j ∈ {1, 2, 4, 5}, then σ

⊢ q is false, and so is the value of the conjunction. If

j ≥ 6 then τ

= τ

+ ( j − 5), i.e., τ

≥ 8 + 1. Hence, hρ, j, [x 7→ 1, y 7→ τ

]i |= y ≤

x+ 4 evaluates to false and the same is true for the conjunction. Finally, for j = 3,

⊢ q is true and τ

= 2 ≤ 1 + 4. Hence, both conjuncts evaluate to true and the

conjunction as well. Hence, the maximal value is true, hρ, 1, [x 7→ 1]i |= ♦y.(q∧y ≤

x+ 4) evaluates to true and the truth value of the implication is true.

– Finally, consider the case i < 0. In this case σ

⊢ p evaluates to unknown. Hence,

the value of the implication is either unknown or true.

It should be noted that we do not need to complete the analysis of the last case, as to

ﬁnd the truth value of the original formula, we need to take the smallest value obtained.

This value is unknown and it is obtained for i = 4. ⊓⊔

Example 1 also explains the true meaning of unknown. The formula is evaluated to

unknown due to the behaviour on the boundaries of the observation sequence. Consider

the ﬁnite timed word in Fig. 2 which differs from the one from Fig. 1 only for i = 4. One

would expect that the response property from Example 1 is evaluated to true, but due to

unknown values before start it still be unknown. In such a case one might like to exclude

the interval before start and/or after now from the consideration. The formulation of the

response property φ that gives true in case all p are followed by q within 4 time units,

unknown in case there are some p within the distance 4 from now that are not followed

by q (yet) and all other p are followed by q within 4 time units, and false in case there are

some p farther than 4 units from now not followed by q can be formulated as following:

φ = - x.(x < τ

start

∨ x > τ

now

∨ (p ⇒ ♦y.(q∧ y ≤ x+ 4))) (1)

This formula is evaluated to unknown for the word from Fig. 1 and to true for the word

from Fig. 2.

Since similar restrictions turn out to be useful for expressing interesting business

properties, we introduce the following short-hand notation:



now

start

x.φ(x)

def

= x.(x < τ

start

∨ x > τ

now

∨ φ(x))

♦

now

start

x.φ(x)

def

= ♦x.(x < τ

start

∨ x > τ

now

∨ φ(x))

-

now

start

x.φ(x)

def

= - x.(x < τ

start

∨ x > τ

now

∨ φ(x))

♦-

now

start

x.φ(x)

def

= ♦- x.(x < τ

start

∨ x > τ

now

∨ φ(x))

Subscripts and superscripts of boxes and diamonds can be omitted when only one of

boundaries is of interest. Using the short-hand notation formula (1) can be written as

-

now

start

x.(p ⇒ ♦y.(q∧ y ≤ x+ 4)). (2)

Lemma 2. Let a restricted LogLogics-formulas ψ be inductively deﬁned as: ψ := p |

x ∼ y+ c | x ∼ c | x.ψ | false | ¬ψ | ψ

∧ ψ

| 

now

start

ψ | -

now

start

ψ | ♦

now

start

ψ | ♦-

now

start

ψ, where

x, y ∈ V, p ∈ P, ∼ is one of <, >, ≤, ≥, =, 6= and c ∈ N. Then ρ

∗

|= ψ is evaluated to

true or false for any extension ρ

∗

of a ﬁnite timed word ρ .

3 Typical Guards of Interest

Dwyer et al. [5] have identiﬁed a number of property speciﬁcation patterns for software

veriﬁcation. In this section we analogously consider LogLogics guard speciﬁcation pat-

terns for business processes.

Occurrence patterns. The ﬁrst pattern concerns the occurrence of a certain desired

event, or dually, the absence of a certain undesirable event. In the most general form

this pattern requires that in a given scope a given event occurs at least a and at most b

times. In particular, if b = 0, the event does not occur at all, and if a equals the number

of time points in a scope, the event occurs through the scope.

Occurrence. For instance, we would like to check that the software license has been

renewed in 2005. To encode this property we write ♦- x.(p∧ x ≥ ’January 1, 2005’∧ x ≤

’December 31, 2005’), where p stands for the licence renewal. In general, this pattern

has the following form: ♦- x.(φ∧ x ≥ t

∧ x ≤ t

). The value unknown is returned in case

] 6⊆ [start, now].

Bounded Occurrence. This pattern is similar to the previous one but requires a certain

event to occur at least k times within a scope:

♦- x

.(φ∧ x

≥ t

∧ x

≤ t

∧

♦- x

.(φ∧ x

≥ t

∧ x

≤ t

∧ x

6= x

∧ . . .

♦- x

.(φ∧ x

≥ t

∧ x

≤ t

∧ x

6= x

∧ . . . ∧ x

6= x

k−1

)))

Variants of this pattern require the event to occur exactly k or at most k times. Using

this pattern we can express the demand that the employee’s salary has been increased

at least three times between January 1, 2000 and January 1, 2006.

Absence. This pattern is dual to the occurrence pattern and can be written as - x.(¬φ(x)

∨x < t

∨ x > t

), where φ denotes an event undesired between time points t

and t

. In

this way we can check that during the last year the daily revenue never fell beyond a

given threshold.

Universality. This pattern allows to express properties that should hold through the

period from t

to t

: - x.(φ(x) ∨ x < t

∨ x > t

Ordering patterns. Ordering patterns can be constructed from the occurrence patterns

by demanding that one of them occurs in a scope within a time slot of another one.

Bounded response. This extremely common pattern (an instance of which we con-

sidered in Example 1) allows us to express such guards as “every bill is paid within

30 days”. In general, the pattern has the following form -

now

start

x.((φ

(x) ∧ π

(x)) ⇒

♦y.(φ

(x) ∧ π

(x, y))), where π

and π

are predicates on the clock values. Require-

ments on business processes typically restrict the value of y from above.

Precedence. The precedence pattern requires that any occurrence of p is preceded by

an occurrence of q within a scope: - x.((φ

(x)∧π

(x)) ⇒ ♦- y.(φ

(x)∧π

(x, y))), where

and π

are predicates on the clock values. For instance, we formulate a guard saying

that every failure is preceded by some speciﬁc event.

Compound patterns. Finally, compound patterns can be constructed from the patterns

above by means of conjunction.

4 Introducing Statistical Values

From here on we restrict our attention to temporal formulas constructed according to

patterns discussed in Section 3. Furthermore, we assume that the formulas have been

rewritten to the negation normal form, i.e. negation is applied to atomic propositions

only.

Now we would like to distinguish between propositions that “hold almost all the

time” and those that “almost never hold”. To this end we redeﬁne the semantics as

function θ from formulas to [0, 1], where 0 corresponds to falsity and 1 to truth. This will

allow us to deﬁne guards that take into account statistical aspects of history rather than

a presence or universality of events. For instance, a bank can propose more interesting

loans to those customers who pay off the previous loans on-time in at least 95% of the

cases. In the current paper we present the reﬁned semantics only for pattern instances

where all formulas are in fact atomic propositions.

To this end we need to determine [0, 1] truth value of a formula φ with respect to the

given timed word ρ, index i and clock valuation α.

Occurrence patterns. Occurrence and bounded occurrence are always mapped either

to 0 or to 1 according to the traditional semantics.

The truth value of hρ, i, αi |= x.(p∧ x ≥ t

∧ x ≤ t

) for universality formulas is

deﬁned as

∑

[σ

⊢p]=true

(τ

i+1

− τ

)

min{now, t

} − max{start,t

}

For absence, replace [σ

⊢ p] = true in the formula above by [σ

⊢ p] = f alse. The

formula says which part of the period of interest the property stayed true/false.

Ordering patterns. Since the sub-formulas are atomic prepositions, π

(x, y) has the

following form π

min

(x) ≤ y ≤ π

max

(x). If one of the inequalities is ommitted we take

the value of x instead. Using this observation we deﬁne the truth value of hρ, i, αi |= φ

for bounded response and precedence as

brp

(i, j, p)

|{ j | ψ

brp

(i, j, p)}|

where ψ

brp

(i, j, p)

def

= (i ≥ j ∧ i ≥ start∧ j ≤ now∧ π

(τ

) ∧ [σ

⊢ p] = true), and ζ

deﬁned as











1 if ∃m :: ξ

brp

( j, m, q) ∧ start ≤ m ≤ now

0 if ¬∃m :: ξ

brp

( j, m, q) ∧ τ

start

≤ π

min

(τ

)∧

max

(τ

) ≤ τ

now

(π

max

(τ

)−τ

now

)+(τ

start

−π

min

(τ

))

max

(τ

)−π

min

(τ

)

otherwise

while ξ

brp

( j, m, q)

def

= (m≃ j∧π

min

(τ

) ≤ τ

≤ π

max

(τ

)∧[σ

⊢ q] = true). For bounded

response ≃ is ≥, for precedence ≃ is ≤. If a restricted form of a pattern is used, start ≤

m ≤ now should be added to the deﬁnition of ξ

brp

( j, m, q).

The value obtained indicates in which percentage of cases the property of interest

holds.

Compound formulas Truth value θ of compound formulas is determined from the truth

values of the sub-formulas according to the following rule:

θ(hρ, i, αi |= φ

∧ φ

)

def

= θ(hρ, i, αi |= φ

) ∗ θ(hρ, i, αi |= φ

)

Example 2. Let φ be -

now

start

x.(p ⇒ ♦y.(q∧ y ≤ x+ 4)) and ρ, start and now as in Ex-

ample 1. This formula is an instance of the bounded response pattern and it is already

normalised, so we can compute the corresponding truth value.

Then, for given now, ψ

brp

holds for j = 1 and j = 4. Hence, the denominator is equal

to 2. If j = 1 there exists m = 3 such that ξ

brp

(1, m, q) and start ≤ m ≤ now. Therefore,

= 1. If j = 4 there is no such m. However, π

max

(τ

), i.e., 5 + 4 = 9 is greater than

now

, and the third case of the deﬁnition of ζ

applies. Hence, ζ

—indeed three

quarters of the expected “responce period” have passed. Summarising these observa-

tions we conclude that the truth value of ρ |= φ is

. ⊓⊔

5 Conclusion

In this paper we have proposed a logics for guards in models of history-dependent

processes. Since at any given moment of time information is ﬁnite and inherently in-

complete, we had to adapt existing timed temporal logics, which resulted in a three-

valued logics, LogLogics, presented above. Moreover, we have shown how guard pat-

terns common for business processes can be expressed in our logics and deﬁned an

additional extension allowing to express certainty of LogLogics-formulas for these pat-

terns.

For the future work we consider creating a compositional generalization of our ex-

tension of the logic with uncertainty that would be applicable to all formulas. We also

plan to create a simple textual language for working with patterns targeted on non-

specialists and to build a tool for checking LogLogics-formulas on history logs. As

shown in [7], the complexity of checking whether a ﬁnite path u satisﬁes an LTL+P

formula ϕ is O(|u| × |ϕ|). Therefore the complexity of checking formulas of our logic

will not form an obstacle for applying it in practice.

References

1. R. Alur and T. A. Henzinger. A really temporal logic. In FOCS, pages 164–169, 1989.

2. R. Alur and T. A. Henzinger. Logics and models of real time: A survey. In J. W. de Bakker,

C. Huizing, W. P. de Roever, and G. Rozenberg, editors, REX Workshop, volume 600 of

Lecture Notes in Computer Science, pages 74–106. Springer, 1991.

3. R. Alur and T. A. Henzinger. A really temporal logic. J. ACM, 41(1):181–204, 1994.

4. P. Bouyer, F. Chevalier, and N. Markey. On the expressiveness of TPTL and MTL. In

R. Ramanujam and S. Sen, editors, FSTTCS, volume 3821 of Lecture Notes in Computer

Science, pages 432–443. Springer, 2005.

5. M. B. Dwyer, G. S. Avrunin, and J. C. Corbett. Patterns in property speciﬁcations for ﬁnite-

state veriﬁcation. In ICSE, pages 411–420, 1999.

6. R. Koymans. Specifying real-time properties with metric temporal logic. Real-Time Systems,

2(4):255–299, 1990.

7. N. Markey and Ph. Schnoebelen. Model checking a path (preliminary report). In R. M.

Amadio and D. Lugiez, editors, Proceedings of the 14th International Conference on Con-

currency Theory (CONCUR’03), volume 2761 of Lecture Notes in Computer Science, pages

251–265, Marseilles, France, Aug. 2003. Springer.

8. O. Morikawa. Extended Gentzen-type formulations of two temporal logics based on incom-

plete knowledge systems. Notre Dame Journal of Formal Logic, 42(1):55–64, 2001.

9. A. Nakamura. On a three-valued logic based on incomplete knowledge systems. Techni-

cal Report 1, Japan Research Group of Multiple-valued Logic, The Institute of Electronics,

Information and Communication Engineers, 1995. Many-Valued Logic Technical Report.

10. Nick, W. M. P. van der Aalst, A. H. M. ter Hofstede, and D. Edmond. Workﬂow resource

patterns: Identiﬁcation, representation and tool support. In CAiSE05. Springer.

11. J.-F. Raskin. Logics, Automata and Classical Theories for Deciding Real-Time. PhD thesis,

Facult

es Universitaires Notre-Dame de la Paix, Namur, Belgium, 1999.

12. S. Rinderle, M. Reichert, and P. Dadam. Correctness criteria for dynamic changes in work-

ﬂow systems - a survey. Data Knowl. Eng., 50(1):9–34, 2004.

13. P. Thati and G. Rosu. Monitoring algorithms for metric temporal logic speciﬁcations. Electr.

Notes Theor. Comput. Sci., 113:145–162, 2005.