Iterated Pushdown Automata and Sequences of Rational Numbers
by
Se'verine Fratani
Bordeaux 1 University
Coauthors: Ge'raud Se'nizergues

We introduce a link between automata of level k and tree-structures. This method allows us to prove new decidability results about integer sequences. We also reduce some equality problems for sequences of rational numbers to the equivalence problem for deterministic pushdown automata of level k.

Automata and logics The class of pushdown automata of level k (for k >= 1) has been introduced in [Gre70, Mas74] as a generalisation of the automata and grammars of [Aho68, Aho69, Fis68] and has been the object of many further studies: see [Mas76, Dam82, Eng83, ES84, EV86, DG86], and more recently [KNU02].

We show that the structure of the memory of some pushdown automata of level k with pushdown alphabet A, is logically definable inside the k-fold expansion of the finite structure A. This remark enables one to make use of the powerful generalisation of Rabin's tree-theorem ([Rab69]) over arbitrary tree-structures due to A. Muchnik ([Muc92, Sem84, Wal96]). We thus re-obtain the known decidability properties of this class of automata and also obtain some new ones. Namely we show

Theorem 1 The Monadic Second-Order theory of the computation-graph of any pushdown automaton of level k is decidable.

Corollary 2 The membership problem, the emptiness problem and the finiteness problem are decidable for languages recognized by pushdown automata of level k.

Integer sequences We focus here on the class of integer sequences recognised by deterministic pushdown automata of level k : we denote by S_k this class of sequences. These classes enjoy nice closure properties and their union \cup _{k in N} S_k seems quite wide. Level 2 contains the classical rational sequences of integers (see [BR88]).

The closure properties obtained so far by the authors, can be summarized as follows.

Theorem 3 1- For every f, g in S_k+1, k >= 2, the sequences f+g, f ·g (the ordinary product), belong to S_k+1.

2-For every f in S_k+1, g in S_k, k >= 2, f ×g (the convolution product) belongs to S_k+1.
3- For every f in S_k, g in S_l, k, l >= 2, f o g (the composition ) belongs to S_k+l-1.
4- For every system of recurrent equations expressed by polynomials in

S_k+1[X₁, ... , X_p], with initial conditions in S_k+1, k >= 2, every solution belongs to S_k+1.
5- For every f, g in S_k+1, k >= 2, the sequence g^f belongs to S_k+2.

6- For every f in S_k+1, k >= 2, every sequence g fulfilling the recurrent equation g(n+1)=g(n)^f(n) together with some initial condition in S_k+1 belongs to S_k+2.

Application to weak arithmetics A close analysis of the particular pushdown automata of level k associated with sequences f in S_k shows that their computation-graphs have a linear structure. It is then possible to define, inside such a computation graph, the structure < N, S, P> where P is the predicate defined by :

P={\Sigma0 <= i <= nf(i)|  n in N }.

As a corollary of theorem 1, we obtain :

Theorem 4 The Monadic Second-Order theory of the structure < N, S, P> is decidable for every predicate P associated with some sequence f in S_k.

This theorem is an extension of the theorem of Büchi ([Büc60]). The class of predicates P obtained in this way from the classes S_k seems to be incomparable with the class studied in [Car00] (which also yields generalisations of Büchi's theorem).

Sequences of rational numbers Next we consider the class F(S_k) consisting of all the sequences of rational numbers which can be decomposed as (a_n - b_n)/(a'_n - b'_n) for sequences a, b, a', b' in S_k.

This class enjoys nice closure properties too and generalizes some well-known classes of recurrent sequences (or formal power series). The level 3, for example, contains all the so-called P-recurrent sequences of rational numbers, corresponding also to the D-finite formal power series (see [Sta80] for a survey and [PWZ96] for efficient algorithms allowing to transform and compare such series).

Theorem 5 1-For every u, v in F( S_k+1), k >= 2, the sequences u+v, u-v, u ·v (the ordinary product), belong to F( S_k+1). If v does not vanish, then \fracuv belongs to F( S_k+1).
2-For every u in F( S_k+1), v in F( S_k), k >= 2, u ×v (the convolution product) belongs to F( S_k+1).

4- For every system of recurrent equations expressed by polynomials in

F( S_k+1)[X₁, ... , X_p], with initial conditions in F( S_k+1), k >= 2, every solution belongs to F( S_k+1).

Let us define the equality problem for sequences in F( S_k+1) as the following algorithmic problem:

Corollary 6 Let k >= 2. The equality problem for sequences in F( S_k+1) reduces to the equivalence problem for deterministic pushdown automata of level (k+1).

This establishes a new connection between the algorithmic problems about sequences (treated in [PWZ96], for example) and the decision problems about automata (treated in [Sen02] for example).

Detailed version: available on the personal web-pages of both authors: URL:http://dept-info.labri.u-bordeaux.fr/{ ~ fratani, ~ ges}.

Some References

[Aho68]: A.V. Aho.Indexed grammars-an extension of context-free grammars. J. Assoc for Comput. Mach. 15, pages 647-671, 1968.
[Büc60]: J.R. Büchi.On a decision method in resticted second-order arithmetic. In Methodology and Philosophy of Science, stanford Univ. Press, pages 1-11. Int. Congr. for Logic, 1960.
[Mas74]: A.N. Maslov.The hierarchiy of indexed languages of an arbitrary level. Soviet. Math. Dokl. 15, 1974.
[PWZ96]:M. Petkovsek, H.S. Wilf, and D. Zeilberger. A=B. 1996.

Date received: March 15, 2003