9512.net

甜梦文库

甜梦文库

当前位置：首页 >> >> # Linearly bounded infinite graphs

Acta Informatica manuscript No. (will be inserted by the editor)

Arnaud Carayol · Antoine Meyer

Linearly Bounded In?nite Graphs

arXiv:0705.3487v1 [cs.LO] 24 May 2007

Received: date / Revised: date

Abstract Linearly bounded Turing machines have been mainly studied as acceptors for context-sensitive languages. We de?ne a natural class of in?nite automata representing their observable computational behavior, called linearly bounded graphs. These automata naturally accept the same languages as the linearly bounded machines de?ning them. We present some of their structural properties as well as alternative characterizations in terms of rewriting systems and context-sensitive transductions. Finally, we compare these graphs to rational graphs, which are another class of automata accepting the context-sensitive languages, and prove that in the bounded-degree case, rational graphs are a strict sub-class of linearly bounded graphs.

1 Introduction One of the cornerstones of formal language theory is the hierarchy of languages introduced by Chomsky in [9]. It rests on the de?nition of four increasingly restricted classes of grammars, which respectively generate the recursively enumerable, context-sensitive, context-free and rational languages. All these classes were extensively studied, and have been given several alternative characterizations using di?erent kinds of formalisms (or acceptors ). For instance, pushdown systems characterize context-free languages, and linearly

A preliminary version of this article appeared in MFCS 2005. Arnaud Carayol Irisa, Campus de Beaulieu, 35042 Rennes Cedex, France Tel.: +33299847278, Fax: +33299847171 E-mail: Arnaud.Carayol@irisa.fr Antoine Meyer Liafa, Universit? e Denis Diderot, Case 7014, 2 place Jussieu, 75251 Paris Cedex 05, France E-mail: Antoine.Meyer@liafa.jussieu.fr

2

Arnaud Carayol, Antoine Meyer

bounded Turing machines (LBMs) characterize context-sensitive languages. More recently, several authors have related these four classes of languages to classes of in?nite graphs (for a survey, see for instance [27]). Given a ?xed initial vertex and a set of ?nal vertices, one can associate a language to a graph by considering the set of all words labeling a path between the initial vertex and one of the ?nal vertices. In [8], a summary of four classes of graphs accepting the four classes of the Chomsky hierarchy is presented. They are the Turing graphs [6], rational graphs [20,21,24], pre?x-recognizable graphs [4,5], and ?nite graphs. Several approaches exist to de?ne classes of in?nite graphs, among which we will cite three. The ?rst one is to consider the ?nite acceptor of a formal language, and to build a graph representing the structure of its computations: vertices represent con?gurations, and each edge re?ects the observable e?ect of an input on the con?guration. One speaks of the transition graph of the acceptor. An interesting consequence is that the language of the graph can be deduced from the language of the acceptor it was built from. A second method proposed in [8] is to consider the Cayley-type graphs of some classes of word rewriting systems. Each vertex is a normal form for a given rewriting system, and an edge between two vertices represents the addition of a letter and re-normalization by the rewriting system. Finally, a third possibility is to directly de?ne the edge relations in a graph using automata or other formalisms. One may speak of derivation, transduction or computation graphs. In this approach, a path no longer represents a run of an acceptor, but rather a composition of binary relations. Both pre?x-recognizable graphs and Turing graphs have alternative definitions along all three approaches. Pre?x-recognizable graphs are de?ned as the graphs of recognizable pre?x relations. In [25], Stirling characterized them as the transition graphs of pushdown systems. It was also proved that they coincide with the Cayley-type graphs of pre?x rewriting systems. As for Turing graphs, Caucal showed that they can be seen indi?erently as the transition and computation graphs of Turing machines [6]. They are also the Cayley-type graphs of unrestricted rewriting systems. Rational graphs, however, are only de?ned as transduction graphs (using rational transducers) and as the Cayley-type graphs of left-overlapping rewriting systems, and lack a characterization as transition graphs. In this paper, we are interested in de?ning a suitable notion of transition graphs of linearly bounded Turing machines, and to determine some of their structural properties as well as to compare them with rational graphs. As in [6] for Turing machines, we ?rst de?ne a labeled version of LBMs, called LLBMs. Their transition rules are labeled either by a symbol from the input alphabet or by a special symbol denoting an internal, unobservable transition. Following an idea from [25], we consider that in every con?guration of a LLBM, either internal actions or inputs are allowed, but not both at a time. This way, we can distinguish between internal and external con?gurations. The transition graph of a LLBM is the graph whose vertices are external con?gurations, and whose edges represent an input followed by any ?nite number of silent transitions. This de?nition is purely structural and associates a unique graph to any given LLBM. For convenience, we call

Linearly Bounded In?nite Graphs

3

such graphs linearly bounded graphs. A similar work was proposed in [16,23], where the class of con?guration graphs of LBMs up to weak bisimulation is studied. However, it provides no formal de?nition associating LBMs to a class of real-time graphs (without edges labeled by silent transitions) representing their observable computations. To further illustrate the suitability of our notion, we provide two alternative de?nitions of linearly bounded graphs. First, we prove that they are isomorphic to the Cayley-type graphs of length-decreasing rewriting systems. The second alternative de?nition directly represents the edge relations of a linearly bounded graph as a certain kind of context-sensitive transductions. This allows us to straightforwardly deduce structural properties of linearly bounded graphs, like their closure under synchronized product (which was already known from [16]) and under restriction to a context-sensitive set of vertices. To conclude this study, we show that linearly bounded graphs and rational graphs form incomparable classes, even in the ?nite degree case. However, bounded degree rational graphs are a strict sub-class of linearly bounded graphs. 2 Preliminary De?nitions A labeled, directed and simple graph is a set G ? V × Σ × V where Σ is a ?nite set of labels and V a countable set of vertices. An element (s, a, t) a of G is an edge of source s, target t and label a, and is written s ?→ t or simply s ?→ t if G is understood. The set of all sources and targets of a graph is its support VG . Two graph G, H ? V × Σ × V are isomorphic if a there exists a bijection ρ from VH to VG such that for all x, y ∈ VH , x ?→ y i? ρ(x) ?→ ρ(y ).

G

1 k t1 , . . . , sk ?→ tk with ?i ∈ [2, k ], si = ti?1 A sequence of edges s1 ?→ u is a path. It is written s1 ?→ tk , where u = a1 . . . ak is the corresponding path label. A graph is deterministic if it contains no pair of edges with the same source and label. One can relate a graph to a language by considering its path language, de?ned as the set of all words labeling a path between two given sets of vertices.

a

G

a

H

a

a

De?nition 1 The (path) language of a graph G between two sets of vertices I and F is the set L(G, I, F ) = { w | s ?→ t, s ∈ I, t ∈ F }.

G w

2.1 Linearly bounded Turing machines We recall the de?nitions of context-sensitive languages and linearly bounded Turing machines. A context-sensitive language is a set of words generated by a grammar whose production rules are of the form α → β with |β | ≥ |α|. Such grammars are called context-sensitive or sometimes growing. A

4

Arnaud Carayol, Antoine Meyer

more operational de?nition of context-sensitive languages is as the class of languages accepted by linearly bounded Turing machines (LBMs). De?nition 2 A linearly bounded Turing machine is a tuple M = (Γ, Σ, [, ], Q, q0 , F, δ ), where – – – – – – – Γ is a ?nite set of tape symbols, Σ ? Γ is the input alphabet which does not contain the symbol ε, [ and ] ∈ / Γ are the left and right end-marker, Q is a ?nite set (disjoint from Γ ) of control states, q0 ∈ Q is the unique initial state, F ? Q is a set of ?nal states, δ is a ?nite set of transition rules of one of the forms: pA ?→qB ± p[?→q [+ p] ?→q ]?

with p, q ∈ Q, A, B ∈ Γ and ± ∈ {+, ?}. As usual in the syntax of Turing machines, symbols + and ? in transition rules respectively denote a move of the read head to the right and to the left. The set of con?gurations CM of M is the set of words uqv such that q ∈ Q, v = ε and uv ∈ [Γ ? ]. The transition relation ?→ is a subset of CM × CM de?ned as:

M M

?→ = { (upAv, uBqv ) | pA ?→ qB + ∈ δ } ∪ { (uCpAv, uqCBv ) | pA ?→ qB ? ∈ δ } We will simply write ?→ when M is understood. For any input word w ∈ Σ ? , the unique initial con?guration is [q0 w] and a ?nal con?guration cf is a con?guration containing a terminal control state. A word w is accepted by M if [q0 w] ?→ cf where cf is a ?nal con?guration. Quite naturally, M is deterministic if, from any con?guration, at most one rule can be applied. Formally, for all con?gurations c, c1 and c2 such that c ?→ c1 and c ?→ c2 , then c1 = c2 . Other de?nitions of linearly bounded machines do not use the border symbols to constrain the head inside a portion of the tape whose size equals the size of the input. Instead, they externally require that the tape size used at any point during any computation be at most k times the size of the input, where k is a ?xed constant. It is a well-known fact that k can be considered equal to 1 without loss of generality, and that these de?nitions are equivalent to the one given above. An interesting open problem raised by Kuroda [17] concerns deterministic context-sensitive languages, which are the languages accepted by deterministic LBMs. It is not known whether they coincide with non-deterministic context-sensitive languages, as is the case for recursively enumerable or rational languages. Note that, contrary to unbounded Turing machines, it is su?cient to only consider linearly bounded machines which always terminate, also called terminating machines. This is expressed by the following proposition: Proposition 1 For every linearly bounded Turing machine, there exists a terminating linearly bounded Turing machine recognizing the same language.

Linearly Bounded In?nite Graphs

5

Proof It su?ces to show that, for every linearly bounded machine M whose con?guration graph contains a cycle, there is an equivalent terminating machine M ′ , i.e. a machine which always terminates and accepts the same language as M . The total number of distinct con?gurations of M during a run on a word of size n is bounded by k n , where k is a constant depending on the size of the control state set and work alphabet of M . It is easy to see that a word w accepted by M must be accepted by at least one run of size less than k |w| . Indeed, if the smallest run accepting w was longer than this bound, it would necessarily contain two occurrences of the exact same con?guration, i.e. a cycle. By removing this cycle, one would obtain a shorter accepting run. Let M ′ be the machine which simulates M while incrementing a n-digit counter in base k encoded in the alphabet and stops the run if the counter over?ows. By construction, M ′ accepts the same language as M and is terminating. ? ? Similar arguments are used in [17] to show that the set of words on which a linearly bounded machine has an in?nite run is context-sensitive. Another property of context-sensitive languages is that they are closed under union and complement. Theorem 1 ([14, 26]) The context-sensitive languages over a ?nite alphabet Γ form an e?ective Boolean algebra. The notion of space-bounded Turing machine can be extended to any bound f : N → N such that for all n ≥ 0, f (n) ≥ log(n). The set of all languages accepted by a Turing machine working in space f (n) on an entry of size n is written NSPACE[f (n)]. The following theorem states that the space hierarchy is strict. Theorem 2 ([13, 14]) For all space-constructible f and g in N → N such f (n) = 0, we have NSPACE[f (n)] NSPACE[g (n)]. that limn→+∞ g (n) In particular, the class NSPACE[2n ] of languages recognizable in exponential space strictly contains the class of context-sensitive languages (or NSPACE[n]).

2.2 Rational graphs Consider the product monoid Σ ? × Σ ? , whose elements are pairs of words (u, v ) in Σ ? , and whose composition law is de?ned by (u1 , v1 ) · (u2 , v2 ) = (u1 u2 , v1 v2 ). A ?nite transducer is an automaton over Σ ? × Σ ? with labels in (Σ ∪ {ε}) × (Σ ∪ {ε}). Transducers accept the rational subsets of Σ ? × Σ ? , which are seen as binary relations on words and called rational transductions. We do not distinguish a transducer from the relation it accepts and write (w, w′ ) ∈ T if the pair (w, w′ ) is accepted by T . Graphs whose vertices are words and whose edge relations are de?ned by transducers (one per letter in the label alphabet) are called rational graphs.

6

Arnaud Carayol, Antoine Meyer

De?nition 3 ([20]) A rational graph labeled by Σ with vertices in Γ ? is given by a class of transducers (Ta )a∈Σ over Γ . For all a ∈ Σ , (u, a, v ) ∈ G if and only if (u, v ) ∈ Ta . For w ∈ Σ + and a ∈ Σ , we recursively de?ne Twa = Tw ? Ta , where ? w denotes the standard relational composition, and we write u ?→ v if and only if (u, v ) ∈ Tw . In general, there is no bound on the size di?erence between input and output in a transducer (and hence between the lengths of two adjacent vertices in a rational graph). Interesting sub-classes are obtained by enforcing some form of synchronization. The most well-known was de?ned by Elgot and Mezei [11] (see also [12]) as follows. A transducer over Σ with initial state q0 is (left-)synchronized if for every path q0 ?→ q1 . . . qn?1 ?→ qn , there exists k ∈ [0, n] such that for all i ∈ [1, k ], xi and yi belong to Σ and either xk+1 . . . xn = ε and yk+1 . . . yn ∈ Σ ? or yk+1 . . . yn = ε and xk+1 . . . xn ∈ Σ ? . A rational graph de?ned by synchronized transducers will simply be called a synchronized (rational) graph. Rational graphs form a class of in?nite acceptors for context-sensitive languages. For a discussion on the expressive power of the sub-classes of rational graph seen as language acceptors see [3]. Theorem 3 ([21]) The languages accepted by the rational graphs between a rational set of initial vertices and a rational set of ?nal vertices are the context-sensitive languages. This result can be slightly strengthened in the case of a single initial and ?nal vertex. Corollary 1 For any rational graph G labeled by Σ , pair (i, f ) of vertices of G, and symbol ? ∈ Σ , the language LG = {i?w?f | w ∈ L(G, {i}, {f })} is context-sensitive. Proof Let G be a rational graph labeled by Σ with vertices in Γ ? and de?ned ? and Γ ? be two ?nite alphabets by a family of transducers (Ta )a∈Σ . Let Γ disjoint from but in bijection with Γ . For any x ∈ Γ , we write x ? (resp. x ?) ? (resp. Γ ? ). We consider the rational graph H the corresponding symbol in Γ ? ∪Γ ? de?ned by the family of transducers (Tx )x∈Ξ where labeled by Ξ = Σ ∪ Γ ? for all x ∈ Γ , Tx = { ( u, ux) | u ∈ Γ ? } and Tx ? ? = {(xu, u) | u ∈ Γ }. ? ? ?? ? By Thm. 3, the language L = L(H, ε, ε) ∩ Γ Σ Γ is context-sensitive. ? | i, f ∈ Γ ? and w ∈ L(G, {i}, {f })}. It By construction, L is equal to {? iwf follows that LG is context-sensitive. ? ? 3 Linearly Bounded Graphs 3.1 LBM Transition Graphs Following [6], we de?ne the notion of labeled linearly bounded Turing machine (LLBM). This notion is very close to the notion of o?-line Turing machine

xn /yn x1 /y1

Linearly Bounded In?nite Graphs

7

[13]. It is essentially equivalent to an o?-line Turing machine with a oneway input tape and a two-way linearly bounded work tape. As in standard de?nitions of LBMs, the transition rules can only move the head of the LLBM between the two end markers [ and ]. In addition, a silent step can decrease the size of the con?guration (without removing the markers) and a Σ -transition can increase the size of the con?guration by one cell. This ensures that while reading a word of length n, the labeled LBM uses at most n cells. De?nition 4 A labeled linearly bounded Turing machine is a tuple M = (Γ, Σ, [, ], Q, q0 , F, δ ) as in De?nition 2, where all components but δ are de?ned similarly, and δ is a ?nite set of labeled transition rules of one of the forms: pA ?→qB ± pB ?→qAB

a ε

p[?→q [+ p] ?→qA]

a

ε

p] ?→q ]? pA ?→q

ε

ε

with p, q ∈ Q, A, B ∈ Γ , ± ∈ {+, ?} and a ∈ Σ . Con?gurations are de?ned similarly to the previous case. However, the x transition relation is now labeled. For all x ∈ Σ ∪ {ε}, the relation ?→ is a subset of CM × CM de?ned as: ?→ = { (upAv, uBqv ) | pA ?→ qB + ∈ δ }

M x x M

∪ { (uCpAv, uqCBv ) | pA ?→ qB ? ∈ δ } ∪ { (upAv, uqv ) | pA ?→ q ∈ δ } { (upAv, uqBAv ) | pA ?→ qBA ∈ δ }

wx w x x x

x

with x = ε with x ∈ Σ.

Transitions are composed by de?ning ?→ as (?→ ? ?→) for all w ∈ Σ ? . The de?nition of runs also changes to re?ect the fact that input words are no longer present on the tape but are read as the run progresses. The unique w initial con?guration is thus [q0 ]. A word w is accepted by M if [q0 ] ?→ cf where cf is a ?nal con?guration. M is deterministic if, from any con?guration, either all possible moves are labeled by distinct letters of Σ , or there is only one possible move labeled by ε. Formally, for all con?gurations c, c1 and c2 y x such that c ?→ c1 and c ?→ c2 , either x and y belong to Σ and if c1 = c2 then x = y , or x = y = ε and c1 = c2 . Labeled LBMs are as expressive as classical LBMs. Proposition 2 A language is (deterministic) context-sensitive if and only if it is accepted by a (deterministic) labeled linearly bounded Turing machine. Proof Let us ?rst consider a context-sensitive language L accepted by a terminating LBM N (by Prop. 1). We sketch the construction of a LLBM M = (Γ, Σ, [, ], Q, q0 , F, δ ) accepting L. Let qA , qR and qS be three states in Q. In a con?guration of the form [wqX ] for w ∈ Σ ? and qX ∈ {qA , qR }, M reads an input letter a ∈ Σ and goes to the con?guration [waqs ]. Then it simulates N on wa using only ε-transitions while remembering wa. Using the

8

Arnaud Carayol, Antoine Meyer

same work alphabet as N , this would require the use of 2|wa| cells. However using an increased work alphabet (or a second work tape), this can be done using only |wa| cells. If N accepts (resp. rejects) wa, M restores wa on its (primary) work tape and steps in con?guration [waqA ] (resp. [waqR ]). By taking F = {qA } and q0 = qA if ε belongs to L and q0 = qR otherwise, it is easy to see that the set of words accepted by M from [q0 ] is precisely L. Note that non-deterministic behavior can only appear in N while simulating M . Hence, if M is deterministic then so is N . Conversely, let M be a LLBM accepting a language L ? Σ ? . We describe a LBM N accepting L with two tapes: the input tape and work tape. It is well known that this model is equivalent to LBMs with one tape as presented in Sec. 2.1 (see for example [13]). To each tape corresponds a set of control states: the set of work states QΓ contains the set Q of states of M and the set of input states QΣ is reduced to {qi , qA } respectively the initial and accepting state. The machine N working on word w ∈ Σ ? starts with the con?guration ([qi w], [q0 ]). From a con?guration ([w1 qi w2 ], [uqv ]) with w1 , w2 ∈ Σ ? , q ∈ Q and u, v ∈ Γ ? , N can non-deterministically simulate any ε-transition of N that can be applied to the con?guration represented by the work tape. The deletion rules are simulated by shifting all tape content on the right of the read head by one cell to the left. Moreover N can non-deterministically simulate any a-transition for a ∈ Σ provided that the input head is on top of the symbol a in which case it is moved one cell to the right. The insertion rules are simulated by shifting the work tape content to the right of the read head by one cell on the right. The machine M enters the accepting state qA if the input head is on top of the right border symbol ] and the work state is a ?nal state of N . It follows from the construction of M that w is accepted by M if and only if it is accepted by N . Moreover, if N is deterministic then so is M . ? ? Remark 1 For convenience, one may consider LBMs whose initial con?guration is not of the form [q0 ] but is any ?xed con?guration c0 . This does not add any expressive power, as can be proved by a simple encoding of c0 into the control state set of the machine, which will not be detailed here. Remark 2 For simplicity, the above de?nition forces the insertion of a new tape cell each time a letter is read. More relaxed forms where a cell deletion or rewriting can occur during an input may be considered without any consequence for the results. Similarly, rules which do not move the read head can be allowed. Let M = (Γ, Σ, [, ], Q, q0 , F, δ ) be a LLBM, we de?ne its con?guration graph a CM = (c, a, c′ ) | c ?→ c′ for a ∈ Σ ∪ {ε} .

M

The vertices of this graph are all con?gurations of M , and its edges denote the transitions between them, including ε-transitions. One may wish to only consider the behavior of M from an external point of view, i.e. only looking at the sequence of inputs. This means one has to ?nd a way to conceal ε-transitions without changing the accepted language or destroying the

Linearly Bounded In?nite Graphs

9

structure. One speaks of the transition graph of an acceptor, as opposed to its con?guration graph. In [25], Stirling mentions a normal form for pushdown automata which allows him to consider a structural notion of transition graphs, without relying on the naming of vertices. We ?rst recall this notion of normalized systems adapted to labeled LBMs. A labeled LBM is normalized if its set of control states can be partitioned in two subsets: one set of internal states, noted Qε , which can perform ε-rules and only ε-rules, and a set of external states noted QΣ , which can only perform Σ -rules. More formally: De?nition 5 A labeled LBM M = (Γ, Σ, [, ], Q, q0 , F, δ ) is normalized if there are disjoint sets QΣ and Qε such that Q = Qε ∪ QΣ , F ? QΣ , and pB ?→ qAB ∈ δ =? p ∈ QΣ , pA ?→ qB ± ∈ δ or pA ?→ q ∈ δ =? p ∈ Qε , p ∈ Qε =? for all A ∈ Γ , ?pA ?→ qB ± ∈ δ. This de?nition implies in particular that a control state from which there exists no transition must belong to QΣ . A con?guration is external if its control state is in QΣ , and internal otherwise. This makes it possible to structurally distinguish between internal vertices, which have one or more outgoing ε-edges, and external ones which only have outgoing Σ -edges or have no outgoing edges. Given any labeled LBM, it is always possible to normalize it without changing the accepted language. Proposition 3 Every labeled linearly bounded machine can be normalized without changing the accepted language. Proof Let M be a LLBM, we know from Prop. 2 that the language L accepted by M is context-sensitive. Consider the LLBM M ′ accepting L obtained in the construction of the proof of Prop. 2. It is easy to see that M ′ is normalized: qA and qR are the only states that can perform transitions labeled by Σ , and they cannot perform ε-transitions. All other states can only perform ε-transitions. To verify the third condition in the de?nition of normalized ε LLBMs, it su?ces to add instruction pA ?→ pA for every p and A for which the condition is violated. Moreover, the unique terminal state is qA , which is external. ? ? Remark 3 Normalization as previously described preserves determinism. From this point on, unless otherwise stated, we will only consider normalized LLBMs. We can now de?ne the transition graph of a LLBM as the ε-closure of its con?guration graph, followed by a restriction to its set of external con?gurations (which happens to be a rational set). De?nition 6 Let M = (Γ, Σ, [, ], Q, q0 , F, δ ) be a (normalized) LLBM, and CΣ be its set of external con?gurations. The transition graph of M is GM = (c, a, c′ ) | c, c′ ∈ CΣ , a ∈ Σ, ∧ c ?→ c′ .

M aε? ε ε ε a

10

Arnaud Carayol, Antoine Meyer

a a a

[q0 ] [q1 a] [q0 a] [q0 aa]

[q0 aaa]

b b b

b

[bq1 a]

b

[q1 aaa]

[bq1 aa]

b

[q2 b]

b

[q1 aa]

b

[bq2 b]

a

[bbq1 a] [q3 baa]

b a

a

[q3 ba]

a

a

[bbq2 b] [bq3 ba]

a

Fig. 1 The transition graph of a labeled LBM accepting {(an bn )+ | n ≥ 1}.

We now de?ne the class of linearly bounded graphs as the closure under isomorphism of transition graphs of labeled LBMs. Example 1 Figure 1 shows the transition graph of the normalized LLBM M whose rules are: q0 ] ?→ q0 a] q0 a ?→ q0 aa q0 a ?→ q1 b+ and whose unique accepting state is q2 . This machine accepts the language {(an bn )+ | n ≥ 1}, which is also the language of paths of the graph between vertex [q0 ] and the set [b? q2 b]. For the sake of clarity, only the part of the graph reachable from con?guration [q0 ] is shown. We will see in Sect. 4 that this sub-graph is still a linearly bounded graph.

b a a

q1 a ?→ q1 b+ q1 ] ?→ q2 ]?

ε

b

q2 b ?→ q3 a?

a

q3 b ?→ q3 a? q3 [ ?→ q1 [+

ε

a

3.2 Alternative de?nitions This section provides two alternative de?nitions of linearly bounded graphs. In [8], it is shown that all previously mentioned classes of graphs can be expressed in a uniform way in terms of Cayley-type graphs of certain classes of rewriting systems. We show that it is also the case for linearly bounded graphs, which are the Cayley-type graphs of length-decreasing rewriting systems. The second alternative de?nition we present changes the perspective and directly de?nes the edges of linearly bounded graphs using incremental context-sensitive transductions. This variety of de?nitions will allow us to prove in a simpler way some of the properties of linearly bounded graphs. 3.2.1 Cayley-type graphs of decreasing rewriting systems We ?rst give the relevant de?nitions about rewriting systems and Cayley-type graphs. A word rewriting system R over alphabet Γ is a subset of Γ ? × Γ ? . Each element (l, r) ∈ R is called a rewriting rule and noted l → r. The words

Linearly Bounded In?nite Graphs ε a 0 a 00 a 000 b c 001 b b a 010 b c 01 c 011 b b a 100 b 10 c 101 b b a b a 110 b c 1 c 11 c 111

11

Fig. 2 Cayley-type graph of the rewriting system R = {a → 0, b → b, 0b → 1, 1b → b0, c → c, 1c → ε}, with Σ = {a, b, c} and Γ = {a, b, c, 0, 1}. Rules b → b and c → c ensure that no normal form of R contains b or c. As an example, edge b 01 ?→ 10 is justi?ed by the derivation 01b → 0b0 → 10.

l and r are respectively called the left- and right-hand side of the rule. The rewriting relation of R is the binary relation {(ulv, urv ) | u, v ∈ Γ ? , l → r ∈ R} which we also denote by R, consisting of all pairs of words (w1 , w2 ) such that w2 can be obtained by replacing (rewriting ) an instance of a left-hand side l in w1 with the corresponding right-hand side r. The re?exive and transitive closure R? of this relation is called the derivation of R. Whenever for some words u and v we have uR? v , we say R rewrites u into v . A word which contains no left-hand side is called a normal form. The set of all normal forms of R is written NF(R). One can associate a unique in?nite graph to any rewriting system by considering its Cayley-type graph de?ned as follows: De?nition 7 The Σ -labeled Cayley-type graph of a rewriting system R over Γ , with Σ ? Γ , is the in?nite graph GR = {(u, a, v ) | a ∈ Σ, u, v ∈ NF(R), uaR? v }. The class of rewriting systems we consider is that of ?nite length decreasing word rewriting systems, i.e. rewriting systems with a ?nite set of rules of the form l → r with |l| ≥ |r|, which can only preserve or decrease the length of the word to which they are applied. The reason for this choice is that the derivation relation of such a system coincides with arbitrary compositions of ε-rules of a given labeled LBM. Example 2 Figure 2 shows the Cayley-type graph of a simple decreasing rewriting system.

12

Arnaud Carayol, Antoine Meyer

3.2.2 Incremental context-sensitive transduction graphs The notion of computation graph was ?rst systematically used in [8] (where the terminology used is relation graph ). It corresponds to the graphs de?ned by the transductions (i.e. binary relations on words) associated to a class of ?nite machines. These works prove that for pushdown automata and Turing machines, the classes of transition and computation graphs coincide. We show that it is also the possible to give a de?nition of linearly bounded graphs as the computation graphs of a certain class of LBMs, or equivalently as the graphs de?ned by a certain class of context-sensitive transductions. A relation R is recognized by a LBM M if the language {u#v | (u, v ) ∈ R} where # is a fresh symbol is accepted by M . However, this type of transductions generates more than linearly bounded graphs. Even if we only consider linear relations (i.e relations R such that there exists c and k ∈ N such that (u, v ) ∈ R implies |v | ≤ c · |u| + k ), we obtain graphs accepting the languages recognizable in exponential space (NSPACE[2n ]) which strictly contain the context-sensitive languages (cf Thm. 2). We need to consider relations for which the length di?erence between a word and its image is bounded by a certain constant. Such relations can be associated to LBMs as follows: De?nition 8 A k -incremental context-sensitive transduction T over Γ is de?ned by a LBM recognizing a language L ? {u#v | u, v ∈ Γ ? and |v | ≤ |u| + k } where # does not belong to Γ . Relation T is de?ned as {(u, v ) | u#v ∈ L}. The synchronized relations of ?nite image (i.e for u there are ?nitely many v such that (u, v ) ∈ R) provide a ?rst example of k -incremental contextsensitive transductions. Proposition 4 For any synchronized relation R of ?nite image, there exists a constant k ∈ N such that R is a k -incremental context-sensitive transduction. Proof Let R ? Γ ? × Γ ? be a synchronized relation of ?nite image. It follows from the de?nition of synchronized relations that R is equal to a ?nite union: ? ? Si · (Ai × ε)

i∈I

where for all k ∈ I ∪ J , Sk is a length-preserving relation1 and for all i ∈ I and j ∈ J , Ai and Bj are rational subsets of Γ ? . As R has a ?nite image, for all j ∈ J the set Bj is necessarily ?nite. Let k be the maximal length of a word in j ∈J Bj , it is easy to check that for all pairs of words (u, v ) ∈ R, |v | ≤ |u| + k . Moreover the language {u#v | (u, v ) ∈ R} is context-sensitive. Hence R is a k -incremental context-sensitive transduction. ? ? The following proposition states that incremental context-sensitive transductions of a given level form a Boolean algebra.

1

∪ ?

j ∈J

Sj · (ε × Bj )?

A synchronized relation R is length-preserving if ?(x, y ) ∈ R, |x| = |y |

Linearly Bounded In?nite Graphs

13

Proposition 5 For all k -incremental context-sensitive transductions T and T ′ over Γ ? , T ∪ T ′ , T ∩ T ′ and T = Ek ? T (where Ek is {(u, v ) | 0 ≤ |v | ≤ |u| + k }) are incremental context-sensitive transductions. Proof The closure under union follows from that of context-sensitive languages. The proof of closure under complement is a straightforward consequence of the closure under complement of context-sensitive languages (cf Thm. 1). Let T ? Γ ? × Γ ? be a k -incremental context-sensitive transduction. By de?nition, the set L = {u#v | (u, v ) ∈ T } is context-sensitive. It is straightforward to check that the set L′ = {u#v | (u, v ) ∈ Ek ? T } is equal to: L ∩ {u#v | |u| ≤ |v | + k }. As the context-sensitive languages are closed under complement and inter? is a k -incremental context-sensitive section, L′ is context-sensitive. Hence, T transduction. ? ? The canonical graph associated to a ?nite set of transductions is called a transduction graph. Relating graphs to a class of binary relations on words was already used to de?ne rational graphs and their sub-classes. De?nition 9 The Σ -labeled transduction graph of a ?nite set of incremental context-sensitive transductions (Ta )a∈Σ is GT = {(u, a, v ) | a ∈ Σ and (u, v ) is recognized by Ta }. Example 3 The linearly bounded graph of Ex. 1 is isomorphic to the transduction graph of the following set of incremental context-sensitive transductions: Ta = {(#an , #an+1 ) | n ≥ 0} ∪ {(bm an , bm?1 an+1 ) | m ≥ 1, n ≥ 0}, Tb = {(#an , an?1 b) | n ≥ 1} ∪ {(am bn , am?1 bn+1 ) | m ≥ 1, n ≥ 0}. The symbol # is needed to distinguish a vertex directly reachable through a sequence of a’s from a vertex reachable through a sequence of the form (an bn )? . As for the Cayley-type graph of Ex. 2, it can be seen as the transduction graph of the set of incremental context-sensitive transductions {Ta , Tb , Tc }, where Ta adds a 0 and Tc removes a 1 to the right of a binary number, and Tb implements binary increment. Length-preserving context-sensitive transductions have already been extensively studied in [18]. In the rest of this presentation, unless otherwise stated, we will only consider 1-incremental transductions without loss of generality regarding the obtained class of graphs: indeed, any k -incremental transduction graph is isomorphic to a 1-incremental one over an increased alphabet.

14

Arnaud Carayol, Antoine Meyer

3.2.3 Equivalence of all de?nitions We now prove that both classes of Cayley-type graphs of decreasing rewriting systems, and incremental context-sensitive transduction graphs de?ne precisely the class of linearly bounded graphs, up to isomorphism (i.e. up to vertex renaming). Theorem 4 For any graph G, the following statements are equivalent: 1. G is isomorphic to the transitions graph of a labeled LBM, 2. G is isomorphic to the Cayley-type graph of a ?nite length-decreasing system, 3. G is isomorphic to a context-sensitive transduction graph. Proof 1 =? 2: Let M = (Γ, Σ, [, ], Q, q0 , F, δ ) be a normalized labeled linearly bounded Turing machine, with Σ ∩ Γ = ?. As M is normalized, its control states can be partitioned into QΣ and Qε (see De?nition 5). Let Γ ′ = Γ ∪ {[, ]}. We build a ?nite length-decreasing rewriting system R whose Cayley-type graph is the transition graph of M . Let the alphabet of R be ′ ? = Σ ∪ Γ ′ ∪ (Γ ′ × Q) ∪ S , where S = {va , va , sa | a ∈ Σ } is a new set of symbols disjoint from Γ and Q. Elements (x, q ) of Γ ′ × Q will be noted xq . For convenience, for any set X , X? will denote X ∪ (X × QΣ ), and x? any symbol in {x}? . There are several important points which the rules of R must ensure:

? 1. Only words of the form (ε ∪ [? ) Γ? (ε ∪ ]? ), i.e. words in which only external control states may occur and in which no symbol occurs to the left of a left bracket or to the right of a right bracket, should be normal forms (please be aware that Γ? denotes the set Γ ∪ (Γ × QΣ ), and not Γ ∪ (Γ × Q)):

x[? → [? ,

]? y →]? ,

′

s→s

for all x ∈ ?, y ∈ ? \ Σ, s ∈ Σ ∪ S ∪ (Γ × Qε ). 2. When a letter a in Σ is added to the right of an irreducible word u, one should ensure that u actually represents a legal con?guration2 , i.e. that u is of one of the forms [q Γ ? ], [Γ ? Aq Γ ? ] or [Γ ? ]q for A ∈ Γ , q ∈ Q: ]a → va ], ]q a → va ′ ]q , Ava → va A, [q va → [sa , Aq va → va ′ Aq , [va ′ → [sa . Ava ′ → va ′ A,

3. Finally, once it has been made sure that the word represents a legitimate LBM con?guration, one should simulate an insertion operation followed by any number of ε-transitions of the LBM: sa A → Asa ,

a

sa Bp → Cq B

for all a ∈ Σ, A, B, C ∈ Γ and pB ?→ qCB ∈ δ , and Ap C → BCq ,

ε ε

CAp → Cq B

ε

Ap C → Cq

for all pA ?→ qB +, pA ?→ qB ?, pA ?→ q ∈ δ (respectively).

Note that this encoding of con?guration di?ers from the one used previously, where control states were standalone symbols.

2

Linearly Bounded In?nite Graphs

a

15

There is an edge u ?→ v in the Cayley-type graph GR of R if and only if u and v are words representing valid con?gurations of M from which no ε-transition can be performed, i.e. observable con?gurations, and there exists a sequence of transitions labeled by aε? of M by which u reaches v . There is a bijection between the edges and vertices of GR and the transition graph of M , hence these two graphs are isomorphic. 2 =? 3: Let R be a ?nite length-decreasing rewriting system, GR its Cayley-type graph. For each letter a, we will show that the relation Ta = {(ua, v ) | u ?→ v } = {(ua, v ) | u, v ∈ NF(R) ∧ uaR? v }

GR a

is an incremental context-sensitive transduction by building a LBM Ma = (Γ, Σ, [, ], Q, q0 , F, δ ) recognizing Ta . For every pair (ua, v ), Ma starts in con?guration ua#v , and ?rst has to check that u is a normal form of R by verifying that it contains no lefthand side of any rule in R. Second, Ma simulates the derivation of R on ua, applying one rewriting rule at a time until a normal form is reached. Due to non-determinism, there might be unsuccessful runs, but the pair is accepted if and only if one run reaches con?guration v #v , meaning that R can normalize ua into v . Hence, a pair (ua, v ) is in Ta if and only if (u, a, v ) ∈ GR , meaning that the transduction graph of (Ta )a∈Σ is isomorphic to GR . 3 =? 1: Let T = (Ta )a∈Σ be a ?nite set of incremental contextsensitive transductions de?ning a graph GT , each Ta being recognized by an LBM Ma . We informally describe a normalized labeled LBM M whose transition graph GM is isomorphic to GT . Let q be the unique external control state of M , M should have a run labeled by aε? between con?gurations qu and qv whenever (u, v ) ∈ Ta , or equivalently whenever the word u#v is accepted by Ma . This is done as follows. First, starting from con?guration qu, M should perform an a-labeled transition, increasing its available tape space by 1, and step into an internal control state. It should then guess a word v , and write u#v on its tape. Since Ta is incremental, this can be done using no more than |u| + 1 tape cells by writing two symbols in each cell. Then, M simulates the LBM Ma on input word u#v , while keeping an intact copy of v on the tape (this can again be done by a simple alphabet encoding). If the simulated run of Ma succeeds, M steps into external con?guration qv by restoring the saved copy of v on the tape, otherwise it loops in a non-accepting internal state. By this construction, there is an edge (qu, a, qv ) in GM if and only if there is an edge (u, a, v ) in GT , hence both graphs are isomorphic. ? ? This shows that the three types of graphs presented in this section actually all de?ne the same class, namely that of linearly bounded graphs. This variety of de?nitions will allow us to prove in a simpler way some of the properties of linearly bounded graphs. 4 Structural properties Now that the class of linearly bounded graphs has been de?ned using three di?erent formalisms, we can easily deduce some of their structural properties.

16

Arnaud Carayol, Antoine Meyer

In particular, we look at the languages accepted by linearly bounded graphs and some of their closure properties. We also give some insight about the relation between linearly bounded graphs and deterministic context-sensitive languages, and conclude with a few logical properties. But ?rst, we compare our notions to related work.

4.1 Comparison with existing work We now give a precise comparison of linearly bounded graphs with the restriction of Turing graphs ([6]) to the linearly bounded case, and with the con?guration graphs considered in [16]. 4.1.1 Con?guration graphs In [16], the con?guration graphs of a class of o?ine linearly bounded machines very similar to our labeled LBM are considered. However, they include in their de?nition a restriction to the set of con?gurations reachable from the initial con?guration. Therefore, their class of con?guration graphs is incomparable to ours. As we will see in Prop. 8, the linearly bounded graphs are closed under restriction to the set of vertices reachable from a given vertex. Hence, it is not necessary to impose this restriction directly in the de?nition of the con?guration graph. Apart from this restriction, our class of con?guration graphs coincides with the con?guration graphs of [16] and with those of [6] in the case of linearly bounded Turing machines. 4.1.2 Transition graphs Knapik and Payet do not consider transition graphs: instead of characterizing the ε-closure of con?guration graphs, they prove a closure property of this class up to weak bisimulation [19], which is not a structural characterization. Nevertheless, it is straightforward to prove that their results can be extended to the class of transition graphs considered up to isomorphism, as mentioned in Sect. 4. In [6], Caucal de?nes the transition graphs of Turing machines from their con?guration graphs using the very general notion of ε-closure: wherever there is a path labeled by ε? aε? in the con?guration graph, there is an edge labeled by a in its ε-closure, for every letter a. Furthermore, the de?nition allows the restriction to an arbitrary rational set of vertices (potentially the whole set of vertices). Figure 3 illustrates on a small con?guration graph the di?erence between these two approaches. Our approach has two main advantages. First, the ε-closure operation as de?ned by Caucal may give rise to spurious non-determinism in the obtained graphs. This additional complexity is arti?cial and is eliminated using our de?nition. Furthermore, our notion is purely structural, and does not rely on the naming of vertices. But interestingly, we can show that both classes still coincide up to isomorphism: for every labeled linearly bounded machine

Linearly Bounded In?nite Graphs a a

1

17

a

2

ε

3

ε

4

b

5

1

a

2

3

4

b

5

1

a

4

b

5

b b (a ) (b) (c)

Fig. 3 (a) Normalized LLBM con?guration graph. (b) Transition graph of (a) as de?ned in [6] (with no restriction on vertices). (c) Linearly bounded graph associated to (a).

M and rational set R, one can de?ne a machine M ′ such that the transition graph of M following Caucal’s de?nition with respect to R is isomorphic to the linearly bounded graph corresponding to M ′ in our framework. Proposition 6 The class of linearly bounded graphs coincides, up to isomorphism, with the restriction of Turing graphs to the (uniform) linearly bounded case. Proof Let M be a normalized LLBM, C its con?guration graph, R its (rational) set of external con?gurations and G its transition graph de?ned as G = {c ?→ c′ | c, c′ ∈ R ∧ c ?→ c′ ∈ C }. Consider the graph G′ de?ned as the restriction to R of the ε-closure of C . G′ = {c ?→ c′ | c, c′ ∈ R ∧ c ?→ c′ ∈ C }. The graphs G and G′ are equal, since by de?nition of external vertices, they have no outgoing ε-transitions. Conversely, let M be a (not necessarily normalized) LLBM, C its con?guration graph, and R a rational set of con?gurations of M . The binary relation ε? aε? ?→ in C × C is a 1-incremental context-sensitive transduction. Hence the graph G de?ned as the restriction to R (see Prop. 8) of the ε-closure of C is a linearly bounded graph. ? ? 4.2 Languages It is quite obvious that the language of the transition graph of a LLBM M between the vertex representing its initial con?guration and the set of vertices representing its ?nal con?gurations is the language of M . In fact, the choice of initial and ?nal vertices has no importance in terms of the class of languages one obtains. Proposition 7 The languages of linearly bounded graphs between an initial vertex i and a ?nite set F of ?nal vertices are the context-sensitive languages.

a ε? aε? a aε?

18

Arnaud Carayol, Antoine Meyer

Proof Let G be a linearly bounded graph labeled by Σ de?ned by a family (Ta )a∈Σ of 1-incremental context-sensitive transductions. We will prove that L(G, i, F ) is context-sensitive even if F is a context-sensitive set. Let # ∈ Σ be a new symbol, we consider the graph G obtained from G by adding a loop labeled by # on each vertex in F . Obviously, G is a linearly # bounded graph as ?→= {(f, f ) | f ∈ F } is a 0-incremental context-sensitive transduction. By Thm. 4, G is the transition graph of a LLBM M . Let c0 be the con?guration of M corresponding to the vertex i in G. Consider the LLBM M ′ whose initial con?guration is i (see Rem. 1) and whose set of ?nal states are the states that appear in the left-hand side of a #-rule (without loss of generality, we can assume that the #-rules do not depend on the current value of the cell). It is easy check that M ′ accepts L(G, i, F ) and by Prop. 2, L(G, i, F ) is context-sensitive. For the converse implication, let L be a context-sensitive language and M the normalized LLBM constructed in Prop. 2 accepting L. The transition graph of M traces L from the initial con?guration to an in?nite set of con?gurations (i.e the con?gurations with state qA ). Therefore, we need to adapt the construction of Prop. 2. We add a new state qf to the machine M and whenever M makes an ε-transition to enter state qA , we add the ability to enter con?guration [qf ] by a sequence of ε-transitions. As [qf ] has no out-going edges, it is an external con?guration and it is easy to see that L = L(G, c0 , [qf ]). ? ? Remark 4 When a linearly bounded graph is explicitly seen as the transition graph of a LLBM, as a Cayley-type graph or as a transduction graph, i.e. when the naming of its vertices is ?xed, considering context-sensitive sets of ?nal vertices does not increase the accepted class of languages. 4.3 Closure properties Linearly bounded graphs enjoy several good properties, which will be especially important when comparing them to other classes of graphs related to LBMs or context-sensitive languages (see Section 5). Proposition 8 The class of linearly bounded graphs is closed under restriction to reachable vertices from any vertex and under restriction to a contextsensitive set of vertices. Proof We ?rst prove the closure under restriction to a context-sensitive set of vertices. Let G be a linearly bounded graph de?ned by a family of (Ta )a∈Σ of 1-incremental context-sensitive transduction. By Prop. 5, the transduction Ta ∩{(u, v ) | u ∈ F, v ∈ F and|v | ≤ |u| +1} is 1-incremental context-sensitive. It follows that G|F is a linearly bounded graph. Let us now prove the closure of linearly bounded graphs under restriction to reachable vertices. Let G be a linearly bounded graph given by a family of 1-incremental context-sensitive transductions (Ta )a∈Σ and u0 a vertex in VG . Each transduction Ta for a ∈ Σ is accepted by a LBM Ma . Consider the graph G′ obtained by restricting G to its set of vertices reachable from u0 .

Linearly Bounded In?nite Graphs ? a ?a b b # ?b b # ?bb ?bb? # ?bb?2 # ?bb?3 # ?bb?4 # bb ?b? # ?b?2

19

Fig. 4 The graph G for some L containing bb but not b.

Note that this set is in general not context-sensitive, as illustrated by the following example. Example 4 Consider a language L ? {a, b}? that is recognizable in exponential space but not in linear space (i.e. L ∈ NSPACE[2n ] \ NSPACE[n]). The existence of such a language is guaranteed by Thm. 2. Consider the graph G labeled by {a, b, ?} and de?ned by: – ?u ?→ ?ux for all u ∈ {a, b}? and x ∈ {a, b}, – –

G n ? ?u? ?→ ?u?n+1 for all u ∈ {a, b}? G |u| ? and ?u?2 ?→ u for all u ∈ L. G x

and n + 1 ≤ 2|u| ,

The edge relations of this graph are 1-incremental context-sensitive transductions, hence G is linearly bounded. Figure 4 illustrates the construction of this graph. The set of vertices reachable from ? restricted to {a, b}? is precisely the language L which by de?nition is not context-sensitive. Therefore, we need to adopt a di?erent naming of the vertices of G′ . We construct a graph H isomorphic to G′ which is de?ned by a family of 1incremental context-sensitive transductions. For any pair of vertices u and v ∈ VG , we write u ?n v if there exists a path from u to v in G using only vertices of size less than or equal to n. Note that since u and v are considered as part of any path between u and v , then necessarily n ≥ max(|u|, |v |). The set of vertices of H is VH = {u n | u ∈ Γ ? , u0 ?|u|+n u and u0 ?|u|+n?1 u}. Note that for all u ∈ VG′ , there is a unique n such that u n ∈ VH , and that a u ∈ VG \ VG′ =? u n ∈ VH for all n. For all a ∈ Σ , we take u n ?→ v m i? u

n

∈ VH , v

m

∈ VH and u ?→ v .

G

a

H

The graph H is isomorphic to G′ . It is easy to see that the mapping ρ ∈ VG′ → VH associating to every u ∈ VG′ the unique u n ∈ VH is a bijection and a graph morphism from G′ to H . We ?rst prove that VH is a context-sensitive and that for all a ∈ Σ , ?→ is a 1-incremental contextsensitive transduction. It will then follow that H and G′ are linearly bounded.

H

20

Arnaud Carayol, Antoine Meyer

1. Consider the language L+ equal to {u n | u0 ?|u|+n u, n ∈ N} and the language L? equal to {u n | u0 ?|u|+n?1 u, n ∈ N}, it is easy to check that VH = L+ ∩ L? . If we prove that L+ and L? are context-sensitive languages, it follows by Thm. 1 that VH is a context-sensitive language. We construct a LBM M accepting L+ . When starting with u n , M guesses a path from u0 to u with vertices of length at most |u| + n. It starts with u0 and guesses a word u1 of length at most |u| + n then a simulates one of the Ma ’s to check that u0 ?→ u1 . Finally, M replaces u0 by u1 and iterates the process until ui is equal to u. This can be done using at most 3(|u| + n) cells. A similar construction allows to recognize L? . a 2. For all a ∈ Σ , u n ?→ v m implies that |v | + m ≤ |u| + n + 1, because u0 ?|u|+n u, u ?→ v and ?→ is 1-incremental. Therefore, ?→ is 1incremental. The language La = {u

G G H n a H a a G

?v

m

| u ?→ v } is accepted by a LBM that

H

a

checks that u n and v m belong to VH (by simulating a machine accepta a ing VH ) and that u ?→ v . Hence ?→ is a 1-incremental context-sensitive transduction.

G H

? ?

Example 5 This last construction applied to the graph of Ex. 4 gives the graph H de?ned by: – ?u ?→ ?ux for all u ∈ {a, b}? and x ∈ {a, b}, – –

G ? ?u?n ?→ ?u?n+1 for all u ∈ {a, b}? and G |u| |u| ? and ?u?2 ?→ u 2 +1 for all u ∈ L. G x

n + 1 ≤ 2|u| ,

Since all rational languages are context-sensitive, linearly bounded graphs are also closed under restriction to a rational set of vertices. This shows that it is not necessary to allow arbitrary rational restrictions in the de?nition of transition graphs of linearly bounded machines, since such a restriction can be directly applied to the set of external con?gurations of a machine. Finally, we can extend the result of [16] to the class of linearly bounded graphs, and show that they are closed under synchronized products [1]. The synchronized product of two graphs G and G′ with labels in Σ and Σ ′ with respect to a set of constraints C ? Σ × Σ ′ is the graph G ? G′ = {(u, v ) ?→ (u′ , v ′ ) | u ?→ u′ ∧ v ?→ v ′ ∧ (a, b) ∈ C }.

G G (a,b) a b

Proposition 9 The class of linearly bounded graphs is closed under synchronized products, up to isomorphism. Proof It is straightforward from this de?nition that if G and G′ are both linearly bounded, de?ned for instance as context-sensitive transduction graphs, the binary edge relations of their synchronized product are also incremental context-sensitive transductions. ? ?

Linearly Bounded In?nite Graphs

21

ε ε a ε ε ε ε ε b

ε a b

Fig. 5 Con?guration graph and deterministic transition graph of a non-deterministic labeled LBM

4.4 Deterministic linearly bounded graphs We now consider the relations between the determinism of linearly bounded graphs and the determinism of the linearly bounded machines de?ning them. As a ?rst remark, it is straightforward to notice that there exist non-deterministic labeled LBMs whose transition graphs are deterministic. More precisely, any machine in which, from any given con?guration, at most one external con?guration is reachable by a partial run labeled by ε? , has a deterministic transition graph. Figure 5 illustrates this fact. In fact, we can show that any LLBM can be transformed (while preserving the accepted language) in order to verify this property. Consequently, as expressed by the following proposition, all context-sensitive languages can be accepted by a deterministic linearly bounded graph. Proposition 10 For every context-sensitive language L, there exists a deterministic linearly bounded graph G, a vertex i and a rational set of vertices F of G such that L = L(G, {i}, F ). Moreover, G can be chosen to be a tree. Proof Let L ? Σ ? be a context-sensitive language, we build a linearly bounded graph G labeled by Σ whose vertices are words of the form Aw or Rw, with w ∈ Σ ? and A, R ∈ Σ , and whose edges are de?ned by the following 1-incremental context-sensitive transductions: Au ?→ Aua, Rv ?→ Ava Au ?→ Rua, Rv ?→ Rva

a a a a

for all u ∈ L, v ∈ L and ua, va ∈ L, for all u ∈ L, v ∈ L and ua, va ∈ L.

The language of this deterministic graph between vertex X where X is equal to A if ε ∈ L or equal to R if ε ∈ L and the rational set AΓ ? is precisely L. Moreover, G is a tree isomorphic to the complete in?nite Σ -labeled tree. ? ? Remark 5 The previous result does not stand for a ?nite set of ?nal vertices even if we only consider deterministic context-sensitive languages. Consider for example, the language L = {(an b)? |n ∈ N}. Suppose that there exists a deterministic graph G such that L = L(G, i, F ) for some ?nite set F , then there would exists m = n, such that i ?→ f and i ?→ f . As f ?→ f ′ for some f ′ ∈ F , it would follow that i ?→ f ′ .

G G an bam b G G an b am b am b

22

Arnaud Carayol, Antoine Meyer

ε a ε

ε b ε a b

Fig. 6 Con?guration graph and deterministic transition graph of a non-deterministic terminating labeled LBM

Of course, we cannot conclude from this that the languages of deterministic linearly bounded graphs are the deterministic context-sensitive languages, which would amount to answering the general question raised by Kuroda [17] whether deterministic and non-deterministic languages coincide. However, if we only consider terminating linearly bounded machines (which have no in?nite run on any given input word) the class of transition graphs we obtain faithfully illustrates the determinism of the languages. Remark 6 Even for terminating LLBMs, the determinism of a transition graph does not imply that the machine de?ning it is deterministic. Figure 6 illustrates this fact. The idea of the following proof is to show that any terminating LLBM whose transition graph is deterministic can be determinized without changing the structure of the graph. Proposition 11 The languages of deterministic transition graphs of terminating linearly bounded machines (between an initial vertex and a rational set of ?nal vertices) are the deterministic context-sensitive languages. Proof Let L be a deterministic context-sensitive language. By Prop. 2, there exists a deterministic terminating LLBM M accepting L. By de?nition, its transition graph GM is deterministic, and it accepts L between the vertex corresponding to the initial con?guration and those corresponding to the ?nal con?gurations of M . Conversely, let GM be the deterministic transition graph of a terminating LLBM M = (Γ, Σ, [, ], Q, q0 , F, δ ), we construct a deterministic LLBM N whose transition graph GN is equal to GM . The machine N is obtained from M by keeping exactly one rule in δ with a given left-hand side and label. The machine N is equal to (Γ, Σ, [, ], Q, q0 , F, δ ′ ) where δ ′ is a subset of δ : – if pA ?→ qU ∈ δ then there exists pA ?→ q ′ U ′ ∈ δ ′ , x x – if pA ?→ qU ∈ δ ′ then for all pA ?→ q ′ U ′ ∈ δ ′ , q = q ′ and U = U ′ . By construction, N is deterministic. Moreover, the set of external con?gurations of N is equal to the set of external con?gurations of M . It remains to a prove that for any two external con?gurations c and c′ , c ?→ c′ if and only if c ?→ c′ .

GN a GM x x

Linearly Bounded In?nite Graphs

a

23

If c ?→ c′ , there exists a path between c and c′ labeled by aε? in the

GM

con?guration graph CM of M . As GM is deterministic and terminating, any maximal path in CM labeled by aε? ends in c′ . This property still holds for the con?guration graphs of CN . Suppose by contradiction that there exists a maximal path in CN labeled by aε? starting from c and ending in c′′ = c′ . This implies the c′′ has out-going ?-edges in CM and not in CN which is impossible by construction of N . a a Conversely if c ?→ c′ then, by construction of N , we have c ?→ c′ . Hence,

GN GM

it follows that GM = GN .

? ?

Remark 7 Other equivalent de?nitions of deterministic transition graphs of terminating labeled LBMs can be given: they coincide with the Cayley-type graphs of length-decreasing rewriting systems with unique normal forms3 , and to the graphs of deterministic terminating incremental context-sensitive transductions. The intuitive reason behind this equivalence is that, in every such case, for each label the corresponding edge relation of the graph is a partial function from vertices to vertices. Remark 8 One can not use the previous constructions to determinize any LLBM. Indeed, the construction from Prop. 10 produces non terminating machines in general, and the construction from Prop. 1 does not preserve the structure of a machine’s transition graph.

4.5 Logical properties To conclude this section on properties of linearly bounded graphs, we investigate the decidability of the ?rst-order theory of con?guration graphs of LLBMs and linearly bounded graphs. Due to the high expressive power of the model considered, only local properties expressed in ?rst-order logic can be checked on LLBM con?guration graphs. Proposition 12 Con?guration graphs of linearly bounded Turing machines have a decidable ?rst-order theory. Proof This is a direct consequence of the fact that con?guration graphs of LLBMs are synchronized rational graphs, which have a decidable ?rst-order theory [2,15]. ? ? However, as remarked by [16], there exists no algorithm which, given a LLBM M and a ?rst-order sentence φ, decides whether the transition graph of M satis?es φ. This statement can be strengthened to the following proposition. Proposition 13 There exists a linearly bounded graph with an undecidable ?rst-order theory.

A rewriting system has unique normal forms if any word can be derived into at most one normal form.

3

24

Arnaud Carayol, Antoine Meyer

Proof Consider a ?xed enumeration (Mn )n∈N of all (unlabeled) Turing machines, and a labeled Turing machine M whose language is the set of all words of the form #n such that machine Mn halts on the empty input. Using only ε-transitions, M guesses a number n and writes #n on its tape, then simulates machine number n on the empty input. If the machine halts, then M reads word #n and stops. All accepting runs of M are thus labeled by ε? #n for some n. When replacing ε by an observable symbol τ , the con?guration graph C of M is a linearly bounded graph. Let C ′ be its restriction to vertices reachable from the initial con?guration of M , the graph C ′ is still linearly bounded by Prop. 8. For all n, the formula φn expressing the existence of a path labeled by τ #n ending in a vertex with no successor is satis?ed in C ′ if and only if machine Mn halts on input ε. The set of all such satis?able formulas is not recursive. Hence the ?rst-order theory of C ′ is undecidable (not even recursively enumerable). ? ? 5 Comparison with rational graphs We will now give some remarks about the comparison between linearly bounded graphs and several di?erent sub-classes of rational graphs. First note that since linearly bounded graphs have by de?nition a ?nite degree, it is therefore only relevant to consider rational graphs of ?nite degree. However, even under this structural restriction, rational and linearly-bounded graphs are incomparable, due to the incompatibility in the growth rate of their vertices’ degrees. A ?rst observation is that in a rational graph the out-degree at distance n n from any vertex can be cc for some constant c, whereas in a linearly bounded graph it is at most cn . Lemma 1 For any linearly bounded graph G and any vertex x, there exists c ∈ N such that the out-degree of G at distance n > 0 of x is at most cn . Proof Let (Ta )a∈Σ be a set of incremental context-sensitive transductions describing G and ka ∈ N such that Ta is a ka -incremental context-sensitive transduction. We take k to be the maximum of {ka | a ∈ Σ } ∪ {|x|}. At distance n > 0 of x, a vertex has length at most k (n + 1) and hence the outdegree is bounded by the number of vertices of length at most k (n + 2) which is less than |Γ |k(n+2)+1 . Hence, there exists c ∈ N such that the out-degree is bounded by cn . ? ? Figure 7 shows a rational graph whose vertices at distance n from the n+1 root A have out-degree 22 . This graph is thus not linearly bounded. Conversely, in a rational graph of ?nite degree, the in-degree at distance n n from any vertex is at most cc for some c ∈ N, in a linearly bounded graph it can be as large as f (n) for any mapping f from N to N recognizable in linear space (i.e. such that the language {0n 1f (n) | n ∈ N} is context-sensitive). Lemma 2 For any mapping f : N → N recognizable in linear space, there exists a linearly bounded graph G with a vertex x such that the in-degree at distance n > 0 of x is f (n).

Linearly Bounded In?nite Graphs

A/AA A/AB A/BA A/BB

BA BB

25

A

AA

AB

T:

AAAA

... ...

ABAA

... ...

BBBB

AAAAAAAA

AAABBABB

BBBBBBBB

B/AA B/AB B/BA B/BB

Fig. 7 A ?nite degree rational graph (together with its transducer) which is not isomorphic to any linearly bounded graph.

ε 0 0n

01

0n 1

01f (1)?1

0n 12

01f (1)

0n 1f (n)?1

0n 1f (n)

Fig. 8 A linearly bounded graph which is not isomorphic to any rational graph.

Proof Let f be a mapping from N to N recognizable in linear space, and let Gf be the linearly bounded graph de?ned using the following incremental context-sensitive transduction: T = {(u, u0) | u ∈ 0? } ∪ {(u, u1) | u ∈ 0n 1m , m < f (n)} ∪ {(uv, u) | u ∈ 0? , v ∈ 1? and |v | ≤ f (|u|)}. Note that, since context-sensitive languages are closed under complement, it is not di?cult to see that the set {0n 1m | m < f (n)} is context-sensitive for every f recognizable in linear space. Figure 8 illustrates the construction of Gf . The in-degree of vertex 0n at distance n from the root ε is equal to f (n), for any mapping f recognizable in linear space. ? ? An instance of such a mapping is f : n → 22 , which is more than the in-degree at distance n of a vertex in any rational graph of ?nite degree. From these two observations, we easily get: Proposition 14 The classes of ?nite degree rational graphs and of linearly bounded graphs are incomparable. Since ?nite-degree rational graphs and linearly bounded graphs are incomparable, we investigate more restricted sub-classes of rational graphs. For synchronized graphs of ?nite out-degree, we have the following result:

2n

26

Arnaud Carayol, Antoine Meyer

Proposition 15 The synchronized graphs of ?nite out-degree form a strict sub-class of linearly bounded graphs. Proof By Prop. 4, the synchronized relations of ?nite image are k -incremental. Hence, the synchronized graphs of ?nite out-degree are linearly bounded graphs. The strictness can be deduced from the fact that synchronized graphs are not closed under restriction to reachable vertices from a given vertex (cf Prop. 8), or that synchronized graphs have decidable ?rst-order theories (cf Prop. 13). ? ? By restricting the out-degree even further, we can establish the following comparison: Theorem 5 The rational graphs of bounded out-degree form a sub-class of linearly bounded graphs (up to isomorphism). Proof The inclusion result is based on a uniformization result for rational relations of bounded image due to Weber. A relation is said to be k -valued if for all w ∈ Dom(R), we have |{x | (w, x) ∈ R}| ≤ k . In [28], it is proved that for any k -valued rational relation R, there exist k rational functions4 F1 , . . . Fk such that R = i∈[1,k] Fi . Let G = (Ta )a∈Σ be a rational graph over Γ whose out-degree is bounded by k . Each relation Ta is therefore k -valued and hence there exist k rational functions Fa1 , . . . Fak such that Ta = i∈[1,k] Fai . We write X = {ai | a ∈ Σ and i ∈ [1, k ]}. We will represent each vertex x of G by a pair (w, t) ∈ VG × X ? such that x = Ft|t| (. . . (Ft1 (w))). However, there can be several such pairs for a given vertex. We de?ne a total order < on VG × X ? and associate to x the smallest such pair. First, let <Γ and <X be two arbitrary total orders over Γ and X respectively and let ?Γ and ?X be the lexicographic orders induced by <Γ and <X respectively. (m, t) < (n, r) i? |m| + |t| < |n| + |r| or |m| + |t| = |n| + |r| and m ?Γ n or |m| + |t| = |n| + |r|, m = n and t ?X r

It is straightforward to prove that < is a total order on VG ×X ? . We now prove that the function N associating to any pair (w, t) the smallest pair (m, r) such that Ft (w) = Fr (m) is a 0-incremental context-sensitive transduction. There are two important points in this proof. The ?rst one is to be able to check in linear space that for any two given pairs (m, r) and (w, t), Fr (m) = Ft (w). In other terms, we want to prove that the language L = {m?r$t?w | Fr (m) = Ft (w)} is context-sensitive. ? be a ?nite alphabet disjoint from but in bijection with X (for all Let X ? ) , we consider the x ∈ X , we write x ? for the corresponding symbol in X ? ?a rational graph G de?ned by the family of transducers (Fa )a∈X ∪ (F ? )a∈X ?1 ?, F ?a where for all a ?∈X = F . It is easy to check that for all m, w ∈ Γ? ? a

A rational relation which maps exactly one image to each element of its domain is called a rational function.

4

Linearly Bounded In?nite Graphs

? rt ? G

27

and all r, t ∈ X ? , there exists a path m =? w i? Fr (m) = Ft (w) where ? i, f )}∩ Γ ? ?X ? X ? ? ?Γ ? ?= t ?|t| . . . t ?1 . By Cor. 1, the language {i?w?f | w ∈ L(G, t is a context-sensitive language. It follows that L is also context-sensitive. The second point is to show that the language L′ = {m?r$t?w | N ((w, t)) = (m, r)} is itself context-sensitive, which implies that N is indeed a contextsensitive transduction. Given (w, t) and (m, r), let (m1 , r1 ), . . . , (mk , rk ) be an enumeration of all pairs smaller than (m, r) with respect to <. A linearly bounded machine accepting L′ successively tests for all i ∈ [1, k ] whether mi ?ri $t?w ∈ L, which is possible since L is context-sensitive and contextsensitive languages are closed under complement. If any of these k tests fails, then the whole computation fails. Otherwise, it only remains to check that mi ?ri $t?w ∈ L. N is 0-incremental since by de?nition of the total order <, (m, r) < (w, t) =? |m| + |r| ≤ |w| + |t|, and all steps of the construction of the machine accepting L′ can be done in linear space. We can now de?ne the linearly bounded graph G′ with vertices in Γ ? #X ? using the set of transductions (Ta )a∈Σ with: Ta =

i∈[1,k]

{(w#x, w′ #y ) | N ((w, x)) = (w, x) and N (w, xai ) = (w′ , y )}.

As N is 0-incremental, Ta is 1-incremental. The mapping ρ from VG to VG × X ? associating to a vertex x ∈ VG the smallest (w, t) such that x = Ft (w) is a bijection from VG to VG′ , which induces an isomorphism from G to G′ . Hence, G is a linearly bounded graph, which concludes the proof of inclusion. ? ? Example 6 Let Γ be a singleton alphabet, and consider the pair of transductions Ta = {(n, 2n)|n ≥ 1} and Tb = {(n, n ? 3)|n ≥ 4} on the domain of words over Γ seen as unary-coded positive integers. Let us apply the construction from the previous inclusion proof to the bounded-degree rational graph G de?ned by Ta and Tb . Here, <Γ is trivial, and we take a <X b. The graph G and the linearly bounded graph G′ obtained by applying the construction are shown on Fig. 9. Note for instance how vertex 13 in G is represented by vertex (2, a3 b) in G′ because (2, a3 b) is the smallest pair (u, v ) v such that u ?→ 13.

G

In fact, we can prove that the previous inclusion is strict. Theorem 6 There exists a linearly bounded graph of bounded degree which is not a rational graph. Proof We now prove that there exists a linearly bounded graph of bounded degree which is not isomorphic to any bounded degree rational graph. Let us ?rst establish that linearly bounded graphs of bounded degree are not closed under edge reversal. Let L ? {0, 1}+ be a language in NSPACE[2n ] \ NSPACE[n] (cf Thm. 2), we de?ne a linearly bounded graph G with vertices

28

Arnaud Carayol, Antoine Meyer

1

a

2 b

a

4

a

8

a

16 b

a

32 29

b b

13 b 5 a 10 b 7 b

a

26 23

a

20 17

G

b

a

14 11

1, ε

a

2, ε b

a

2, a

a

2, a2

a

2, a3 b

a

2, a4 2, a4 b

b b

2, a3 b b

a

2, a3 ba

2, a3 bab a 5, a2 5, a2 b a 7, a 7, ab

5, ε

a

5, a b 7, ε

G

′

b

b

Fig. 9 Bounded-degree rational graph G and isomorphic lin. bounded graph G′ .

in 0{0, 1}?#? ∪ ? 0{? 0, ? 1}? and edges de?ned by:

x ?→ = {(w, wx) | w ∈ 0{0, 1}?} ∪ {(w, wx ?) | w ∈ ? 0{? 0, ? 1}? }

for x ∈ {0, 1}

?→ = {(w, w#) | w = uv, u ∈ 0{0, 1}?, v ∈ #? and |v | < 2|u| } ∪ {(w, u ?) | w = uv, u ∈ 0{0, 1}?, v ∈ #? , |v | = 2|u| and u ∈ L} The relations ?→, ?→ and ?→ are incremental context-sensitive transduc|w| tions. In fact, as L belongs to NSPACE[2n ], the language {w#2 | w ∈ L} belongs to NSPACE[n]. The construction of GL is illustrated by Figure 10. Suppose that linearly bounded graphs of bounded degree were closed under edge reversal. It would follow that H obtained from G by reversing

0 1

#

#

Linearly Bounded In?nite Graphs

29

0

1 # 0 1 # # # # 1

1

0

0

Fig. 10 The graph G for some L containing 11.

the edges labeled by # is also a linearly bounded graph. As H is linearly bounded, we can assume that ?→, ?→ and ?→ are incremental contextH H H sensitive transductions. Let x be the vertex of H corresponding to ? 0. The set of vertices F = Dom(?→) is a context-sensitive language. It follows from

H 0 1

#

#

Proposition 7 that L(H, {x}, F ) is context-sensitive. As L = L(H, {x}, F ) ∩ {0, 1}?, L would also be context-sensitive which contradicts its de?nition. As rational graphs are closed under edge reversal, it follows from Thm. 5 that rational graphs of bounded degree are strictly contained in linearly bounded graphs of bounded degree. ? ? It may be interesting at this point to recall that there are strong reasons to believe that the languages accepted by ?nite degree synchronized graphs are strictly included in context-sensitive languages (see [3]). Furthermore, all existing proofs that the rational graphs accept the context-sensitive languages break down when the out-degree is bounded. It is not clear whether rational graphs of bounded degree accept all context-sensitive languages. However, as noted in Prop. 10, it is still the case for bounded degree linearly bounded graphs, and in particular for deterministic linearly bounded graphs. 6 Conclusion This paper gives a natural de?nition of a class of canonical graphs associated to the observable computations of labeled linearly bounded machines. It provides equivalent characterizations of this class as the Cayley-type graphs of length-decreasing term-rewriting systems, and as the graphs de?ned by a sub-class of context-sensitive transductions which can increase the length of their input by at most a constant number of letters. Although of a sensibly di?erent nature from rational graphs, we showed that all rational graphs of bounded degree are linearly bounded graphs of bounded degree, and that this inclusion is strict. This leads us to consider a more restricted notion of in?nite automata, closer to classical ?nite automata (as was already observed in [3]), and to propose a hierarchy of classes of in?nite graphs of bounded

30

Arnaud Carayol, Antoine Meyer

Bounded-degree Turing graphs Recursively enumerable languages Bounded-degree linearly bounded graphs Context-sensitive languages Bounded-degree rational graphs ? Bounded-degree regular graphs Context-free languages Finite graphs Rational languages

Fig. 11 A Chomsky-like hierarchy of bounded-degree in?nite graphs.

degree accepting the classes of languages of the Chomsky hierarchy, in the spirit of [8] (see Fig. 11). Finite graphs obviously have a bounded degree, they accept rational languages. The transition graphs of real-time pushdown automata, which accept all context-free languages, are the regular graphs [22], or equivalently the bounded degree HR graphs [10] and bounded degree pre?x-recognizable graphs [7]. By Prop. 10, the languages of deterministic linearly bounded graphs are the context-sensitive languages. Deterministic graphs have by definition a bounded degree, so bounded degree linearly bounded graphs also accept the same class of languages. Finally, since deterministic Turing machines have bounded-degree transition graphs and accept all recursively enumerable languages, we can also restrict the class of Turing graphs to bounded degree. References

1. Arnold, A., Nivat, M.: Comportements de processus. In: Colloque de ? l’Association Francaise pour la Cybern? etique Economique et Th? eorique: Les Math? ematiques de l’Informatique (AFCET ’82), pp. 35–68 (1982) 2. Blumensath, A., Gr¨ adel, E.: Automatic structures. In: Proceedings of the 15th IEEE Symposium on Logic in Computer Science (LICS 2000), pp. 51–62. IEEE (2000) 3. Carayol, A., Meyer, A.: Context-sensitive languages, rational graphs and determinism (2005). Submitted 4. Caucal, D.: On in?nite transition graphs having a decidable monadic theory. In: Proceedings of 23rd International Colloquium on Automata, Languages, and Programming (ICALP 1996), Lecture Notes in Computer Science, vol. 1099, pp. 194–205. Springer Verlag (1996) 5. Caucal, D.: On in?nite transition graphs having a decidable monadic theory. Theoretical Computer Science 290, 79–115 (2003) 6. Caucal, D.: On the transition graphs of Turing machines. Theoretical Computer Science 296, 195–223 (2003)

Linearly Bounded In?nite Graphs

31

7. Caucal, D., Knapik, T.: An internal presentation of regular graphs by pre?xrecognizable graphs. Theoretical Computer Science 34, 299–336 (2001) 8. Caucal, D., Knapik, T.: A Chomsky-like hierarchy of in?nite graphs. In: Proceedings of the 27th International Symposium on Mathematical Foundations of Computer Science (MFCS 2002), Lecture Notes in Computer Science, vol. 2420, pp. 177–187. Springer Verlag (2002) 9. Chomsky, N.: On certain formal properties of grammars. Information and Control 2, 137–167 (1959) 10. Courcelle, B.: The monadic second-order logic of graphs, II: In?nite graphs of bounded width. Mathematical System Theory 21, 187–221 (1989) 11. Elgot, C., Mezei, J.: On relations de?ned by ?nite automata. IBM Journal of Research and Development 9, 47–68 (1965) 12. Frougny, C., Sakarovitch, J.: Synchronized rational relations of ?nite and in?nite words. Theoretical Computer Science 108(1), 45–82 (1993) 13. Hopcroft, J., Ullman, J.: Introduction to Automata Theory, Languages and Computation. Addison-Wesley (1979) 14. Immerman, N.: Nondeterministic space is closed under complementation. SIAM Journal on Computing 17(5), 935–938 (1988) 15. Khoussainov, B., Nerode, A.: Automatic presentations of structures. In: Selected papers of the 1994 International Workshop on Logic and Computational Complexity, Lecture Notes in Computer Science, vol. 960, pp. 367–392. Springer Verlag (1994) ? Synchronized product of linear bounded machines. In: 16. Knapik, T., Payet, E.: Proceedings of the 12th International Symposium on Fundamentals of Computation Theory, (FCT 1999), Lecture Notes in Computer Science, vol. 1684, pp. 362–373. Springer Verlag (1999) 17. Kuroda, S.: Classes of languages and linear-bounded automata. Information and Control 7(2), 207–223 (1964) 18. Latteux, M., Simplot, D., Terlutte, A.: Iterated length-preserving rational transductions. In: Proceedings of the 23rd International Symposium on Mathematical Foundations of Computer Science (MFCS 1998), Lecture Notes in Computer Science, vol. 1450, pp. 286–295. Springer Verlag (1998) 19. Milner, R.: Communication and Concurrency. Prentice Hall International (1989) 20. Morvan, C.: On rational graphs. In: Proceedings of the 3rd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2000), Lecture Notes in Computer Science, vol. 1784, pp. 252–266. Springer Verlag (2000) 21. Morvan, C., Stirling, C.: Rational graphs trace context-sensitive languages. In: Proceedings of the 26th International Symposium on Mathematical Foundations of Computer Science (MFCS 2001), Lecture Notes in Computer Science, vol. 2136, pp. 548–559. Springer Verlag (2001) 22. Muller, D.E., Schupp, P.E.: The theory of ends, pushdown automata, and second-order logic. Theoretical Computer Science 37, 51–75 (1985) ? Thue speci?cations, in?nite graphs and synchronized product. Ph.D. 23. Payet, E.: thesis, Universit? e de la R? eunion (2000) 24. Rispal, C.: The synchronized graphs trace the context-sensitive languages. In: Proceedings of the 4th International Workshop on Veri?cation of In?nite-State Systems (INFINITY 2002), Electronic Notes in Theoretical Computer Science, vol. 68 (2002) 25. Stirling, C.: Decidability of bisimulation equivalence for pushdown processes. Tech. Rep. EDI-INF-RR-0005, School of Informatics, University of Edinburgh (2000) 26. Szelepcsenyi, R.: The method of forced enumeration for nondeterministic automata. Acta Informatica 26, 279–284 (1988) 27. Thomas, W.: A short introduction to in?nite automata. In: Proceedings of the 5th International Conference on Developments in Language Theory (DLT 2001), Lecture Notes in Computer Science, vol. 2295, pp. 130–144. Springer Verlag (2001) 28. Weber, A.: Decomposing a k-valued transducer into k unambiguous ones. Informatique Th? eorique et Applications 30(5), 379–413 (1996)

赞助商链接

更多相关文章：
更多相关标签：