arXiv:1001.0143v1 [cs.FL] 31 Dec 2009

ROMANIAN JOURNAL OF INFORMATION
SCIENCE AND TECHNOLOGY
Volume 12, Number 2, 2009, 265279

Undecidability Results for Finite
Interactive Systems
Alexandru Sofroniaa and Alexandru Popab and Gheorghe Stefanescuc,1
a

Faculty of Mathematics and Computer Science, University of Bucharest
E-mail: alexandrusofronia@yahoo.com
b

c

Department of Computer Science, University of Bristol
E-mail: popa@cs.bris.ac.uk

Department of Computer Science, University of Illinois at Urbana-Champaign
E-mail: ghstef@yahoo.com

Abstract. A new approach to the design of massively parallel and interactive
programming languages has been recently proposed using rv-systems (interactive systems with registers and voices) and Agapia programming. In this paper
we present a few theoretical results on FISs (finite interactive systems), the underlying mechanism used for specifying control and interaction in these systems.
First, we give a proof for the undecidability of the emptiness problem for FISs,
by reduction to the Post Correspondence Problem. Next, we use the construction in this proof to get other undecidability results, e.g., for the accessibility of
a transition in a FIS, or for the finiteness of the language recognized by a FIS.
Finally, we present a simple proof of the equivalence between FISs and tile systems, making explicit that they precisely capture recognizable two-dimensional
languages.

1. Introduction
A new approach to the design of massively parallel and interactive programming
languages has been recently proposed. The approach focuses on Agapia [2, 13], a
1 On

leave from the Faculty of Mathematics and Computer Science, University of Bucharest.

2

Sofronia, Popa, Stefanescu

programming language paradigm based on classical register machines and space-time
duality [16, 18]. Agapia extends usual programming languages with coordination features, being a step forward to the integration of coordination features (as in Klaim
[4], Reo [1], Orc [12], etc.) into practical programming languages. A few distinctive features of Agapia are: high-level modularity, including a structured approach
to interaction based on name-free processes; simple operational and relational semantics based on grids and scenarios (enriched two-dimensional words); invariance with
respect to space-time duality.
Agapia language uses (i) complex spatial and temporal data for inerfaces, (ii)
modules over usual programming languages, and (iii) temporal, spatial, or spatiotemporal while-programs for coordination. In Agapia v0.1 one can write programs for
open processes located at various sites and having their temporal windows of adequate
reaction to the environment. It naturally supports process migration, structured
interaction, and deployment of modules on heterogeneous machines. Agapia can be
seen as an extension of usual procedural or functional programming languages (used
in the basic modules), for instance may be developed on top of languages as C, Java,
Scheme, etc.
The theoretical foundation of Agapia is strongly related to the theory of twodimensional languages [6, 7, 10, 11]. It is based on FISs (finite interactive systems) [17,
18], abstract mechanisms for specifying control and interaction in interactive systems.
FISs can be used to recognize two-dimensional languages, and, in this respect, FISs
are equivalent to tile systems [6], existential monadic second order logic [7], or other
equivalent presentations of regular (or recognizable) two-dimensional languages [6, 10].
However, they come equipped with abstract “states” and “interaction classes,” which,
by instantiation, may be used to design interactive programs.
The present paper contains a few results on FISs. First, it presents a proof for the
undecidability of the emptiness problem for FISs by reduction to the Post Correspondence Problem. Next, the construction in this proof is used to show the accessibility
problem for FISs (i.e., whether, for a specific transition, there is an accepting scenario
for a two-dimensional word using that transition) is undecidable. Finally, the paper
includes a simple and direct proof of the equivalence between FISs and tile systems,
emphasizing the conceptual differences between these two equivalent presentations of
recognizable two-dimensional language; as a byproduct, this gives another (this time,
indirect) proof of the undecidability of the emptiness problem for FISs via the undecidability of a similar problem for tile systems. A conference version of the paper has
appeared in [14].

2. Preliminaries

Grids and scenarios A grid (also called a two-dimensional word) is a rectangular
two-dimensional area filled in with letters of a given alphabet. The columns in a
grid correspond to processes, the top-to-bottom order describing their progress in
time. The left-to-right order corresponds to process interaction in a nonblocking

3

Undecidability Results for Finite Interactive Systems

message passing discipline: a process sends a message to the right, then it resumes
its execution.
A scenario is a grid enriched with data around each letter. The data may have
various interpretations: they either represent control/interaction information, or current values of the variables, or both. In this paper, we only use abstract scenarios
of the first type resulting from accepting runs in finite interactive systems. A grid is
presented in Fig. 1(a) and an abstract scenario in Fig. 1(b).

aabbabb
abbcdbb
bbabbca
ccccaaa

(a)

1 1 1
AaBbBbB
2 1 1
AcAaBbB
2 2 1
AcAcAaB
2 2 2

F1 =

1

b

A

a

B

c

2

(b)

(c)

Figure 1: A grid (a), an abstract scenario (b), and a FIS (c).
We use the following notation for operations on grids: · and ⋆ denote vertical composition and iteration, while ⊲ and † denote the horizontal composition and iteration.
Finite interactive systems A finite interactive system (shortly FIS) is a finite
hyper-graph with two types of vertices and one type of (hyper) edges: the first type
of vertices is for states (labeled by numbers), the second is for classes (labeled by
capital letters) and the edges/transitions are labeled by letters denoting the atoms of
the grids; each transition has two incoming arrows (one from a class and the other
from a state), and two outgoing arrows (one to a class and the other to a state). Some
classes/states may be initial (indicated by small incoming arrows) or final (indicated
by double circles); see, e.g., [17, 18].
For the parsing procedure, given a FIS F and a grid w, insert initial states/classes
at the north/west border of w and parse the grid completing the scenario according
to the FIS transitions; if the grid is fully parsed and the south/east border contains
final states/classes only, then the grid w is recognized by F . The language of F is the
set of its recognized grids.
Let F1 be the FIS graphically represented as in Fig. 1(c). It is equivalently represented specifying its transitions

1
A a B
2

A, 1 are initial and B, 2 final. A parsing
1 1 1
Aa b b

1
B b B
1
abb
for cab
cca

,

Ac a b

1 1 1
AaBb b
2
Ac a b

Ac c a

Ac c a

...

,

2
A c A
2

is
1 1 1
AaBbBbB
2 1 1
AcAaBbB
2 2 1
AcAcAaB
2 2 2

and pointing out that

4

Sofronia, Popa, Stefanescu

Post Correspondence Problem Let x = (x1 , . . . , xn ) and y = (y1 , . . . , yn ) be
two lists of nonempty words from an alphabet Σ, with at least two letters. The
Post Correspondence Problem (PCP) is to decide whether or not there exist i1 , . . . , ik
where k ≥ 1 and2 1 ≤ ij ≤ n, ∀j ∈ 1, k such that xi1 . . . xik = yi1 . . . yik . It is known
that PCP is undecidable [15] (if |Σ| ≥ 2).
We use this result to prove the emptiness problem for FISs is undecidabile.

3. The emptiness problem and the finiteness problem for FISs
Let x = (x1 , . . . , xn ) and y = (y1 , . . . , yn ) be an instance of the PCP, labeled
P CP (x, y). We construct a finite interactive system S which accepts a language
L = L(S) such that: L is finite iff it is empty iff P CP (x, y) has no solution. Let |w|
denote the length of the string w ∈ Σ.
The idea of the construction is as follows. The FIS associated to the PCP instance
allows to parse grids where the first two rows contain a proposed solution for the PCP.
More precisely, it contains sequences of xi ’s and yj ’s (with a single letter in a cell)
such that their product is equal. The next rows check if the chosen indices are equal,
hence whether or not one gets a solution for the PCP.
The states and the classes of S are:
States
• s
• a(i, j) ∀i ∈ 1, n ∀j ∈ 1, |xi |
• c(i, j) ∀i ∈ 0, n ∀j ∈ 0, n
Classes
• A
• B(i, j) ∀i ∈ 1, n ∀j ∈ 1, |xi | − 1
• C(i, k) ∀i ∈ 1, n ∀k ∈ 1, |yi | − 1
• M (i, j, k) ∀i ∈ 1, n ∀j ∈ 0, |xi | ∀k ∈ 0, |yi |
S has a unique initial state - s, a unique initial class - A, a unique final state c(0, 0) and n + 1 final classes - A and M (i, 0, 0) for each i ∈ 1, n. To simplify the
definition of the transitions we use an extended notation A = B(i, 0) = B(i, |xi |) =
C(i, 0) = C(i, |yi |) ∀i ∈ 1, n.
|x |
Let xi = x1i · x2i · · · xi i , where xki ’s are the letters of the word xi , 1 ≤ i ≤ n
and use a similar notation for yi ’s. The alphabet of the FIS S also contains a special
symbol $ such that $ 6∈ Σ.
We define the transitions of S as follows:
2 p, q

denotes the set {p, p + 1, . . . , q}

5

Undecidability Results for Finite Interactive Systems

(I)

(II)

B(i, j − 1)

s
xji
a(i, j)

a(j, g)
yik
c(j, i)
xgj = yik , where j ∈ 1, n and g ∈ 1, |xj |
C(i, k − 1)

B(i, j)

∀i ∈ 1, n ∀j ∈ 1, |xi |

C(i, k)

∀i ∈ 1, n

(III)

A

c(0, 0)
$
c(0, 0)

(IV)

A

c(i, i)
$
c(0, 0)

(V)

A

c(i, 0)
$
c(0, 0)

M (i, |xi | − 1, |yi |)

∀i ∈ 1, n

(VI)

A

c(0, i)
$
c(0, 0)

M (i, |xi |, |yi | − 1)

∀i ∈ 1, n

(VII)

M (i, k1 , k2 )

c(j1 , j2 )
$
c(m1 , m2 )

M (i, r1 , r2 )

∀k ∈ 1, |yi | iff

A

M (i, |xi | − 1, |yi | − 1) ∀i ∈ 1, n

where i ∈ 1, n, j1 , j2 , m1 , m2 ∈ 0, n, k1 , r1 ∈ 0, |xi |, k2 , r2 ∈ 0, |yi | and k1 satisfies
exactly one of the following conditions
• k1 = 0, m1 = j1 , r1 = k1 .
• k1 > 0, j1 = i, m1 = 0, r1 = k1 − 1.
• k1 > 0, j1 = 0, m1 = 0, r1 = k1 .
and k2 satisfies exactly one of the following conditions
• k2 = 0, m2 = j2 , r2 = k2 .
• k2 > 0, j2 = i, m2 = 0, r2 = k2 − 1.
• k2 > 0, j2 = 0, m2 = 0, r2 = k2 .
The following lemmas reveal the behavior of this FIS and the role of the transitions.
Recall that the grids below are parsed from left to right and from top to bottom.
Note that equalities of indexes in the following lemmas must be interpreted as
equalities of lists over {1, . . . , n} rather than weaker string equalities. We use a
simplified notation in instead of (i, . . . , i), where i appears n times in a row.

6

Sofronia, Popa, Stefanescu

Lemma 1 Let w be a grid with m lines and q columns. If there exists a successful
running for w with respect to the border conditions3 bn , bw , bs , be , then:
(i) m ≥ 3, q ≥ 1, bn ∈ {s}⋆ , bw ∈ {A}⋆ , bs ∈ {c(0, 0)}⋆ .
(ii) There exist k ≥ 1, r ≥ 1, i1 , . . . , ik and j1 , . . . , jr where 1 ≤ il ≤ n ∀l ∈ 1, k and
1 ≤ jl ≤ n ∀l ∈ 1, r such that xi1 · · · xik and yj1 · · · yjr are the first two lines of
w (as strings) and xi1 · · · xik = yj1 · · · yjr .
(iii) The southern border of the second line of w is c(a1 , b1 ), . . . , c(aq , bq ) where
|xi1 |

(a1 , . . . , aq ) = (i1
{1, . . . , n})

|xik |

, . . . , ik

|yj1 |

) and (b1 , . . . , bq ) = (j1

|yjr |

, . . . jr

) (as lists over

(iv) The first two lines of w are parsed using type (I) and type (II) transitions,
and no other lines can be parsed using type (I) or type (II) transitions. In
particular, all the lines of w, except the first two, are composed of $.
Proof:
(i) Since s is not a final state, it follows that q ≥ 1 and m ≥ 1. The conditions for
the border are trivial from uniqueness of initial and final states and initial classes.
Recall that the only final state of S is c(0, 0). A successful run of w has at least
three transitions from a northern border s to a southern border c(0, 0): a type (I)
transition, followed by a type (II) transition and, as i, j > 0 in type (II) transitions,
a type (IV ) or (V II) transition. Therefore, in order to be accepted, w has to have
at least three lines.
(ii) First, since A is the only initial class and s the only initial state, only type
(I) transitions can be used to parse the first letter of w. Therefore this letter must
be the first letter of some word xi . Note that this argument can be applied whenever
we have A on the western border and s on the northern border.
All the transitions on the first line of w have s as the northern border and therefore
are type (I) transitions. Such transitions contain only letters from the words in the list
x. Note that these transitions can be connected horizontally only if the corresponding
letters are adjacent in some xi (this is the role played by the B(i, j) classes) or are
the final letter of some xi and the first letter of some xk (in which case, the class in
the middle is A = B(i, |xi |) = B(k, 0)).
It follows that the words from the list x that appear in the first line of w cannot be
truncated (except for possibly the rightmost one). Since type (I) transitions cannot
have any M (i, 0, 0) as a eastern border, the eastern border of the first line of w must
be A, the only final class remaining. Therefore, the first line of w is some xi1 · · · xik
where k ≥ 1 (as q ≥ 1).
The northern border of the second line of w is made of a(i, j) states, therefore only
type (II) transitions can be used for parsing. Since C(i, k) classes prevent truncation,
3 I.e.,

using on the borders the specified sequences bn , bw , bs , be of initial/final states/classes

Undecidability Results for Finite Interactive Systems

7

similar to the B(i, j) classes, a similar argument shows that the second line of w is
yj1 · · · yjr for some r ≥ 1, and it is parsed using only type (II) transitions.
A type (I) transition accepting a letter xki has on the southern border the state
a(i, k). The first index encodes the position of the word xi in the list x and the second
index encodes the position k in which the letter xki appears in xi . The condition
xgj = yik in the definition of type (II) transitions forces the letters in the first and
second line to be identical. Therefore, xi1 · · · xik = yj1 · · · yjr .
(iii) From (ii) it follows that the southern border of the first line has the following
format a(i1 , 1)a(i1 , 2) . . . a(i1 , |xi1 |) . . . a(ik , 1) . . . a(ik , |xik |). As type (II) transitions
copy the first index of the northern border a(j, g) to the first index of the southern
border c(j, i), the southern border of line 2 (or northern border of line 3) can be
written c(a1 , b1 ), . . . , c(aq , bq ), and, by extracting the first indexes, (a1 , . . . , aq ) =
|x

|

|xi |

(i1 i1 , . . . , ik k ). The second index of the state c(j, i) in a type (II) transition is
equal to the position of the word yi in the list y, so from (ii) we get (b1 , . . . , bq ) =
|yj1 |

(j1

|yjr |

, . . . , jr

).

(iv) Recall that the first line of w is parsed using only type (I) transitions and
the second line using only type (II) transitions. To conclude the proof, note that
the northern border of line 3 is made of c(∗, ∗) states, type (III) − (V II) transitions
also produce c(∗, ∗) states on the southern border and type (I) and (II) transitions
cannot be used for any c(∗, ∗) on the northern border.
In particular, since only type (III) − (V II) transitions can be used, all the lines
of w except the first two, are composed of $.
✷
In order to obtain a successful “encoding” in w of a solution for P CP (x, y) we
must prove that k = r and indexes il = jl ∀l ∈ 1, k.
Using type (III) − (V II) transitions, a p + 2 line marks the letters of a corresponding pair of tiles (xip , yip ) in the PCP solution. Final states and a final class are
obtained only after successful reduction of these tiles. Additional $ lines parsed with
type (III) transitions can be added to such final positions. This behavior is captured
by the following lemma.
Lemma 2 Let w be a grid with m lines and q columns parsed by S and let us use
the notation xi1 , . . . xik , yj1 , . . . yjr as in Lemma 1. Then:
(i) For all p with 0 ≤ p ≤ k, the southern border of the p + 2 line of w can be
written c(ap,1 , bp,1 ), . . . , c(ap,q , bp,q ) and satisfies the following equalities (as lists
over {0, 1, . . . , n}):
|xi

|

|xik |

(ap,1 , . . . , ap,q ) = (0α , ip+1p+1 , . . . , ik
(bp,1 , . . . , bp,q ) = (0
where α =

β

Pp

)

|yj
|
|y |
, jp+1p+1 , . . . , jr jr )

z=1

|xiz | and β =

Pp

z=1

Furthermore, k = r and ip = jp ∀p ∈ 1, k.

|yjz |.

8

Sofronia, Popa, Stefanescu

(ii) Any line of w after the k + 2 line, if any, is parsed using type (III) transitions
only.
(iii) The eastern border be is of the following type be ∈ A·A·M (i1 , 0, 0) · · · M (ik , 0, 0)·
{A}⋆
Proof:
(i) Recall from the previous lemma that the two equalities of lists hold for p = 0.
We will prove the equalities by induction over p.
We refer to the index sequences (ap,1 , . . . , ap,q ) and (bp,1 , . . . , bp,q ), as the first
stream and the second stream of specifying the southern border of the p + 2 line of w
(or the northern border of the p + 3 line, if such a line exists).
First, some remarks on type (V II) transitions. These transitions can be composed horizontally only with transitions of the same type. These transitions are only
defined if the first index of the classes M on the western and eastern border are equal.
Therefore, whenever a class M (i, k1 , k2 ) appears on a line, only M (i, , ) classes can
appear when parsing the rest of the line. Furthermore, whenever k1 = 0, the second
index in M (i, , ) classes remains 0 until the end of the line and the rest of the first
northern stream is copied to the first southern stream. Similarly, whenever k2 = 0
the third index in M (i, , ) classes remains 0 until the end of the line and the rest of
the second northern stream is copied to the second southern stream.
Let p = 1. From the previous lemma, the northern border of the first letter in
the third line is c(i1 , j1 ) with i1 , j1 ≥ 1 and the western border is A. Then i1 = j1
since only a type (IV ) transition can be used to parse this letter and the transitions
used to parse the rest of line 3 are only type (V II) transitions, with M (i1 , , ) on the
western and eastern borders. The processing of the following letters on the third line
is deterministic, since depending on the northern and western border, at most one
type (V II) transition can be chosen at each step.
Let α = |xi1 | ≥ 1 and β = |yi1 | ≥ 1 (recall that both lists in PCP have nonempty
words). The first letter of this line is processed using the following type (IV ) transition:
c(i1 , i1 )
A
$
M (i1 , α − 1, β − 1)
c(0, 0)
For the sake of simplicity, assume α < β. Then the following α − 1 letters in this
line are parsed using type (V II) transitions, each creating a southern border of c(0, 0)
and decreasing the second and third indexes in M (i, , ) by 1 until k1 reaches 0 using
M (i1 , k1 , k2 )

c(i1 , i1 )
$
c(0, 0)

M (i1 , k1 − 1, k2 − 1) .

The first and second southern streams have α leading zeros and k1 = 0 is carried over
when parsing the rest of the line. The first equality is thus proven since the rest of
the first northern stream is copied to the first southern stream.

Undecidability Results for Finite Interactive Systems

9

After parsing α i1 ’s from the first northern stream there are still at least β − α =
|yi1 | − |xi1 | i1 ’s on the second northern stream. For the next β − α letters only type
(V II) transitions can be used:
c(j, i1 )
$
c(j, 0)

M (i1 , 0, k2 )

M (i1 , 0, k2 − 1)

therefore the second southern stream has a total of β leading zeros. After that,
k2 reaches zero and the rest of the second northern stream is copied to the second
southern stream. Thus we have obtained the second required equality and M (i1 , 0, 0)
on the easternmost border of line 3. A symmetrical argument holds when α ≥ β.
Note that if k > p ≥ 1 or r > p ≥ 1, then the southern border of this line still
contains non-final states - c(ik , jr ) so w has at least another line, which motivates the
use of induction.
Let p ∈ 2, k. Let
p−1
p−1
X
X
|yjz |.
|xiz | and β =
α=
z=1

z=1

We distinguish only two non-similar cases: α = β or α < β, due to the symmetry in
type (V II) transitions.
If α = β, then by the induction hypothesis, both northern streams of line p + 2
have exactly α leading zeros followed by q − α nonzero numbers. This allows us to
use α type (III) transitions to parse the first α letters on this line. The next letter
has the northern border c(ip , jp ) which forces a type (IV ) transition and therefore
ip = jp . The two equalities are proved similarly with the case p = 1 above. Note that
this case can be avoided entirely if we consider only atom solutions of P CP (x, y) (i.e.
no non-trivial prefix of the solution forms a valid solution).
If α < β, then after the first α leading zeros, the first northern stream contains
only nonzero numbers, while the second one has another β − α leading zeros followed
by q − β nonzero numbers. Then after α type (III) transitions, the α + 1 atom has
c(ip , 0) on the northern border and A on the western border. The type (V ) transition
used to parse the first letter is:
A

c(ip , 0)
$
c(0, 0)

M (ip , ϕ − 1, ψ) .

where ϕ = |xip | and ψ = |yip |.
The rest of the first northern stream contains at least ϕ−1 ip ’s that require parsing
by type (V II) transitions with k1 > 0. Thus, the corresponding first southern stream
will contain an equal number of zeros in that part of the stream. After that, only type
(V II) transitions with k1 = 0 can be used which copy the rest of the first northern
stream to the first southern stream.
The rest of the second northern stream has another β − α − 1 leading zeros which
force type (V II) transitions with k2 > 0, j2 = 0, that copy the zeros to the second

10

Sofronia, Popa, Stefanescu

southern stream. Afterwards, the second northern stream reaches the ψ jp ’s created
in line 2 by the word yjp and carried over to this line.
Since the case k2 > 0, jp > 0 jp 6= ip is undefined for type (V II) transitions, the
only remaining possibility is that jp = ip . Thus the next ψ numbers from the second
northern stream are replaced by zeros in the second southern stream, decreasing k2
until it becomes 0. Afterwards the rest of the second stream is copied from north to
south, yielding the eastern border M (ip , 0, 0).
This proves the required equalities. Moreover, w must have an additional line and
the process continues if p < min(k, r) because k > p or r > p imply that the southern
border of the current line contains the non-final state c(ik , jr ).
Assume k < r, then the southern border of line k + 2 has a first stream containing
only zeros, and a second one with β leading zeros followed by 0 < q − β nonzero numbers. In this case, the southern border contains the non-final state c(0, jr ), therefore
w must have at least another line. However, in this case, it is impossible to obtain a
final class on the additional line. Indeed, the first β pairs of zeros are deterministically
parsed by type (III) transitions. The following β + 1 letter, with c(0, jk+1 ) on the
northern border and A on the eastern border, can only be parsed by a type (V I)
transition with M (jk+1 , |xjk+1 |, |yjk+1 | − 1) on the eastern border.
However, since the rest of the first northern border contains only zeros, the rest
of the line can be parsed only using type (V II) transitions with k1 = |xjk+1 | > 0 and
j1 = 0. Therefore r1 = k1 > 0 and the eastern border of this line is M (jk+1 , |xjk+1 |, 0)
which is not a final class! A similar argument for k > r proves that k = r.
(ii & iii) If m ≥ k + 3, the northern border of the k + 3 - th line of w has both
streams full of 0’s. Therefore, only type (III) transitions are used to parse this line,
copying the northern border to the next line and resulting in an eastern border of A.
Similarly, any line of w after the k + 2 line has only type (III) transitions yielding
A on the eastern border. From Lemma 1 the first two lines have A on the eastern
border. From (i) the eastern border of the next k lines is M (i1 , 0, 0) . . . M (ik , 0, 0)
which concludes the proof.
✷
Using these two lemmas, one can prove the following result:
Theorem 3 The finiteness and the emptiness problems for finite interactive systems
are undecidable.
Proof: Assume that the emptiness problem is decidable. Then for each PCP instance, P CP (x, y), we can use the above construction in order to obtain the FIS
S = S(x, y). For this FIS, we can decide whether or not L(S) is empty. The previous
lemmas show that for every w ∈ L(S), the first two lines of w determine a solution for
P CP (x, y) and that from any solution of P CP (x, y), a grid w constructed from the
strings of the solution and composed vertically with enough $’s (k lines where k is the
length of the solution), can be parsed according to the lemmas (therefore w ∈ L(S)).
Therefore the assumption contradicts the fact that PCP is undecidable.
For the undecidability of the finiteness problem, it suffices to observe that if L(S)

Undecidability Results for Finite Interactive Systems

11

is not empty, then it is infinite. That follows from the fact that if w ∈ L(S) then
w · $† ∈ L(S) (parsing the additional lines with type (III) transitions). Also, the
iteration (any number of times) of a solution for P CP (x, y) gives another P CP (x, y)
solution for which a w′ ∈ L(S) can be constructed by horizontal iteration of w. Therefore L(S) is empty iff it is finite which concludes the proof.
✷

4. The accessibility of a given FIS transition
For any instance of PCP, we construct a FIS S1 which has all the states, classes,
and transitions of the FIS S in the previous section, an additional state q, and two
additional classes Q,T . The initial states and classes of S1 are those of S, the only
final state is q and the only final class is T . In addition to S, S1 has the following
new transitions:
(i)

A

s
$
s

T

(ii)

M (i, 0, 0)

s
$
s

T

(iii)

A

c(0, 0)
$
q

Q

(iv)

Q

c(0, 0)
$
q

Q

(v)

Q

s
$
q

T

∀i ∈ 1, n

This construction may be used to get the following result:
Theorem 4 The accessibility of a transition in a FIS is undecidable.
Proof: It suffices to prove that transition of type (v) is accessible iff P CP (x, y) has
a solution.
If P CP (x, y) has a solution then there is a w with m lines and q columns accepted
by the FIS in the previous section. Because of the border conditions established by
Lemma 1 and 2, we can add one column to the right of w and an additional line,
obtaining u ∈ L(S1). Indeed if we take a successful running of w in the previous FIS,
and parse the last line of u using q type (iii) and (iv) transitions, the last column with

12

Sofronia, Popa, Stefanescu

type (i) and (ii) transitions, and finally a type (v) transition for the southeasternmost
letter of u, we obtain a successful running of u on S1, which uses the transition (v).
If transition (v) is accessible, let u be a grid that can be parsed such that transition
(v) can be applied to the southeasternmost letter. We shall prove that there exists w
such that u = (w ⊲ $⋆ ) · $† and w is recognized by the FIS S in the previous section.
Firstly, the letter parsed with this type (v) transition cannot be on the first column
since Q is not an initial class. The only way of obtaining class Q on the western border
on this line is by using a type (iii) transition and some (if any) type (iv) transitions.
This implies that c(0, 0) is on the northern border of all the atoms in the last line of
u and since c(0, 0) is not an initial state, u has at least 2 lines. Similarly, the state s
cannot appear on the northern border of the last atom, unless only type (i) and some
(if any) type (ii) transitions were used for processing the atoms on the last column
of u. Then there exists w such that u = (w ⊲ $⋆ ) · $† . The southern border of w
is composed only of c(0, 0)’s and the eastern border of A’s and M (i, 0, 0)’s for some
i ∈ 1, n.
Since type (i)-(v) transitions cannot lead to A’s or M (i, 0, 0)’s on the eastern border, it follows that w was parsed using transitions of the FIS in the previous section.
Furthermore, due to the southern and eastern border conditions for w, this parsing is
a successful running of w in the FIS in the previous section and therefore P CP (x, y)
has a solution.
✷

5. The equivalence of FISs and tile systems
In this section we present a simple, direct proof of the equivalence between FISs
and tile systems. Tile systems [6, 10] are but one of many equivalent mechanisms
specifying the class of recognizable two-dimensional languages.
Tile systems For a grid w of size m×n, let w
b denote the grid of size (m+2)×(n+2)
obtained bordering w with a special symbol ♯. A tile system is defined as follows:
• for a bordered grid w,
b let Br,s (w)
b be the set of its sub-grids of size r × s;
• a two-dimensional language L over V is local if there is a set ∆ of 2 × 2 grids
over V ∪ {♯} such that
L = {w | w grid over V ∧ B2,2 (w)
b ⊆ ∆}
• a two-dimensional language L over an alphabet V is recognized by a tile system
if there is an alphabet V ′ , a local language L′ over V ′ and a letter-to-letter
homomorphism h : V ′ → V such that h(L′ ) = L.
From FISs to tile systems Let L be a grid language over an alphabet V recognized
by a FIS F . Let V1 denote the extended alphabet consisting of tuples (N, W, a, E, S)

13

Undecidability Results for Finite Interactive Systems

(N/W/E/S stands for north/west/east/south, respectively), with W, E classes in F ,
with N, S states in F , with a in V , and such that

W

N
a E
S

is a transition in F .

Consider the local language L1 over V1 generated by the following set of 2 × 2 tiles
over V1 ∪ {♯}:
• (tiles with letters in V1 which agree on the connecting cells)
w1 w2
, with wk = (Nk , Wk , ak , Ek , Sk ), k ∈ 1, 4 and such that E1 = W2 , S1 =
w3 w4
N3 , S2 = N4 , E3 = W4 .
• (tiles with ♯ for handling the borders) - these are tiles with ♯ and such that the
next elements in V1 have appropriate initial/final states/classes;
♯♯
– for instance, the north-east corner tile is
with N4 , W4 initial;
♯w4
♯ ♯
– the middle-north border tile is
with N3 , N4 initial;
w3 w4
– and so on.
One can easily see that the grids in L1 correspond to the scenarios in F . By
dropping the information around the transition symbols with the homomorphism h :
(N, W, a, E, S) 7→ a one gets a tile systems specifying L. This proves one implication,
namely:
Lemma 5 A language recognized by a FIS can be specified with a tile system.
From tile systems to FISs It is obvious that FIS languages are closed to letterto-letter homomorphism, so we can restrict ourself to local languages.
For a local language L over an alphabet V and specified by a set ∆ of tiles, we
construct an equivalent FIS F as follows:
• the set of states is the same as the set of classes and consists of 2 × 2 tiles over
V ∪ {♯} from ∆;
N1 N2
N3 N4

• the transitions are

W1 W2
W3 W4

a

E1 E2
E3 E4

S1 S2
S3 S4

–
–
–
–

(N1 , N2 , N3 , N4 ) = (W1 , W2 , W3 , W4 ),
N4 = W4 = a,
(N3 , N4 ) = (S1 , S2 ), and
(W2 , W4 ) = (E1 , E3 );

♯ ♯
∈ ∆;
N3 N4
♯ W2
initial classes are tiles
∈ ∆;
♯ W4

• initial states are tiles

with:

14

Sofronia, Popa, Stefanescu
N1 N2
∈ ∆;
♯ ♯
W2 ♯
final classes are tiles
∈ ∆;
W4 ♯

• final states are tiles

A grid w is in L if and only if it is recognized by F . In this way, the following
reverse implication result is proved:
Lemma 6 A language specified by a tile system can be recognized with a FIS.
The two lemmas above prove the main result of this section.
Theorem 7 A language is recognized by a FIS if and only if it can be specified with
a tile system.
Theorem 7 and a result in [11], stating that by extracting the first line from the
grids specified by tile systems one gets precisely the context-sensitive string languages,
yield an alternative, indirect proof of the undecidability of the emptiness problem for
FISs.

6. Conclusions and future work
We have proved that a few simple and easily decidable properties on finite automata (like accessibility of a transition, finiteness, etc.) become undecidable when
extended to finite interactive systems. It may be worthwhile to find interesting restricted classes of FIS languages for which these properties are decidable.
One can also look at possible extensions of the technique in this paper for covering different sets of restricted grids such as: non-rectangular grids, connected grids,
bounded grids, etc. For these classes, one may use the bounded Post Correspondence
Problem (which bounds the number of pairs used in a PCP solution to no more than
k, including repeated tiles) which is also known to be NP-complete [9].
Other open area is to develop an algebraic theory for representing FIS languages,
similar to the regular algebra used for regular languages and finite automata.

Acknowledgment
This research was partially supported by the GlobalComp Grant (PNCDI-II,
Project 11052/18.09.2007, Romania).

References
[1] ARBAB, F.: Reo: a channel-based coordination model for component composition, Mathematical Structures in Computer Science 14(3), 2004, pp. 329-366.

Undecidability Results for Finite Interactive Systems

15

[2] DRAGOI, C., STEFANESCU, G.: Agapia v0.1: A programming language for
interactive systems and its typing systems. In: Proc. FINCO/ETAPS 2007,
ENTCS, 203(3)(2008): pp. 69-94.
[3] DRAGOI, C., STEFANESCU, G.: On compiling structured interactive programs
with registers and voices. In: Proc. SOFSEM 2008. LNCS 4910, Springer, 2008:
pp. 259-270
[4] DE NICOLA, R., FERRARI, G., PUGLIESE, R.: Klaim: a Kernel Language
for Agents Interaction and Mobility. IEEE Transactions on Software Engineering,
24(5): pp. 315-330, IEEE Computer Society, 1998.
[5] GADDUCCI, F., MONTANARI, U.: The tile model. In: Proof, language, and
interaction: Essays in honor of Robin Milner,pp. 133-168. MIT Press, 1999.
[6] GIAMMARRESI, D., RESTIVO, A.: Two-dimensional languages. In: Handbook
of formal languages. Vol. 3: Beyond words (Rozenberg, G., Salomaa, A., eds.),
pp. 215-265. Springer, 1997.
[7] GIAMMARRESI, D., RESTIVO, A., SEIBERT, S., THOMAS, W.: Monadic
second order logic over rectangular pictures and recognizability by tiling systems.
Information and Computation, 125(1996): pp. 32-45.
[8] GOLDIN, D., SMOLKA, S., WEGNER, P.(Eds.): Interactive computation: The
new paradigm. Springer, 2006.
[9] GAREY, M.R. and JOHNSON, D.S.: Computers and Intractability: A Guide to
the Theory of NP-Completeness. W. H. Freeman, 1979.
[10] LINDGREN, K., MOORE, C., NORDAHL, M.: Complexity of two-dimensional
patterns. Journal of Statistical Physics, 91(1998): pp. 909-951.
[11] LATTEUX, M., SIMPLOT, D.: Context-sensitive string languages and recognizable picture languages. Information and Computation, 138(1997): pp. 160-169.
[12] MISRA, J., COOK, W.R. : Computation Orchestration. Software and System
Modeling 6(1)(2007): pp. 83-110
[13] POPA, A., SOFRONIA, A., STEFANESCU, G.: High-level structured interactive programs with registers and voices. Journal of Universal Computer Science,
13(11)(2007): pp. 1498-1500.
[14] SOFRONIA, A., POPA, A., STEFANESCU, G.: Undecidability Results for Finite Interactive Systems, Proc. 10th International Symposium on Symbolic and
Numeric Algorithms for Scientific Computing - SYNASC 2008, IEEE, 2008, pp.
xxx-xxx.
[15] POST, E.L.: Recursive unsolvability of a problem of Thue. Journal of Symbolic
Logic, 12(1947): pp. 1-11.

16

Sofronia, Popa, Stefanescu

[16] STEFANESCU, G.: Network algebra. Springer, 2000.
[17] STEFANESCU, G.: Algebra of networks: modeling simple networks as well as
complex interactive systems. In: Proof and System-Reliability, Proc. Marktoberdorf Summer School 2001, pp. 49-78. Kluwer, 2002.
[18] STEFANESCU, G.: Interactive systems with registers and voices. Fundamenta
Informaticae 73(2006), pp. 285-306.

