Speciﬁcation of Deterministic Regular

Liveness Properties

Frank Nießner

⋆

telecommunications, networks & security Research Group

Department of Computer Science, University of Fribourg

Boulevard de P

erolles 90, CH–1700 Fribourg, Switzerland

Abstract. Even up-to-date automated verﬁcation techniques are affected by the

fundamental complexity of veriﬁcation algorithms which is caused by necessity

to decide subset conditions on certain languages. These languages are recogniz-

able by nondeterministic B

uchi automata and represent a system behavior and the

desired properties of the system. The involved complementation process may lead

to an exponential blow-up in the size of the automata. In this paper we specify

the structure of a rich subclass of languages that can be characterized by deter-

ministic B

uchi automata and hence be complemented rather easily. Furthermore,

we present examples of practically relevant properties belonging to this language

class.

1 Introduction

The behavior of systems that exhibit temporary perpetual behavior and have the ability

to react to their environment [7] can be appropriately described by regular ω-languages

[10] which are Eilenberg-limits [3] of preﬁx-closed regular languages. Here, the funda-

mental alphabet is the set of actions that may be performed by the considered system

and the system behavior is the set of all inﬁnite action-sequences the system may per-

form. In this context, veriﬁcation describes the process of checking whether the behav-

ior is a subset of an ω-language that contains all the action-sequences representing the

correct behavior of the system. We call this latter language a property.

Properties are as well be characterized by regular ω-languages and B

uchi automata

respectively. Due to the difference between the language-classes which are recognizable

by deterministic and nondeterministic B

uchi automata (the deterministic and nondeter-

ministic regular ω-languages) [2], veriﬁcation becomes a different task since it might

be essential to ‘complement’ the, in general, nondeterministic property-automaton. This

can cause an automaton that is exponentially larger. However, we are able to compute

the complement of a property-automaton rather easily if it is deterministic [8].

Therefore, we investigate deterministic automata and deterministic properties re-

spectively. Even though we consider just a proper subset of all regular ω-languages, this

is no major drawback since deterministic properties contain a large class of practically

⋆

The author is supported by the Hasler Foundation under grant number 1922.

Nießner F. (2006).

Speciﬁcation of Deterministic Regular Liveness Properties.

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

173-178

DOI: 10.5220/0002482601730178

 SciTePress

relevant properties in general [8]. Furthermore, before we begin our considerations, we

will brieﬂy explain that it is sufﬁcient to focus on the particular class of properties called

liveness properties. Properties can be separated due to their intuitive meaning into safety

and liveness properties [1]. It is easy to show that safety properties are closed sets in the

Cantor topology and therefore are always deterministic [6]. Additionally, every prop-

erty can be represented by an intersection of a safety and a liveness property [1]. Taking

into account that determinism of regular ω-languages is preserved under intersection,

we obtain that a characterization of deterministic regular liveness properties sufﬁces to

characterize all deterministic regular properties.

In this paper we will present the structure of deterministic regular liveness properties

in terms of regular preﬁx-free languages and, additionally, we will give some examples

of practically relevant subsets of this class.

2 Preliminaries

We assume the reader is familiar with the common notions of formal language and

automata theory as presented in [4]. For a ﬁnite set of actions Σ, let Σ

∗

be the set of all

ﬁnitely long sequences on Σ, let Σ

be the set of all inﬁnitely long sequences, and let

∞

= Σ

∗

∪ Σ

. A set L ⊆ Σ

∗

is called a (ﬁnitary) language, a set L

⊆ Σ

is called

an ω-language.

Let L

∞

⊆ Σ

∞

. Then pre(L

∞

) = {v ∈ Σ

∗

| ∃w ∈ Σ

∞

: vw ∈ L

∞

} denotes

the set of all preﬁxes of L

∞

. We call a language L ⊆ Σ

∗

preﬁx-closed if and only if

pre(L) = L. Further, the Eilenberg-limit [3] (or limit for short) of a language L ⊆ Σ

∗

is given by lim(L) = {w ∈ Σ

| ∃

∞

v ∈ pre(w) : v ∈ L}.

Let w = σ

. . . ∈ Σ

Then we deﬁne Inf (w ) = {σ ∈ Σ | ∃

∞

i : σ

= σ}.

A ﬁnite state automaton is capable of accepting strings. It is given by a quintuple

A = (Q, Σ, δ, q

, F ), where Q is a non-empty ﬁnite set of states, Σ is a non-empty

ﬁnite set of input symbols, q

∈ Q is the initial state, F ⊆ Q is a set of ﬁnal states, and

δ : Q × Σ → 2

denotes the transition function. We assume the transition function δ

to be extended to 2

× Σ

∗

→ 2

as usual. A is deterministic if |δ(q , σ)| ≤ 1, for each

q ∈ Q, σ ∈ Σ. A tripel (q, σ, p) ∈ Q × Σ × Q s.t. δ(q, σ) ∋ p is a transition of A.

Let v = σ

. . . σ

∈ Σ

∗

and w = σ

. . . ∈ Σ

. A ﬁnite state sequence

ρ(v) = r

. . . r

∈ Q

∗

denotes a ﬁnite run of A on v if δ(r

, σ

i+1

) ∋ r

i+1

for

0 ≤ i < n. The ﬁnite run ρ(v) is successful if r

= q

and r

∈ F . An inﬁnite state

sequence ρ(w) = r

. . . ∈ Q

denotes a run of A on w if δ(r

, σ

i+1

) ∋ r

i+1

for

0 ≤ i. The run ρ(w) is successful if r

= q

and Inf (ρ(w )) ∩ F 6= ∅.

Subject to its acceptance condition, A turns into a ﬁnite automaton or a B

uchi au-

tomaton. If we deﬁne A to accept all v ∈ Σ

∗

such that δ(q

, v)∩F 6= ∅, then A is a ﬁnite

automaton (FA) and L(A) = {v ∈ Σ

∗

| There is a successful ﬁnite run of A on v} is

a regular language. If we deﬁne A to accept each w ∈ Σ

such that there are inﬁnitely

many different v ∈ pre(w) such that δ(q

, v) ∩ F 6= ∅, then A turns into a B

uchi

automaton (BA) and L

(A) = {w ∈ Σ

| There is a successful run of A on w} is a

regular ω-language. Throughout this paper we assume our automata to be reduced, i.e.,

they don’t have useless states or transitions.

Read ‘∃

∞

... : ...’ as ‘there exist inﬁnitely many different ... such that ...’.

174

3 System Behavior, Properties and Veriﬁcation

When we consider the behavior of a reactive system, it would make no sense to al-

low for ﬁnite computations having preﬁxes that are not a ﬁnite behavior as well. Thus,

the language representing the ﬁnite behavior of the system is preﬁx-closed and can be

recognized by a ﬁnite automaton with only accepting states. Furthermore, since it is

reasonable to consider the behavior to be the ‘inﬁnitely continued’ ﬁnite behavior of

the system, we consider the behavior to be the limit of a preﬁx-closed language.

Intuitively, a property partitions Σ

into the set Y ⊆ Σ

of sequences that satisfy

the property and the set N ⊆ Σ

of sequences that do not. For a formal deﬁnition of a

property we simply identify it with the set Y ⊆ Σ

that satisﬁes it. A system behavior

B satisﬁes a property P ⊆ Σ

linearly if and only if B ⊆ P .

Properties can be classiﬁed by their intuitive meaning [5, 1]. There are properties

demanding that ‘nothing undesired will happen’. We call these properties safety prop-

erties. If an undesired action occurs in a computation then this computation, indepen-

dently of further actions, does not satisfy the property. Thus, a property P ⊆ Σ

is called a safety property if and only if from w 6∈ P follows the existence of a

u ∈ pre(w), such that uv 6∈ P for all w, v ∈ Σ

[1]. Another important class of

properties are the liveness properties. These properties demand that ‘a desired action

or action sequence occurs eventually’ but without specifying the point in time and the

number of occurences (once or repeatedly). Furthermore, the possible satisfaction of

the property must be independent of the computation performed so far. This means that

for all ﬁnite computations v ∈ Σ

∗

there must exist an inﬁnite continuation w ∈ Σ

such that vw ∈ P . A reformulation yields [1]: P ⊆ Σ

is a liveness property if and

only if pre(P) = Σ

∗

. The classiﬁcation of properties into safety and liveness properties

is well-founded since a common result from topology states that every property is the

intersection of a safety and a liveness property [1].

Verifying a system means deciding subset conditions of the form B ⊆ P which

can be algorithmically performed by checking B ∩

P = ∅ (where L

= Σ

\ L

However, the problem of complementing B

uchi automata is PSPACE-complete [10]

and may result in an automaton of size up to 2

O(n log n)

[9]. An exponential blow-up

can be avoided if we restrict the properties to be deterministic. Then, a deterministic

uchi automaton sufﬁces to describe a property P and it can be complemented in linear

time, yielding a B

uchi automaton (which is not necessarily deterministic anymore) that

recognizes P and has at most twice as many states (plus one in addition) compared to

the original one [8].

4 Deterministic Regular Liveness Properties

We will now have a closer look on the structure of deterministic liveness properties.

A good point of origin is the well-known speciﬁcation for deterministic regular ω-

languages which is based on regular preﬁx-free languages [3]. Here, a language L ⊆ Σ

∗

is called preﬁx-free if no proper preﬁx of a string in L is in L. It is called maximal

preﬁx-free if it is preﬁx-free and for all w ∈ Σ

∗

\ L holds: L ∪ {w} is not preﬁx-free

anymore. In this case we have pre(L · Σ

∗

) = Σ

∗

. The speciﬁcation is given by

175

Lemma 1. A regular ω-language L

⊆ Σ

is deterministic if and only if there exist

regular preﬁx-free languages U

, V

⊆ Σ

∗

, 1 ≤ i ≤ n such that L

1≤i≤n

· V

A proof can be found in [3]. Instead, we give an intuitive explanation that provides

hints on how to improve this characterization towards a speciﬁcation for deterministic

liveness properties.

Obviously, to each deterministic regular ω-language there exists a deterministic

uchi automaton A = (Q, Σ, δ, q

, F ) that recognizes it. Hence, this automaton has

at least one accepting state, say 1, and, since it accepts inﬁnite action sequences, there

must be at least one loop, i.e., a sequence of transitions that starts and ends in this

accepting state without passing it intermediately. In general, there might be inﬁnitely

many of such sequences. We collect all these sequences in a set, say V

⊆ Σ

∗

. In fact,

is a regular language and it is preﬁx-free, since A is deterministic. Furthermore,

there must exist at least one ﬁnite sequence of transitions that start in q

and ends up in

1. Again, there might be more than just one such sequence (even inﬁnitely many) and

we collect all of them in a set U

⊆ Σ

∗

. Notice that U

is as well regular und preﬁx-free

since A is deterministic. Then U

· V

contains all inﬁnite sequences that A accepts in

state 1. These observasions hold for each accepting state from F = {1, . . . , n} of A.

Thus, L(A) =

1≤i≤n

· V

, where U

, V

⊆ Σ

∗

are regular preﬁx-free languages.

In a certain sense, the determinism is captured in the preﬁx-freedom of the regular

languages U

, V

⊆ Σ

∗

(or vice versa). Due to their determinism, the representation

given in Lemma 1 holds as well for deterministic regular liveness properties. However,

there must exist additional constraints on U

, V

⊆ Σ

∗

that capture the ‘liveness’ of a

property. Recall that P is a liveness property if and only if pre(P) = Σ

∗

. Furthermore,

notice that we can add an arbitrary deterministic regular ω-language to P (determin-

istic regular ω-languages are closed under union) and still have a deterministic regular

liveness property.

Now, let U

, V

⊆ Σ

∗

be regular preﬁx-free languages such that P =

1≤i≤n

. Hence, we must have pre(

1 ≤i≤n

· V

) = Σ

∗

. Some of the U

might be

preﬁxes of a U

, i 6= j, and if this is the case, then we can skip them without destroying

the ‘liveness’ of the rest, i.e., pre(

s∈S

· V

) = Σ

∗

, where S = {1, . . . , n} \ R

and R is the set of indices j such that U

is a preﬁx of a U

, i 6= j. This implies

pre(

s∈S

) · Σ

∗

= Σ

∗

which means that pre(

s∈S

) is maximal preﬁx-free.

Moreover, we must have pre(V

) = Σ

∗

for s ∈ S. From pre(V

) = Σ

∗

follows

pre(V

· Σ

∗

) = Σ

∗

, i.e., the regular languages V

, s ∈ S, must be maximal preﬁx-free,

whereas the V

, r ∈ R are at least preﬁx-free. The deterministic regular ω-language

r∈R

· V

can be considered as addition to that part that still describes a determin-

istic regular liveness property. Thus we obtain the following lemma

Lemma 2. L

is a deterministic regular liveness property if and only if there exist

regular preﬁx-free languages U

, V

⊆ Σ

∗

, 1 ≤ i ≤ n, such that L

1≤i≤n

· V

and there exists a subset L

s∈S

· V

of L

, where S ⊆ {1, . . . , n}, such that

s∈S

and the V

are maximal preﬁx-free for all s ∈ S.

We exemplify the concept using the B

uchi automaton A depicted in Figure 1.

176

a,b

Fig.1. B

uchi automaton A.

Example 1. We have four accepting states (the double-circled ones). The preﬁx-free

sets corresponding to state 2 are U

= (a + ba) and V

= a. Thus, (a + ba) · a

the set of ω-words that A recognizes in state 2. The sets corresponding to state 3 are

= bb, V

= (a + b) and A recognizes bb · (a + b)

in state 3. For state 4 we obtain

= (a + ba)a

∗

b, V

= (a + b)a

∗

b and the ω-language a + ba)a

∗

b · ((a + b)a

∗

The sets corresponding to state 5 are U

= (a + ba)a

∗

b(a + b)a, V

= (ab + b)(a + b)a

and thus the ω-language accepted in state 5 is U

= (a + ba)a

∗

b(a + b)a · ((ab +

b)(a + b)a)

. We observe that U

, U

⊆ pre(U

). Hence, L(A) = L

∪ L

where

= (bb · (a + b)

) ∪ ((a + ba)a

∗

b(a + b)a · ((ab + b)(a + b)a)

) is a deterministic

regular liveness property and L

= ((a + ba) · a

) ∪ (a + ba)a

∗

b · ((a + b)a

∗

) is a

deterministic regular ω-language.

5 Practically Relevant Deterministic Regular Liveness Properties

This section introduces two classes of practically relevant deterministic regular liveness

properties and indicates how they can be extend using Lemma 2. Some of the consid-

erations can as well be found in [8]. From the previous observations follows that the

determinism is captured in the preﬁx-freedom of the involved regular languages. A lan-

guage L is preﬁx-free if and only if no word in L is a proper preﬁx of another word in L

or, in other words, if and only if L \ (L · Σ

) [3]. We denote the operation L \ (L · Σ

)

that establishes the preﬁx-free language corresponding to L by π(L). Observe that for

all regular languages L ⊆ Σ

∗

, π(Σ

∗

· L) is a maximal regular preﬁx-free language.

Furthermore, we obtain from Lemma 2 as a special case the following corollary.

Corollary 1. Let U, V ⊆ Σ

∗

be regular preﬁx-free languages. Then U · V

is a deter-

ministic regular liveness property if and only if U and V are maximal [8].

Using this result we establish the following classes of deterministic regular liveness

properties. Let L ⊆ Σ

∗

be a regular language. Then the ω-language P

evt

= Σ

∗

· L ·

demands a regular pattern in L to occur eventually. P

evt

is a deterministic regular

liveness property since Σ

∗

·L ·Σ

= π(Σ

∗

·L) ·Σ

and Σ is a maximal regular preﬁx-

free language [8]. Thus, by Corollary 1, the assertion follows. In a similar way we can

discuss P

inf

= (Σ

∗

· L)

. P

inf

demands regular patterns in L to occur inﬁnitely often.

Since (Σ

∗

· L)

= (π(Σ

∗

· L))

= π(Σ

∗

· L) · (π(Σ

∗

· L))

, we obtain by Corollary 1

that P

inf

is a deterministic regular liveness property.

Notice that P

evt

and P

inf

represent huge classes of properties since there are no

restrictions on L (except for regularity). For instance, we could replace L by (L · Σ

∗

)

177

where n is a natural number, Kleene star‘*’ or Kleene plus‘+’. All these expressions

describe regular languages and thus P

evt

and P

inf

would remain deterministic regular

liveness properties.

Furthermore, Lemma 2 allows to unify any (ﬁnite) number of such deterministic

regular liveness properties and we still obtain a deterministic regular liveness property.

And there is yet another method to extend these property classes. In the representation

given in Lemma 2, we demand the deterministic regular languages V

to be maximal

preﬁx-free so as to ensure that pre(V

) = Σ

∗

. However, this holds as well for any

deterministic regular liveness property. Thus, in the representation given in Lemma 2

we can replace arbitrarily many V

by P

evt

, P

inf

or any deterministic regular live-

ness property and the result will be a deterministic regular liveness property. Notice the

idempotency of this statement: the resulting deterministic regular liveness property can

again replace one (or arbitrarily many) of the maximal preﬁx-free sets V

. Hence, the

class of deterministic regular liveness properties is rather comprehensive and contains

various practically relevant properties.

6 Conclusion

We have considered in detail the deterministic regular liveness properties, since they

form a subclass of regular liveness properties for which an exponential blow-up in the

number of states can be avoided in the corresponding veriﬁcation process. We presented

a speciﬁcation for these languages and demonstrated the richness of this language class.

References

1. B. Alpern and F.B. Schneider, Deﬁning liveness, Information Processing Letters, 21(4), pp

181-185, 1985.

2. J.R. B

uchi, On a decision method in restricted second order arithmetic, In E. Nagel et al.,

editors, Proceedings of the International Congress on Logic, Methodology and Philosophy of

Science 1960, pp 1-11. Stanford University Press, 1962.

3. S. Eilenberg, Automata, Languages and Machines, volume A, Academic Press, New York,

1974.

4. J. E. Hopcroft and J. D. Ullman, Introduction to Automata Theory, Languages and Computa-

tion, Addison-Wesley Publishing Company, 1979.

5. L. Lamport, Proving the correctness of multiprocess programs, IEEE Transactions on Soft-

ware Engineering, SE-3(2), pp 125-143, 1977.

6. Z. Manna and A. Pnueli, A hierarchy of temporal properties, Proceedings of the 9th Annual

ACM Symposium on Principles of Distributed Computing, ACM Press, pp 377-408, 1990.

7. Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems-

Speciﬁcation, Springer Verlag, New York, ﬁrst edition, 1992.

8. F. Nießner, U. Nitsche, and P. Ochsenschl

ager, Deterministic ω-Regular Liveness Properties,

In Symeon Bozapalidis, editor, Proceedings of the 3rd International Conference on Develop-

ments in Language Theory (DLT’97), pp 237-247, 1997.

9. S. Safra, On the complexity of ω-automata, Proceedings of the 29th Annual IEEE Symposium

on Foundations of Computer Science, IEEE, pp 319-327, 1988.

10. W. Thomas, Automata on inﬁnite objects, in J. van Leeuwen, editor, Formal Models and

Semantics, volume B of Handbook of Theoretical Computer Science, pp 133-191, Elsevier,

1990.

178