Checking Simple Properties of Transition Systems Defined by Thue Specifications.
In (possibly infinite) deterministic labeled transition systems defined by Thue congruences, labels are considered as functions of states into states. This paper provides a method for computing domains of such functions for a large class of transition systems. The latter are related to model checking of transition systems defined by Thue congruences.
Introduction
Countable transition systems can model any software or digital hardware system and appear
as one of the most fundamental structures in computer science. While the research on finite
transition systems has a long tradition (see e.g. [1] for further references), infinite transition
systems have only recently attracted attention of computer scientists. One of the basic
problems concerning infinite transition systems is their effective description. We argue that
Thue systems may be used for defining both finite and infinite transition systems and semi-
Thue systems may be used as mechanization tools for reasoning about underlying transition
systems.
When a transition system models a real-life system, the properties of the latter correspond
to the theory of the transition system within some suitable logic. The falsity of a sentence
on a given transition system amounts to the emptiness of a certain set, namely the meaning
of the sentence. Roughly speaking, this set is obtained as a combination of the elementary
relations that interpret atomic formulae. Such a combination is computable whenever so are
elementary relations and the operators of the logic are simple enough. In particular, this is
the case for the Hennessy-Milner logic [9] where the elementary relations are unary and the
operations are boolean ones. To establish the truth of a sentence, the central problem is then
to compute the elementary relations. This is the subject of the present paper.
Our work is related to the well established grounds of formal verification which are based
on the connections between logic and formal languages (see e.g. [19]). In that approach, the
truth of a sentence on a finite transition system is checked using automata-theoretic con-
structions, and is decidable. The transition systems considered here are more general and
possibly infinite. As a consequence, the relations interpreting atomic formulae are not always
computable. In this situation, the truth is no more decidable. We thus fall into a common
pattern of various areas of automated reasoning where deduction rules do not yield an algorithm
but rather a not always terminating procedure. We follow a similar approach to the
problem which is a first step towards formal verification of what we call Thue specifications,
and may be summarized as follows.
The semantics of a Thue specification is given as a labeled transition system, the states
of which form a language over an alphabet \Sigma and labels belong to an alphabet \Gamma . Each label
a in \Gamma corresponds to an event and may be seen as a partial function of states. As in a Hoare
triple [']P [/], where the domain (resp. range) of a partial function associated to a program
P is restricted by a precondition ' (resp. postcondition /), an event a 2 \Gamma may be restricted
to a partial function of X into U where X and U are some subsets of the set of states. This is
written a: X!U . Besides letters of \Gamma , the words over \Gamma may be seen as functions. This leads
to the word-functions of the form u: X!U with . The problem studied in this paper is
that of finding the maximal subset X 0 of X on which u is defined and u(X 0 ) ' U . However, the
only solutions of interest are those which may readily be subject to boolean operations, and
for which the emptiness problem is decidable. Within the Chomsky hierarchy, only rational
languages satisfy both requirements. This leads us to the problem of determining the domain
of u: X!U whenever it is rational, assuming that both X and U are also rational. To solve
this problem, we introduce a procedure that is given under the form of three deduction rules
that derive a system of left-linear (language) equations from a word-function u: X!U . If the
procedure terminates, the least solution of the resulting system of equations is the domain of
u: X!U .
In deduction rule-based automated reasoning, the most fundamental issues are soundness
and completeness [20]. While the soundness is an obvious requirement, the completeness may
be out of range in certain situations. Unlike the set of consequences of a finite set of axioms,
the theory of a single structure need not be recursively enumerable. For instance, since the
theory of the standard model of arithmetics is undecidable (see e.g. [17]), by the Turing-Post
Theorem, one concludes that this theory is not recursively enumerable. A complete method
for deciding the truth of a sentence cannot exist in such a case. This limitation is well known
in the area of inductive theorem proving (see e.g. survey [4]). Similarly, the problem studied in
this paper is not recursively enumerable, hence the procedure introduced here is not complete.
In particular, this procedure is not guaranteed to terminate on each instance of the problem
which has a rational solution. Nevertheless, we establish a reasonably weak sufficient condition
for the termination and we show that this condition is satisfied by several well-known classes
of semi-Thue systems for which the termination is expected.
This paper is organized as follows. In Section 1 basic notions from language theory and
string rewriting are recalled. Section 2 introduces Thue specifications and their models. The
main problem of the paper is stated in Section 3 and is related to the Hennessy-Milner logic.
In Section 4 a procedure that treats the problem is provided. Section 5 is devoted to the
correctness of the procedure. In Section 6 it is established that the problem is not recursively
enumerable and a reasonably weak condition for the termination of the procedure is provided.
The techniques developed in the paper are applied in Section 7 to an example of a simple
railway network. Brief conclusions close the paper.
Assuming a minimum theoretical background from rational languages [16] and string-rewrit-
ing [6], we recall in this section several notions from these topics and we set some notations
for the sequel. The family of rational languages over an alphabet \Sigma is written Rat(\Sigma   ) and
the family of the rational subsets of a language L ' \Sigma   is written Rat(L), viz
stands for the powerset of L.
Systems of equations We speak of rational expressions in the usual meaning but we also use
rational expressions with variables. The variables are written are assumed
to form an infinite, countable set. Subsequently we shall often replace variables in a given
rational expression R (resp. set of equations E ) with some rational expressions (possibly with
variables) by applying a substitution oe on it. The resulting expression (resp. set of equations)
is written Roe (resp. E oe). A substitution of a single variable X by an expression P may be
its application on an expression R (resp. set of equations E) is written
A (left) linear system of equations is a set of equations such that, for each variable, there
is at most one equation with this variable as lefthand side and each equation is of the form
where Y is a rational expression, each Y i is a rational expression denoting a nonempty set and
are variables. In such an equation, Y is called constant term. We say that the system
of equations E is balanced if, for each variable X of the system, there is exactly one equation
in E with X as lefthand side.
Among all solutions of E with respect to (w.r.t.) a given variable X we distinguish the least
solution (w.r.t. inclusion). It is well known that a balanced linear system of n equations has
a least solution w.r.t. any of its variables. One may compute such a solution using the Gauss
elimination method. For more details related to this topic the reader may consult e.g. [3].
Suffixes, prefixes, quotients and remainders Given u; v; w 2 \Sigma   such that
is called a prefix and v a suffix of w. When v 6= " (resp. u 6= "), u (resp. v) is a proper prefix
suffix ) of w. We note pref (u) (resp. suff (u)) the set of all the prefixes (resp. suffixes) of
a word u. These notations are extended to sets; for instance, given X ' \Sigma   , pref (X) stands
for
u2X pref (u). When words x and z, then y is called a factor of w.
When xz 6= ", y is an proper factor of w.
The (right) quotient (resp. remainder) of M ' \Sigma   by N ' \Sigma   , written M=N (resp. MiN)
is defined as follows
resp.
As we will see further, some steps of the procedure that is the main point of this paper
depend on computations of quotients and remainders between rational languages. Remember
that the family of rational languages is closed under both quotients and remainders [10].
String rewriting A semi-Thue system (sts) S over an alphabet \Sigma is a binary relation on
di of S, also noted g ! d, is called a rule; l(r) (resp. r(r)) stands for the
lefthand (resp. righthand) side of r, i.e. g (resp. d). The latter notation is extended on sets of
pairs (e.g. binary relations, functions etc.), especially l(S) denotes the domain and r(S) the
range of S. An sts S is
1. special if
2. monadic if r(S) ' A [ f"g and jlj ? jrj for each (l; r) 2 S,
3. left-basic if for all x;
2 r(S) and for all x;
reduction relation "!
" on \Sigma   is associated with S in the usual way, namely !
and the rewrite relation is the reflexive-transitive closure
of !
. A word is said to be reducible (resp. irreducible) w.r.t. S when it belongs
(resp. does not belong) to l(!
). The set of all irreducible words over \Sigma is written \Sigma   # S . It
is well known that this set is rational whenever l(S) is so, since \Sigma   #
. A
normal form of a word u w.r.t. S is an irreducible word v 2 \Sigma   # S such that u
v. 1 We say
that an sts S is confluent when for all words u; v; v 0 2 \Sigma   such that u
v and u
v 0 there
exists a word w 2 \Sigma   such that v
w and v 0
w. If in addition S is terminating, i.e. there
is no infinite chain
is said to be convergent. It is well known that the
convergence of an sts implies the existence and uniqueness of a normal form of each word.
Throughout this paper we only use convergent semi-Thue systems and the unique normal
form of a word u is written u# S . In notation !
usually omit the subscript S when
there is no ambiguity about the sts we refer to. Notice that in our notations "#" has a lower
precedence than the concatenation, thus uv# stands for the normal form of uv.
Notations for rewriting of rational expressions are similar to those for individual words.
For sake of simplicity, we identify every rational expression with the language it denotes. We
may write etc. for any rational expressions X, Y that, in
this context, stand for associated languages. Consequently, we speak of the normal form of a
rational expression X and we write X# in the reference to the set fu# j u 2 Xg or possibly
to some rational expression denoting this set.
It may be useful to restrict applications of some rules of an sts so that they can only
rewrite prefixes of words. For this aim we may assume that each alphabet \Sigma may be extended
by an additional symbol
the words to rewrite belong to $ \Sigma \Sigma   and S is a subset
of ($ \Sigma \Sigma   \Theta $ \Sigma \Sigma   ) [ (\Sigma   \Theta \Sigma   ). Note that if all rules are in $ \Sigma \Sigma   \Theta $ \Sigma \Sigma   then we are in
the particular case of regular canonical systems [5] (see also [8,15]). The latter are known as
generating rational languages.
Convergent Thue Specifications, Their Languages and Models
A convergent Thue specification cts is a triple h\Sigma is a state alphabet, \Gamma is
an event alphabet, R is a rational subset of $ \Sigma \Sigma   (of \Sigma   if S " ($ \Sigma \Sigma   \Theta $ \Sigma \Sigma   is a
finite convergent sts over \Sigma [ \Gamma and each word of R is irreducible, i.e. R 2 Rat($ \Sigma \Sigma   # S ). The
distinction between state alphabet and event alphabet has no importance from a theoretical
point of view but is useful in practical situations. When simply write h\Sigma ; R; Si.
Recall that the convergence is not decidable in general. On the contrary, for a rational
language R, it is decidable whether R '
The aim of Thue specifications is to provide means for specifying and verifying processes.
This article does not discuss that approach as a specification technique but focuses merely on
We use a restricted version of the notion of normal form that is common in term-rewriting. In the general
version a normal form of a word u w.r.t. S is an irreducible word v 2 \Sigma   #S such that u
v.
a basic problem related to formal verification. In this field, semi-Thue systems are needed.
Moreover since we are intersted in deterministic processes, we only consider confluent semi-
Thue systems.
The semantics of Thue specifications is given in terms of (a variant of) labeled transition
systems. Formally, a labeled transition system (lts) A is a tuple hQA
is a set of states, \Gamma is an alphabet, ' A 2 QA is an initial state and ffi A ' QA \Theta \Gamma \Theta QA a
transition relation. When (q; a; q 0 we say that q (resp. q 0 ) is the origin (resp. target)
of a transition labeled by a. A transition system is deterministic if for all q; q
each a implies that q
Each state q 2 QA recognizes some set of words of that is defined
as the smallest set satisfying the following conditions:
if
The language of A written L is the set of all words recognized by the states of A ,
namely
q2QA
Definition 2.1. An lts is an initial model of cts
and the following holds for all u; v 2 R and each a
if and only if ua#
The language L (cts) of a cts is the language of its initial model: L
cag
c
c
c
c
c
\Deltaff
A
A
A AU
a
c
c
c
c
c
c
c
c
\Deltaff
A
A
A AU
a
c
c
\Gamma\Psi
@
@
@ @R
a b
c
\Gamma\Psi
@
@
@ @R
a b
c c
c
c
c
c
c
\Deltaff
A
A
A AU
\Deltaff
A
A
A AU
ae
ae
ae
ae
ae
ae
ae
ae=
Z
Z Z
Z Z
Z Z Z~
c
a
a
c
c
a b
Fig. 2.1. A convergent Thue specification and its initial model
We emphasize that according to the above definition, the states QA of an initial model are
identified with the words of R. It may be observed that the confluence of S is sufficient for an
initial model to be deterministic. Consequently, convergent Thue specifications only model
deterministic processes. Henceforth, for an initial model A of a cts, ffi A is considered as a
function and we write ffi A (u; a) = v instead of (u; a; v) 2 ffi A . Another important observation
is that the language of a cts is always closed under nonempty prefixes because the language
of a transition system is so.
We speak of an initial model because one may define a satisfaction relation
labeled transition systems and Thue specifications. One may then consider the initial object
in the category of the models of a cts. This initial object may be alternatively characterized
as the initial model in the sense of the above definition. Obviously, the initial model is unique
up to isomorphism and always exists. An example of a convergent Thue specification together
with its initial model is provided in Fig. 2.1. In this example, the identification of the set of
states with R 1 is left as an exercise to the reader.
For sake of simplicity, from now on and up to Sect. 7, we neglect the distinction between
state alphabet and event alphabet. Both alphabets are assumed equal and a cts is written
3 Domains of Word-functions and the Hennessy-Milner Logic
In the previous section we explained the relationship between convergent Thue specifications
and deterministic labeled transition systems. To any convergent Thue specification h\Sigma ; R; Si,
one may associate its initial model, say A . Concerning A , a very basic problem consists
in characterizing all transitions with some given label a 2 \Sigma . More precisely, one may wish
to characterize all states that are origins of the transitions labeled by a. For this aim, it is
convenient to view a as a function of states 2 into states by writing a: R!R. The problem
consists therefore in characterizing the domain of this function. Instead of taking all the states
into account, one may consider a restriction of the above function written a: X!U , for some
subsets X and U of R. In the sequel, we restrict our attention to the case where both X and
U are rational subsets of R.
The main problem of this paper may be stated as follows.
Problem. Given a convergent Thue specification cts = h\Sigma ; R; Si and a function a: X!U
relative to cts and such that both X and U are rational subsets of R (X; U 2 Rat(R)), find
Dom(a: X!U), viz the domain of the function, whenever it is rational.
To better understand this problem, one has to reason about the initial model of the cts, say
A . According to Definition 2.1, given a state w 2 X we have
Hence, w 2 Dom(a: X!U) when wa# 2 U . Thus, Dom(a: X!U) is the largest subset X 0 of
X such that X 0 a# ' U .
In order to solve this problem, it is useful to consider a bit more general question that
appears as a technical trick without specific semantics related to transition systems. With
this aim in view, given u 2 \Sigma   and rational subsets X;U of R, the word-function u: X!U
is defined as follows: u(w) = wu# S , for every w 2 X such that wu# S 2 U . Thus
Remember that R is the set of states of A .
It is important to note that, without additional assumptions, a word-function needs not
coincide with the corresponding composition of functions associated to labels. When
unless 1g. Since the set
of the states of a cts may be strictly included in \Sigma # S , the assumption about \Sigma # S being the
source or a the target of a function is not compatible with the semantics in terms of transition
systems. For this reason, the word-function are considered here as a technical tool without a
special meaning.
To close this section we point out that the problem we are interested in is related to the
model checking, at least in the context of the Hennessy-Milner logic.
Checking Properties Expressed in the Hennessy-Milner Logic
The formulae of the Hennessy-Milner logic [9] are built up from the constants 1 and 0,
using the classical connectives (:; ; "; etc.) and a unary operator hai for each letter a of the
alphabet \Sigma .
Given a labeled transition system A , the meaning of a formula ', viz the set of the states
of A that satisfy ', written ['] A , is inductively defined as follows:
where the map [hai] A :  (QA defined by
When a transition system A is an initial model of cts Si, we can express
the meaning of a formula in terms of the domains of the word-functions. For this aim, the
equalities (3.1) remain valid (we have precisely [:']
becomes [hai] A
It is obvious from the above that the procedure developed in the sequel may be used
for checking the properties, expressed in the Hennessy-Milner logic, of systems defined by
convergent Thue specifications. This is relevant only for those cts's for which the procedure
succeeds in computing Dom(a: R!X) for all a 2 \Sigma and all X 2 Rat(R) (see Subsection 6.2).
Since in the case of success, Dom(a: R!X) is rational, the boolean operations stipulated in
may readily be performed.
4 Introducing the procedure
A method for solving the problem stated in the latter section is now developed. An instance of
the problem consists of a cts h\Sigma ; R; Si and a word-function u: X!U relative to it, such that
both X and U are rational subset of R. More precisely, X, U and R are rational expressions
that, for sake of simplicity, are identified with corresponding languages. In addition, u is
required to be irreducible. This is not restrictive since u: X!U and u#: X!U are equal due
to the convergence of S. Hence, if u is reducible, u has to be normalized before applying the
method.
The solution of an instance of the problem is the subset X 0 of X such that X
however that the method developed in the sequel can find X 0 only
rational. The method consists of a procedure that, provided it terminates, computes
a system of equations, the least solution of which is also the solution of the instance of the
problem. Basic ideas underlying the procedure are developed in subsequent paragraphs.
The task of finding Dom(u: X!U) becomes easier if X is partitioned into two parts Y and
Z such that Y u is irreducible and each word of Zu is reducible. Further, Z will be partitioned
into smaller parts, say Z . Indeed, such a "divide and conquer" strategy is based
on the following obvious equality
In order to characterize Z, assume that a rule g ! d of S is applicable to a word vu of Zu.
Since both v and u are irreducible, g overlaps v and u, i.e.
are such that x 6= " and w 6= ". This remark leads to the following
definition.
Definition 4.1. A word x 2 \Sigma   is a left-overlap completion of u 2 \Sigma   with respect to a
semi-Thue system S if there exist w; w 0 2 \Sigma   such that xw 2 l(S), ww
left-overlap completion x of u is minimal if no left-overlap completion of u is a proper suffix
of x.
In view of the above definition, each word of Z has a suffix that belongs to the set, say L, of
all left-overlap completions of u. The set Y , being the complement of Z in X, is characterized
by X i L. In fact, one may characterize Y as X i L min where L min stands for the set of all
minimal left-overlap completions of u.
In order to partition Z into smaller parts, observe that, given a left-overlap completion x
of u, the expression (X=x)xu denotes all the words of Xu that may be reduced by any rule
d such that w is a prefix of u. Consequently, one may wish to partition Z according to L
as
x2L (X=x)x. However, this is not a partition because (X=x 1 )x 1 ' (X=x 2 )x 2 whenever
x 2 is a suffix of x 1 . In fact, it is L min that provides a partition of Z, namely
(X=x)x.
In sum, the following partition of X is used as basis for the divide and conquer strategy:
Now, according to (4.1), the domain corresponding to each part has to be found. With respect
to the first member of the above partition, it is not too difficult to see that
Indeed,
since both U and (XiL min )u are irreducible.
With respect to the other members of the partition described in (4.2), Dom(u: (X=x)x!U)
has to be found for each x 2 L min . Observe first that
Consider, now, various ways of computing (X=x)xu#. Obviously, one may compute xu# first
and subsequently compute the normal form of (X=x)(xu#). Thus
The maximal suffix of xu# that is not rewritten during any computation of the normal form
of (X=x)(xu#) now has to be isolated. The concept introduced in the following definition is
useful for this purpose.
Definition 4.2. A word v of \Sigma   # is a right irreducible divisor with respect to an sts S when
f"g. The set of all right irreducible divisors w.r.t. S is written rid S .
For any u 2 \Sigma   such that rid S we say that w is a right irreducible divisor of
w.r.t. S. The set of all right irreducible divisors of u is written rid S (u). A right irreducible
divisor of u is maximal if it is not a proper suffix of a right irreducible divisor of u.
It is easy to see that rid . Consequently, since S is finite and
\Sigma   # is rational, rid S is rational too. It is also obvious that any right-irreducible divisor of
xu# is not rewritten during any computation of (X=x)(xu#:
Proposition. Any u 2 rid S and w 2 \Sigma   satisfy
Let us go back to the problem of finding Dom(xu#: X=x!U) assuming that
z is the maximal right irreducible divisor of xu#. Suppose also that
for some V ' \Sigma   . Then V in view of the above proposition, and V y#z ' U .
Therefore V y# ' U=z. Consequently In sum, taking (4.4) and (4.5)
into account, we have
The next definition is not indispensable since it just combines Definitions 4.1 and 4.2.
Nevertheless, it will allow a more concise presentation of the procedure.
Definition 4.3. A left-overlap triple of a word u w.r.t. S is a triple of words hx;
that x is a minimal left-overlap completion of u, z is the maximal right
irreducible divisor of xu#. The set of all left-overlap triples of u is written lot S (u), or simply
lot (u) if S is determined by context. A triple  2 lot (u) is written hx  ; y  ; z  i.
The procedure is given in the form of three deduction rules (see Table 4.1) Generate,
and Eliminate, the first of which corresponds, roughly speaking, to the transformations
discussed up to now in this section. Using (4.1), (4.2), (4.6) and Definition 4.3, those
transformations may be summarized in the next lemma.
Henceforth we speak of an irreducible expression to mean that the expression denotes a
language, each word of which is irreducible.
Lemma 4.4. Let X be an irreducible rational expression and u an irreducible word. Then
U=z 6=?
The proof of the lemma follows from the above discussion together with the following remarks.
When X=x ?. For this reason, such
cases are excluded from (4.7). Also the first member of the above sum is written in a way
that slightly differs from the righthand side of (4.3), since Xi
and
x  is the set of all minimal left-overlap completions of u (formerly L min ).

Table

4.1. Deduction rules
U=z 6=?
U=z 6=?
Xx
is a set of fresh variables.
We shall now describe the procedure by explaining its principles and related notations.
As mentioned at the beginning of this section, in case of success the result of the procedure
consists of a system of equations. Consequently, we still need some variables. In a derivation
of such a system, an expression of the form X 7! u: X!U with a variable X represents a
goal. This means that Dom(u: X!U) should be the least solution w.r.t. X of the resulting
system of equations. Each rule of a procedure is applied downwards with reference to some
goal. The goal is then said to have been treated ; otherwise it is called fresh. We denote by F
(resp. T) the set of fresh (resp. treated) goals. Thus, the procedure manipulates sequents of
the form T; F ' E where E is a system of equations.
Let us now explain the r"ole of each rule of the procedure. First note that any rule is
applied with reference to some fresh goal. Given a fresh goal X 7! u: X!U the rule Generate
introduces a new equation based on (4.7)
U=z 6=?
and for each  2 lot(u) such that X=x  6= ? and U=z  6= ?, it introduces a fresh goal
Each X  is some new variable. The goal X 7! u: X!U is then no
longer fresh and is transferred to T. Notice that if, in the new equation, we replace X by
Dom(u:X!U) and each X  by Dom(y  : X=x  !U=z  ) we thereby obtain (4.7). The fresh
introduced in this step correspond to the principle that the
procedure should be applied recurrently in order to compute Dom(y  : X=x  !U=z  ).
The following idea underlies the rule Identify. If there is a treated goal X 7! u: X!U (the
one for which an equation has been generated) and a fresh goal X 0 7!
then we should not generate an equation from X 0 7!
Instead, we identify the two variables X and X 0 . This is realized by renaming X 0 as X in the
current system of equations. The goal X 0 7! simply removed from F.
The rule Eliminate deals with goals X 7! u: X!U such that Xu is irreducible. A fresh
goal satisfying this condition is moved to T and the equation is added to the
systems of equations.
The applicability of the above rules is restricted by certain conditions (written beside each
rule). We insist on the fact that within such applicability conditions Xu be understood as a
language and r(T) as a set of word-functions (the range of the assignment T). The notation
F q fX 7! u: X!Ug is used for a partition of some F 0 such that X!Ug.
Derivations and related concepts are defined as follows.
A derivation is a (possibly finite) sequence of sequents s 0
for each there exists an instance of a rule, the upper and lower sequent of
which are equal resp. to s i and s i+1 , and s i satisfies the applicability conditions of the rule.
A derivation is called maximal when it is not a proper prefix of another derivation. We say
that a sequent is pure when it is of the form ?; fX 0 7! stands
for an irreducible rational expression and u 0 an irreducible word such that rid f"g. We
say that a derivation is pure when it starts with a pure sequent.
In order to compute Dom(u: X!U) the procedure starts with the pure sequent
f"g. This is not restrictive since, if
with z the maximal right irreducible divisor of u such that z 6= ", then
X!U=z). The procedure may therefore start with the pure sequent
?; fX 7! y: X!U=zig ' ?. Next, the rules are applied as long as possible in order to
produce a maximal derivation. The procedure stops if no rule may be applied. This happens
only if there are no more fresh goals. It then remains to compute the solution of the resulting
system of equations w.r.t. X . Let us illustrate this by applying the procedure to an example.
Example 4.5. Let cts 1 be the convergent Thue specification of Fig. 2.1. We want to compute
We check that both $(a are irreducible, and rid(c) =
f"g. Taking into account that lot (c) = fha; "; bi; hb; c; aig, we have the following derivation.
Generate
ae
oe
Eliminate
ae
oe
ae
oe
ae
oe
ae
oe
Finally, the least solution of the resulting system w.r.t. X 0 yields
as expected, according to the minimal model of cts 1 depicted on Fig. 2.1.
5 Correctness of the procedure
Usually, a sequent-like calculus is correct, when it transforms valid sequents into valid ones.
We shall use the following notation in order to explain what we mean by "valid sequent".
Notation 5.1. For any set G of goals, we denote by oe G the following substitution:
The following definition is used as basis for the correctness.
Definition 5.2. A sequent T; F ' E is valid, when Dom(v: Y !V ) is the least solution of
goal Y 7! v: Y !V 2 T.
We need to establish the following theorem.
Theorem 5.3. Any sequent of a pure derivation is valid.
Proof. Let be a derivation satisfying the assumptions of the theorem and let us
prove the statement for any sequent s k by induction on k 2 N.
Basis: The statement holds trivially for any pure sequent ?; fX 0 7!
Induction step. We have to distinguish 3 cases depending on the rule that yields s k from s k\Gamma1 .
By induction hypothesis s k\Gamma1 is valid and the validity of s k is obtained using the correctness
of each rule, established in Appendix B. 2
The main result on the correctness is given as corollary of Theorem 5.3.
Corollary (Correctness). Let D be a maximal finite derivation starting with a pure sequent
be the last sequent of D. Then Dom(u: X!U) is
the least solution of
Proof. It is obvious that on the first sequent either Generate or Eliminate may by applied.
Consequently, X 7! u: X!U 2 T. On the other hand, F is empty, since no rule can be
applied on the last sequent of D. Hence oe F is empty and by Theorem 5.3 we conclude that
Dom(u:X!U) is the least solution of
6 Incompleteness and termination
Since the procedure computes only linear systems of equations, the rationality of the domain
of a word-function is obviously a necessary condition for the termination. To see that this
condition is not sufficient, consider the following specification: cts
apply the procedure to the
goal . The procedure generates the following infinite sequence of goals:
This example points out that the procedure is not complete. In fact, as established in the
next subsection, a complete procedure for this problem cannot exist. (By the completeness of
the procedure we mean that it terminates on each instance of the problem that has a rational
solution.) In Subsection 6.2, we therefore investigate a sufficient condition for the termination
of our procedure.
6.1 Incompleteness of the problem
The question as to whether a complete procedure exists for this problem is equivalent to the
recursive enumerability of the following set of tuples:
More precisely, we consider an even simpler version of the problem where the cts's are of
the form h\Sigma ; \Sigma   #; Si and the word functions are of the form a: X!U . We establish that the
following set of pairs is not recursively enumerable:
is a convergent sts over \Sigma , a 2 \Sigma ;
To this end we reduce the complement of the halting problem for Turing machines. More
precisely, given a deterministic Turing machine T and an input word w, we construct a
convergent sts and a word-function the domain of which is rational if and only if T does
not halt on w.
be a deterministic single-tape Turing machine, where
is the tape alphabet, denotes the blank symbol, Q is the set of states,
is the transition function and q 0 is the initial (resp.final) state. Observe that without
loss of generality it is implicitly assumed here that T cannot print . Consequently, each tape
cell that has been visited by the tape head contains a letter of \Pi and the language accepted
by T is


stands for the reflexive-transitive closure of the single-step computation relation ' T
Without loss of generality we assume in addition that
is the set of "overlined"
versions of letters of \Pi and 0; 0; are additional symbols. Let
be an input word.
Given the pair hT ; wi we construct the pair hS T ; %:Xw!U# i where
and the sts ST over \Sigma is the union of several groups of rules below. When two rules differ
only by 0 or 1, we abbreviate them by meta-variables  ;  0 that rank over f0; 1g. The use of
"overlined" ("underlined") symbols is not relevant for the understanding of the construction
but aims at avoiding overlaps between lefthand sides of ST . At first reading the reader may
assume that the "underlined" and "overlined" versions of any symbol and the symbol itself
are identical.
ffl Initialization rules
ffl Rules that simulate the behaviour of T
ffl Rules that apply immediately after each simulation step that does not result in a configuration
where the tape head reads
ffl Rules that apply before each simulation step (after (ii) or (vii))
ffl Terminal rules
Before justifying this construction, we state several lemmas. The first one is obvious.
Lemma 6.1. Both Xw and U# are irreducible w.r.t. ST . 2
Lemma 6.2. ST is confluent.
Proof. To establish the confluence, it is enough to check that the lefthand sides of ST do not
Lemma 6.3. ST is terminating.
Proof. Consider the following precedence  on \Sigma : 0  1  a  # for all a 2 \Pi. Let  1 be
the following (rewrite) ordering on (\Sigma r f%g)   :
where  lex is the lexicographic extension of  and e
x (resp. e y) stands for the reversal of x
(resp. y). Using  1 we define a (reduction) ordering  2 on (\Sigma r f%g)   :
It is easy to check that, except for (i), each rule of l ! r 2 ST satisfies l  2 r. Let then  3
be a (reduction) ordering on \Sigma   defined, for all x; y 2 \Sigma , as follows: x  3 y if
stands for the number of occurrences of % in x
- or
where  lex
stands for the lexicographic extension of  2 .
Now, for Rule (i) we have %  3 % because (0; ")  lex
1). For each
other rule l ! r 2 ST we have also l  3 r because  2 and  3 coincide on (\Sigma r f%g)   . 2
Justification of the construction Given a word q 0 wx 2 Xw , where
some a below the
rewrite steps of the word q 0 wx%. (The sequences of rules used in these steps are denoted by
rational expressions.)
Starting from q 0 wx% we get
and by
we end up with u n q n v n #, provided that
Thus if T does not halt on w, Dom(%:Xw!U#
Assume then that T halts after k steps in a configuration u k q f v k and let v
for some b the length 2n of x may be arbitrarily big, without loss of
generality we assume that n ? k l. Starting with q 0 wx% analogous rewrite steps lead to
We then get
(viii)   (ix)(vii)
Now, using the rules (x) and (xi) we end up with u k q f # if and only if the word
belongs to the Dyck language D   . Consequently Dom(%:Xw!U#
which is not a rational language.
We have therefore established the following lemma.
Lemma 6.4. Dom(%:Xw!U# ) is rational if and only if T does not halt on w. 2
Putting together Lemmas 6.1, 6.2, 6.3 and 6.4 and taking into account the fact that the
complement of the halting problem for Turing machines is not recursively enumerable, we
conclude that the following holds.
Theorem 6.5. DomRat is not recursively enumerable. 2
In view of this theorem a complete procedure for the problem of computing rational domains
of (even single-letter) word-functions cannot exist. Otherwise, there would exist a Turing
machine that "semi-decides" the complement of the halting problem.
6.2 Termination
In this subsection we state a sufficient condition for the termination of the procedure. The
following definition provides a tool for studying the termination.
Definition 6.6. The generation set for a goal X 7! Dom(u:X!U) w.r.t. an sts S, written
is the smallest subset of \Sigma   \Theta  (\Sigma   )\Theta  (\Sigma   ) that contains hu; X;Ui and such that
whenever hv; Y; W for each  2 lot (v).
In the sequel, we shall consider the first, the second and the third projections of a generation
set G S (u; X;U
We now state two lemmas that lead to the final result of this section. The first one is
obvious.
Lemma 6.7. A maximal derivation starting with a pure sequent ?; fX 7! Dom(u: X!U)g '
? is finite if and only if its generation set is finite. 2
Lemma 6.8. The second (resp. third) projection of a generation set G S (u; X;U) is finite if
Proof. Note first that for a given rational set Z the cardinality of the set
is not greater than 2 k , where k is the number of states of a minimal automaton accepting Z.
In order to prove the statement, it is therefore enough to show that  2 (G S (u; X;U)) ' QX
According to Definition 6.6,
there exist hy
and
lot (y n ). Thus
Hence
The following theorem states a simple sufficient condition that guarantees that the procedure
will terminate.
Theorem 6.9. Starting with a pure sequent ?; fX 7! Dom(u: X!U)g ' ?, the procedure
terminates if
1. S is finite,
2. for each minimal left-overlap completion x of u, the word xu belongs to l(S) and
3. for each rule r 2 S, any  2 lot (r(r)) and any minimal left-overlap completion x 0 of y  ,
the word x 0 y  belongs to l(S).
Proof. According to Lemmas 6.7 and 6.8, the termination of the procedure is guaranteed
if  1 (G S (u; X;U)) is finite. An easy induction allows us to establish that for any y in
there exists a rule r 2 S such that xy and x is a minimal left-overlap
completion of y. Hence  1 (G S (u; X;U)) is included in a finite set, namely suff (l(S)). 2
Note that, when used for computing the domain of a word-function that is a single letter
(as e.g. in the case of the Hennessy-Milner logic), the procedure terminates provided that
both the first and the third requirements of Theorem 6.9 hold. We may use this observation
for more general word functions. In order to compute Dom(u: X!U) w.r.t. h\Sigma ; R; Si such
that when the second requirement of Theorem 6.9 is not satisfied
whereas the first and the third ones are, we may proceed as follows.
1. compute the ranges of the word functions:
(For the computation of ranges we may use the procedure of [11]. This procedure always
terminates for a single-letter word-function under conditions 1 and 3 of Theorem 6.9.)
2. Set D apply the procedure for computing the domains
of the word functions:
Now
It is important to point out three classes of semi-Thue systems that may successfully
be used for letterwise computation of domains of word-functions, namely left-basic sts's,
monadic sts's and special sts's.
Corollary 6.10. Starting with a pure sequent ?; fX 7! Dom(a: X!U)g ' ?, where a 2 \Sigma ,
the procedure terminates if S is finite and is special, monadic or left-basic.
Proof. When S is monadic, for any r 2 S, the set lot (r(r)) may contain only elements of the
form hx; a; "i or hx; "; ai such that xr(r) ! a is a rule of S. When S is left-basic or special,
obviously for each rule r of S. Hence the sts's that are special, monadic or
left-basic satisfy the third requirement of Theorem 6.9. 2
In view of the corollary, we may assert that the requirements of Theorem 6.9 provide a
reasonably weak sufficient condition for termination. These requirements capture the well
known classes of sts's, the models of which are related to the transition graphs of pushdown
machines [7,12]. For the latter, the rationality of the domains of word-functions follows from
the well known fact that the pushdown store languages are rational. In addition, the scope
of Theorem 6.9 is not restricted to special, monadic or left-basic sts's. Indeed, S 1 (see Fig.
2.1) is neither special, monadic nor left-basic whereas it satisfies the requirements 1 and 3 of
the theorem.
Last but not least, the example of non termination that opened this section has one
interesting property, namely that cts 0
equivalent to cts 2 , in the sense that cts 2 and cts 0
2 have the same initial model. But this
time the procedure terminates for cts 0
2 on any single-letter word-function.
7 Final Example
We consider a simple portion of a railway network. A single track connects two stations: left
(L) and right (R), via a central one (C), as on the following picture.
L C R
All trains run from L to R or vice-versa with a stop at C, never being allowed to go in reverse.
The central station has two platforms allowing train crossing. Each of these platforms may
be occupied by at most one train.
To model this situation we may consider the following state alphabet \Sigma
a train has left L but has not yet arrived at C
a train has left R but has not yet arrived at C
\Gamma! D C
a train has left C for R but has not yet arrived at R
a train has left C for L but has not yet arrived at L
\Gamma! A C
a train coming from L is waiting on a platform of C
a train coming from R is waiting on a platform of C
The underlined versions of \Gamma! D C
have no special meaning for the modeling but aim
at making easier the definition of transitions by a semi-Thue system. For this reason, we
distinguish the set \Sigma 0 of non-underlined letters of \Sigma : \Sigma
g. We also
consider the following event alphabet \Gamma .
d L
departure of a train from L
departure of a train from R
\Gamma! d C
departure of a train from C for R
departure of a train from C for L
\Gamma! a C
arrival of a train from L at C
a C
arrival of a train from R at C
a L
arrival of a train at L
a R
arrival of a train at R
In our modeling a train "appears" when it leaves one of the stations L or R and "disap-
pears" when it arrives at the opposite terminal station. Since the trains do not go in reverse,
there is a deadlock, when two trains run towards one another on the same portion of the track
(between L and C or between C and R).
In order to define the set R of states, we need the following expressions, each of which
describes, in fact, a subset of R satisfying some characteristic property (stated between paren-
(D L
trains run from L to R),
trains run from R to L),
(D L
trains run towards C),
trains run from C to L or R).
Using the above expressions, the states of the system may be defined as follows:
A word of R reflects the events in the reverse chronological order (a state alphabet letter
corresponding to the most recent event is written immediately after $). For instance
means that there is one train, say t running from R to C, a second one, say t running from
L to C and a third one, say t 3 , on a platform of C coming from R. The events corresponding
to this configuration occurred in the following has left R before t 2 left L and t 2 has
left L before t 3 arrived at C.
The transitions are defined by the following sts S over f$g [
xd L
\Gamma! d L
x for x 2 \Sigma 0 xd R
\Gamma! d R
x for x 2 \Sigma 0
$d L
\Gamma! $D L
\Gamma! $D R
x \Gamma! a C
\Gamma! \Gamma! a C
x /\Gamma a C
\Gamma! /\Gamma a C
x for x 2 \Sigma 0 r f \Gamma! D C
\Gamma! a C
\Gamma! \Gamma! A C
a C
\Gamma!
x \Gamma! A C
\Gamma! \Gamma! A C
\Gamma!
x for x 2 \Sigma 0
\Gamma!
\Gamma!
x \Gamma! d C
\Gamma! \Gamma! d C
x for x 2 \Sigma 0 r f \Gamma! A C
x /\Gamma d C
\Gamma!
\Gamma! A C
\Gamma! d C
\Gamma! \Gamma! D C
\Gamma!
x \Gamma! D C
\Gamma! \Gamma! D C
\Gamma!
x for x 2 \Sigma 0
\Gamma!
\Gamma!
\Gamma! a R
x for x 2 \Sigma 0 r f \Gamma! D C
xa L
\Gamma! a L
\Gamma! D C
a R
a L
When a meta-variable x is replaced by all possible values, we get a system of 62 rules with
non-overlapping lefthand sides. This system is therefore finite and confluent. The termination
of S may readily be established using standard reduction orderings, thus concluding that S
is convergent.
As an example of questions concerning this system, we may ask about the set of states in
which a departure of a train may occur at one of the terminal stations, for instance at R. The
set of such states, say P
, is precisely given by P d R
computing P d R
it is useful to ask about the termination of the procedure in this case. Since the first condition
of Theorem 6.9 is obviously satisfied by S, we check whether the second one is satified by d R
Indeed, for each letter a and any left-overlap completion x of a, we have xa 2 l(S). Hence, it
remains to verify the third condition of Theorem 6.9. To this end, we compute the set T of
left-overlap triples of r(S):
For the rules with a meta-variable, we obtain, for all x 2 \Sigma 0
lot(d L
xig
lot (d R
xig
lot ( \Gamma! a C
lot ( /\Gamma a C
lot( \Gamma! A C
xig
lot(
xig
lot ( \Gamma! d C
lot ( /\Gamma d C
lot ( \Gamma! D C
xig
lot ( /\Gamma D C
xig
lot(a R
lot (a L
For the rules with $, we have
lot($D L
\Gamma! A C
and for other rules
lot(
\Gamma! A C
ig
lot(
ig
lot ( \Gamma! D C
ig
lot ( /\Gamma D C
ig
We observe that  2 (T ) f"g. Thus, for each u 2  2 (T ) and each left-overlap
completion x of u we have xu 2 l(S), meaning that the third condition of Theorem 6.9 is
satisfied. We may therefore conclude that the procedure terminates here for any single-letter
word-function.
Starting with a pure sequent ?; fX 7! Dom(d R
the procedure terminates
and yields a system of equations, the least solution of which is, as expected,
ing
Thus, the departures of trains from R are possible only when there are no trains running from
C to R.
Concluding remarks
Semi-Thue systems and transition systems have been related here by sketching a formal
specification technique named as Thue specifications. A particular emphasis has been placed
on the simplest case of the problem of formal verification. A pragmatic point of view has been
necessary in approaching the latter problem, since this has been shown not to be recursively
enumerable, and has led to an incomplete procedure. This problem is perhaps the most
elementary problem that one has to deal with in order to be able to approach the model
checking of Thue specifications, at least in the special case of the Hennessy-Milner logic.
However, since the expressive power of the latter is not very rich, our work needs be extended
so as to handle more powerful logics. With this aim in view, our attention is currently focussed
on the monadic second-order logic [13].
One of the most important problems concerns the specification of systems that consist of
interacting processes. This problem may be handled via the concept of synchronized product
[2]. Within that approach, each component of the system is specified separately and interactions
between components are defined as synchronization constraints. For instance, the
railway example may be specified in an even more elegant way as four interacting processes:
the two portions of the track and the two platforms of the central station. When a system
is specified componentwise by several Thue specifications provided with a synchronization
constraint, these specifications may be combined into a single one, (on wich the procedure
may be applied for checking the properties of the system). Based on the ideas of [14], an
algorithm that performs the latter task, has been developed [18].

Acknowledgments

We wish to thank Marie-Catherine Daniel-Vatonne and '
Etienne Payet
for careful reading of a preliminary version of this paper, and Adrian Bondy for correcting
the English text. We are grateful to Damian Niwi'nski for numerous suggestions that helped
improving the presentation of this paper. Special thanks are due to Serge Burckel whose
comments have influenced Subsection 6.1 and to an anonymous referee that has suggested
the current proof of Lemma 6.3 which is more elegant than our original proof.



--R

Finite Transition Systems.
Comportements de processus.

Theorem proving in hierarchical clausal specifications.
Regular canonical systems.

A string-rewriting characterization of context-free graphs
On the regular structure of prefix rewriting.
Algebraic laws for nondeterminism and concurrency.
Introduction to Automata Theory
A procedure for computing normal forms of certain rational sets.

The graphs of finite monadic semi-Thue systems have a decidable monadic second-order theory
Thue specifications and their monadic second-order properties

A method for enumerating cosets of a group presented by a canonical system.
Finite automata.
Mathematical Logic.
An automata-theoretic approach to automatic program verification
Automated reasoning: Introduction and Applications.
first occur all self-Identify steps
and other Identify steps occur after.
--TR
automated deduction;infinite-state systems;formal verification;string-rewriting