MFCS'98:Abstracts of Accepted Papers

Gaussian elimination and a characterization of algebraic power series
by Werner Kuich

We show first how systems of equations can be solved by Gaussian elimination. This yields a characterization of algebraic power series and of Alg(A'), A \subseteq A', A a continuous semiring. In the case of context-free languages this characterization coincides with the characterization given by Gruska [3].

Flow Logic for Imperative Objects
by Flemming Nielson, Hanne Riis Nielson

We develop a control flow analysis for the Imperative Object Calculus. We prove the correctness with respect to two Structural Operational Semantics that differ in *minor* technical ways, and we show that the proofs differ in *major* ways as regards the use of proof techniques like coinduction and Kripke-logical relations.

Locally explicit construction of Rodl's asymptotically good packings
by Nikolai N. Kuzjurin

We present a family of asymptotically good packings of l-subsets of an n-set by k-subsets and an algorithm that given a natural i finds the i-th k-subset of this family. The bit complexity of this algorithm is almost linear in encoding length of i that is close to best possible complexity. A parallel NC-algorithm for this problem is presented as well.

Combinatorial Hardness Proofs for Polynomial Evaluation
by Mikel ALDAZ, Joos HEINTZ, Guillermo MATERA, Jose L. MONTANA, Luis M. PARDO

We exhibit a new method for showing lower bounds for the time complexity of polynomial evaluation procedures given by straight-line programs. Time, denoted by L, is measured in terms of nonscalar arithmetic operations. The time complexity function considered here is L^2. In contrast with known methods for proving lower complexity bounds, our method is purely combinatorial and does not require powerful tools from algebraic or diophantine geometry.
By means of our method we are able to verify the computational hardness of new natural families of univariate polynomials for which this was impossible up to now. By computational hardness we mean that the complexity function L^2 increases linearly in the degree of the polynomials of the family we are considering.
Our method can also be applied to classical questions of transcendence proofs in number theory and geometry. A list of (old and new) formal power series is given whose transcendency can be shown easily by our method.

On One-pass Term Rewriting
by Zoltan Fulop, Eija Jurvanen, Magnus Steinby, Sandor Vagvolgyi

Two restricted ways to apply a term rewriting system (TRS) to a tree are considered. When the one-pass root-started strategy is followed, rewriting starts from the root and continues stepwise towards the leaves without ever rewriting a part of the current tree produced in a previous rewrite step. One-pass leaf-started rewriting is defined similarly, but rewriting begins from the leaves. In the sentential form inclusion problem one asks whether all trees which can be obtained with a given TRS from the trees of some regular tree language T belong to another given regular tree language U, and in the normal form inclusion problem the same question is asked about the normal forms of T. We show that for a left-linear TRS these problems can be decided for both of our one-pass strategies. In all four cases the decision algorithm involves the construction of a suitable tree recognizer.

On some recognizable picture-languages
by Klaus Reinhardt

We show that the language of pictures over \{a,b\}, where all occurring b's are connected is recognizable, which solves an open problem in [Mat98]. We generalize the used construction to show that monocausal deterministically recognizable picture languages are recognizable, which is surprisingly nontrivial. Furthermore we show that the language of pictures over \{a,b\}, where the number of a's is equal to the number of b's is nonuniformly recognizable.

Blockwise Variable Orderings for Shared BDDs
by Harry Preuss, Anand Srivastav

A state-of-the-art data structure for the representation of Boolean functions are ordered binary decision diagrams (OBDDs). The size of an OBDD representing a Boolean function depends on the variable ordering. Finding a variable ordering with optimal (i.e. minimum) OBDD size is a central, but NP-hard problem. Thus it is of great interest to characterize optimal variable orderings from the structure of the given function. In this paper we investigate the problem of characterizing optimal variable orderings for shared OBDDs of two Boolean functions f_i = g_i \otimes_i h_i, \ i=1,2, where \otimes_i is an operator from the Base B^*_2 and g_i (resp.\ h_i) depends only on x-variables (resp. \y-variables). Tree-like circuits provide an example for such functions. In the special case f_1=\overline{f_2}, Sauerhoff, Wegener and Werchner [Sauerhoff] proved that there is some optimal ordering where all x-variables are tested before all y-variables or vice versa (blockwise variable ordering). We show that this is also true for arbitrary f_1,f_2 provided that \otimes_1 = \wedge and \otimes_2=\vee, and for shared OBDDs with complemented edges and arbitrary f_1,f_2 provided that \otimes_1 = \wedge and \otimes_2=\oplus. For all other combinations of \otimes_1 und \otimes_2 we give counterexamples.

Topological Definitions of Chaos applied to Cellular Automata Dynamics
by G. Cattane, L. Margara

We apply the two different definitions of chaos given by Devaney and by Knudsen for general discrete time dynamical systems (DTDS) to the case of 1-dimensional cellular automata. A DTDS is chaotic according to the Devaney's definition of chaos iff it is topologically transitive, has dense periodic orbits, and it is sensitive to initial conditions. A DTDS is chaotic according to the Knudsen's definition of chaos iff it has a dense orbit and it is sensitive to initial conditions. We continue the work initiated in~[ciac97], [stacs97], [CM97a], and~[TCS] by proving that an easy-to-check property of local rules on which cellular automata are defined--introduced by Hedlund in~[hed] and called {\em permutivity}--is a sufficient condition for chaotic behavior. Permutivity turns out to be also a necessary condition for chaos in the case of elementary cellular automata while this is not true for general 1-dimensional cellular automata. The main technical contribution of this paper is the proof that permutivity of the local rule either in the leftmost or in the rightmost variable forces the cellular automaton to have dense periodic orbits.

Shuffle on trajectories: a simplified approach to the Schutzenberger product and related operations
by Tero Harju, Alexandru Mateescu, Arto Salomaa

We investigate the problem of finding monoids that recognize languages of the form L_1\shu_TL_2, where T is an arbitrary set of trajectories. Thereby, we describe two such methods: one based on the so called trajectories monoids and the other based on monoids of matrices. Many well-known operations such as catenation, bi-catenation, shuffle, literal shuffle and insertion are just particular instances of the operation \shu_T. Hence, our results offer a uniform treatment for classical methods, notably the Sch\" utzenberger product. We investigate some other related operations, too.

Equations in transfinite strings
by Christian Choffrut, Sandor Horvath

We address the question of extending the theory of equations in finite strings to transfinite strings. We give a full description of the solutions of the equations in two unk nowns as well as the equations of the form x^my^p=z^q for m,p,q\geq 2. By so doing we introdu ce some new notions that we believe are interesting for their own sake.

A Finite Hierarchy of the Recursively Enumerable Real Numbers
by Klaus Weihrauch, Xizhong Zheng

In this paper we discuss the relationships between weak computabilities of a real number x and effective enumerabilities of corresponding set A which enumerates 1-position in the binary expresion of x. We call a real number x semi-computable if it is a limit a computable monotonic sequence of rational numbers, x is called weakly computable if it is a sum of two semi-computable real numbers and x is recursively enumerable if it is a limit of a computable sequence of rational numbers. We show that, there are d-r.e, k-r.e. and even \omega-r.e. sets which correspond to the semi-computable real numbers. On the other hand, there is also d-r.e set A which corresponds to a non-semi-computable but weakly computable real number. For the weakly computability of real numbers we give another characterization that x is weakly computable iff there is a computable sequence of rational numbers which converges to x weakly effectively. At last we show that there is an \omega-r.e set A which corresponds to a recursively enumerable but not weakly computable real number. Therefore, the classes of computable real numbers, semi-computable real numbers, weakly computable real numbers and r.e. real numbers form a noncollapsed hierarchy.

Minimal forbidden words and factor automata
by M. Crochemore, F. Mignosi, A. Restivo

Let L(M) be the (factorial) language avoiding a given anti-factorial language M. We design an automaton accepting L(M) and built from the language M. The construction is effective if M is finite.
If M is the set of minimal forbidden words of a single word v, the automaton turns out to be the factor automaton of v (the minimal automaton accepting the set of factors of v).
We also give an algorithm that builds the trie of M from the factor automaton of a single word. It yields a non-trivial upper bound on the number of minimal forbidden words of a word.
{\bf Keywords}: factorial language, anti-factorial language, factor code, factor automaton, forbidden word, avoiding a word, failure function.

Communication complexity and Lower Bounds on Multilective Computations
by Juraj Hromkovic

Communication complexity of two-party (multiparty) protocols has established itself as a successful method for proving lower bounds on the complexity of concrete problems for numerous computing models. While the relations between communication complexity and oblivious (semilective) computations are ususally transparent and the main difficulty is reduced to proving nontrivial lower bounds on the communication complexity of given computing problems, the situation essentially changes, if one considers non-oblivious or multilective computations. The known lower bound proofs for such computations are far from beeing transparent and the crucial ideas of these proofs are often hidden behind some nontrivial combinatorial analysis. The aim of this paper is to create a general framework for the use of two-party communication protocols for lower bound proofs on multilective computations. The result of this creation is not only a transparent presentation of some known lower bounds on multilective computation, but also the derivation of new nontrivial lower bounds on multilective VLSI circuits and branching programs. Another advantage of this framework is that it provides lower bounds for a lot of concrete functions. This contrasts to the typical papers devoted to lower bound proofs, where one establishes a lower bound for one or a few specific functions.

On the Word, Subsumption, and Complement Problem for Recurrent Term Schematizations
by Miki Hermann, Gernot Salzer

We investigate the word and the subsumption problem for recurrent term schematizations, which are a special type of constraints based on iteration. By means of unification, we reduce these problems to a fragment of Presburger arithmetic. Our approach is applicable to all recurrent term schematizations having a finitary unification algorithm. Furthermore, we study a particular form of the complement problem. Given a finite set of terms, we ask whether its complement can be finitely represented by schematizations, using only the equality predicate without negation. The answer is negative as there are ground terms too complex to be represented by schematizations with limited resources.

Characterization of Sensitive Linear Cellular Automata with Respect to the Counting Distance
by giovanni manzini

In this paper we give sufficient and necessary conditions for a linear 1-dimensional cellular automata F to be sensitive with respect to the counting distance defined in [Cattaneo et al, MFCS'97]. We prove an easy-to-check characterization in terms of the coefficients of the local rule, and an alternative characterization based on the properties of the iterated map F^n.

Average-Case Intractability vs. Worst-Case Intractability
by Johannes Koebler, Rainer Schuler

We use the assumption that all sets in NP (or other levels of the polynomial-time hierarchy) have efficient average-case algorithms to derive collapse consequences for MA, AM, and various subclasses of P/poly. As a further consequence we show for C=P(PP) and C=PSPACE that C is not tractable in the average-case unless C=P.

One Quantifier Will Do in Existential Monadic Second-Order Logic over Pictures
by Oliver Matz

We show that every formula of the existential fragment of monadic second-order logic over picture models (i.e., finite, two-dimensional, coloured grids) is equivalent to one with only one existential monadic quantifier.
The corresponding claim is true for the class of word models (see Thomas '82) but not for the class of graphs (see Otto '95).
The class of picture models is of particular interest because it has been used to show the strictness of the different (and more popular) hierarchy of quantifier alternation.

A Second Step Towards Circuit Complexity-Theoretic Analogs of Rice's Theorem
by Lane A. Hemaspaandra, Joerg Rothe

Rice's Theorem states that every nontrivial language property of the recursively enumerable sets is undecidable. Borchert and Stephan initiated the search for circuit complexity-theoretic analogs of Rice's Theorem. In particular, they proved that every nontrivial counting property of circuits is UP-hard, and that a number of closely related problems are SPP-hard. The present paper studies whether their UP-hardness result itself can be improved to SPP-hardness. We show that their UP-hardness result cannot be strengthened to SPP-hardness unless unlikely complexity class containments hold. Nonetheless, we prove that every P-constructibly bi-infinite counting property of circuits is SPP-hard. We also raise their general lower bound from unambiguous nondeterminism to constant-ambiguity nondeterminism.

On repetition-free binary words of minimal density
by Roman Kolpakov, Gregory Kucherov, Yuri Tarannikov

In [KolpakovKucherovMFCS97], a notion of minimal proportion (density) of one letter in n-th power-free binary words has been introduced and some of its properties have been proved. In this paper, we proceed with this study and substantially extend some of these results. First, we introduce and analyse a general notion of minimal letter density for any infinite set of words which don't contain a specified set of ``prohibited'' subwords. % is closed under subwords. We then prove that for n-th power-free binary words, the density function is \frac{1}{n}+\frac{1}{n^3}+\frac{1}{n^4}+{\cal O}(\frac{1}{n^5}) refining the estimate from [KolpakovKucherovMFCS97]. Following [KolpakovKucherovMFCS97], we also consider a natural generalization of n-th power-free words to x-th power-free words for real argument x. We prove that the minimal proportion of one letter in x-th power-free binary words, considered as a function of x, is discontinuous at all integer points n\geq 3. Finally, we give an estimate of the size of the jumps.

Encoding the Hydra Battle as a rewrite system
by H. Touzet

In rewriting theory, termination of a rewrite system by Kruskal's theorem implies a theoretical upper bound on the complexity of the system. This bound is, however, far from having been reached by known examples of rewrite systems. All known orderings used to establish termination by Kruskal's theorem yield a multiply recursive bound. Furthermore, the study of the order types of such orderings suggests that the class of multiple recursive functions constitutes the least upper bound. Contradicting this intuition, we construct here a rewrite system which reduce by Kruskal's theorem and whose complexity is not multiply recursive. This system is even totally terminating. This leads to a new lower bound for the complexity of totally terminating rewrite systems and to rewrite systems that reduces by Kruskal's theorem. Our construction relies on the Hydra battle using classical tools from ordinal theory and subrecursive functions.It can be extended to exhaust the provably total functions of Peano arithmetic.

Lazy Functional Algorithms for Exact Real Functionals
by Alex K. Simpson

We show how functional languages can be used to write programs for real-valued functionals in exact real arithmetic. We concentrate on two useful functionals: definite integration, and the functional returning the maximum value of a continuous function over a closed interval. The algorithms are a practical application of a method, due to Berger, for computing quantifiers over streams. Correctness proofs for the algorithms make essential use of domain theory.

Locality of order-invariant first-order formulas
by Martin Grohe, Thomas Schwentick

A query is local if the decision of whether a tuple in a structure satisfies this query only depends on a small neighborhood of the tuple. We prove that all queries expressible by order-invariant first-order formulas are local.

Spatial and Temporal Refinement of Typed Graph Transformation Systems
by M. Grosse--Rhode, F. Parisi--Presicce, M. Simeoni

Graph transformation systems support---among others---the formal modeling and specification of dynamic, concurrent, and distributed systems. States are given by their graphical structure, and transitions are modeled by graph transformation rules. In this paper we investigate two kinds of refinement relations for graph transformation systems. In a spatial refinement each rule is refined by an amalgamation of rules, in a temporal refinement it is refined by a sequence of rules. Types for graph transformation systems are used as a structuring means that allows uniform restrictions and extensions of rules and derivations. With these constructions hiding can be introduced in the refinement relations, which supports the modeling of implementation. The background of these investigations is the development of a module concept for typed graph transformation systems, with export and import interfaces, and a body implementing the services offered at the export interface.

Predicative Polymorphic Subtyping
by Marcin Benke

We consider a version of the Mitchell's subsumption. Here, it is not suited for the system F but for the predicative version of it introduced by Leivant. The aim of the approach is to propose a new notion of polymorphic functional subsumption which may be decidable unlike the Mitchell's one. We define a system for predicative subsumption in the style of Mitchell and then prove its equivalence with a Gentzen-style definition. Next, we study the notion of bicoercibility. This is followed by a reduction of the typability in the Leivant's system with subsumption to subsumption itself.

On defect effect of bi-infinite words
by Juhani Karhumaeki, Jan Manuch, Wojciech Plandowski

We prove the following two variants of the defect theorem. Let X be a finite set of words over a finite alphabet. Then if a nonperiodic bi-infinite word w has two X-factorizations, then the combinatorial rank of X is at most \card(X)-1, i.e.\ there exists a set F such that X\subseteq F^+ with \card(F)<\card(X). Moreover, in the case \card(F)=\card(X), the number of periodic bi-infinite words which has two different X-factorizations is finite. Further, if \card(X)=2 and a bi-infinite word possesses two X-factorizations which are not shift-equivalent, then the primitive roots of the words in X are conjugates.

Tally NP Sets and Easy Census Functions
by Judy Goldsmith, Mitsunori Ogihara, Joerg Rothe

We study the question of whether every P set has an easy (i.e., polynomial-time computable) census function. We characterize this question in terms of unlikely collapses of language and function classes such as the containment of #P_1 in FP, where #P_1 is the class of functions that count the witnesses for tally NP sets. We prove that every #P_{1}^{PH} function can be computed in FP^{#P_{1}^{#P_{1}}}. Consequently, every P set has an easy census function if and only if every set in the polynomial hierarchy does. We show that the assumption #P_1 being contained in FP implies P = BPP and that PH is contained in MOD_{k}P for each k \geq 2, which provides further evidence that not all sets in P have an easy census function. We also relate a set's property of having an easy census function to other well-studied properties of sets, such as rankability and scalability (the closure of the rankable sets under P-isomorphisms). Finally, we prove that it is no more likely that the census function of any set in P can be approximated (more precisely, can be n^{\alpha}-enumerated in time n^{\beta} for fixed \alpha and \beta) than that it can be precisely computed in polynomial time.

Minimum Propositional Proof Length is NP-Hard to Linearly Approximate
by Michael Alekhnovich, Sam Buss, Shlomo Moran, Toniann Pitassi

We prove that the problem of determining the minimum propositional proof length is NP-hard to approximate within any constant factor. These results hold for all Frege systems, for all extended Frege systems, for resolution and Horn resolution, and for the sequent calculus and the cut-free sequent calculus. Also, if NP is not in QP (quasi-polynomial time), then it is impossible to approximate minimum propositional proof length within a factor of 2^{\log^{(1-e)} n} for any constant e>0. All these hardness of approximation results apply to proof length measured either by number of symbols or by number of inferences, for tree-like or dag-like proofs. We introduce the Monotone Minimum (Circuit) Satisfying Assignment problems and prove the same hardness results for these problems.

A Superpolynomial Lower Bound for a Circuit Computing the Clique Function with at most (1/6)loglog n Negation Gates
by Kazuyuki Amano, Akira Maruoka

In this paper, we investigate about a lower bound on the number of gates in a Boolean circuit that computes the clique function with a limited number of negation gates. To derive strong lower bounds on the size of such a circuit we develop a new approach by combining the three approaches: the restriction applied for constant depth circuits, the approximation method applied for monotone circuits and boundary covering developed in the present paper. Based on the approach the following statement is established: If a circuit C with at most (1/6)loglog m negation gates detects cliques of size (log m)^(3 sqrt(log m)) in a graph with m vertices, then C contains at least 2^((1/5)(log m)^(sqrt(log m))) gates. No non-trivial lower bounds on the size of such circuits were previously known even if we restrict the number of negation gates to be a constant. Moreover, by the Fischer's result if one can improve the number of negation gates (1/6)loglog m up to 2log m in the statement, then we have that P not equal to NP. In addition, we present a general relationship between negation-limited circuit size and monotone circuit size of an arbitrary monotone function.

Degree-preserving forests
by Hajo Broersma, Andreas Huck, Ton Kloks,Otto Koppius, Dieter Kratsch, Haiko Mueller, Hilde Tuinstra

We consider the degree-preserving spanning tree (DPST) problem: given a connected graph G, find a spanning tree T of G such that as many vertices of T as possible have the same degree in T as in G. This problem is a graph-theoretical translation of a problem arising in the system-theoretical context of identifiability in networks, a concept which has applications in e.g., water distribution networks and electrical networks. We show that the DPST problem is NP-hard, even when restricted to split graphs or bipartite planar graphs, but that it can be solved in polynomial time for AT-free graphs and for graphs with bounded treewidth. Moreover, we present linear time approximation algorithms for planar graphs of worst case performance ratio (k-1)/k for every integer k>1.

The semi-full closure of Pure Type Systems
by Gilles Barthe

R. Pollack introduced the class of semi-full Pure Type Systems and gave an efficient type-checking algorithm for Pure Type Systems in that class. We show that every so-called functional Pure Type System may be extended to a semi-full Pure Type System. Moreover, the extension is conservative and preserves weak normalisation. Based on these results, we give a new efficient and conceptually simple type-checking algorithm for functional Pure Type Systems. As a further application of our method, we show that the Barendregt-Geuvers-Klop conjecture implies the K-conjecture for all functional specifications.

Proof Theory of Fuzzy Logics: Urquhart's C and Related Logics
by Matthias Baaz, Agata Ciabattoni, Christian Fermueller, Helmut Veith

We investigate the proof theory of Urquhart's C and other logics underlying the most prominent fuzzy logics, such as Goedel, Lukasiewicz and Product logic (cf. Hajek's forthcoming book.) All these logics share the property that their truth values are linearly ordered. We define hypersequent calculi for such logics, and show the following results: (1) The contraction-free counterparts of intuitionistic logic and Goedel logic (including C) admit cut-elimination. (2) Validity in these logics is decidable, and in fact in PSPACE. (3) Hajek's basic fuzzy logic BL properly extends the contraction-free Goedel logics. (4) The axiom for commutativity of the minimum is independent from the other axioms of BL. (5) All abovementioned logics are distinct from each other.

Facial circuits of planar graphs and context-free languages.
by Bruno Courcelle, Denis Lapoire

It is known that a language is context-free iff it is the set of borders of the trees of recognizable set, where the border of a (labelled) tree is the word consisting of its leaf labels read from left to right. We give a generalization of this result in terms of planar graphs of bounded tree-width. Here the border of a planar graph is the word of edge labels of a path which borders a face for some planar embedding. We prove that a language is context-free iff it is the set of borders of the graphs of a set of (labelled) planar graphs of bounded tree-width which is definable by a formula of monadic second-order logic.

The equivalence problem for deterministic pushdown transducers into abelian groups

the equivalence problem for deterministic pushdown transducers with inputs in a free monoid X^* and outputs in an abelian group H is shown to be decidable. The result is obtained by constructing a complete formal system for equivalent pairs of deterministic rational series on the variable alphabet associated with the dpdt M with coefficients in the monoid H^0 (the monoid obtained by adjoining a zero to the group H).

Nonstochastic languages being projections of 2-tape quasideterministic languages
by Richard Bonner, Rusins Freivalds, Janis Lapins, Antra Lukjanska

A language L_k of k-tuples of words which is recognized by a k-tape rational probabilistic finite automaton with probability 1 - \varepsilon, for arbitrary \varepsilon > 0, is called quasideterministic. It is proved by R. Freivalds in 1982 that each rational stochastic language is a projection of a quasideterministic language L_k of k-tuples of words. Had projections of quasideterministic languages on one tape always been rational stochastic languages, we would have a good characterization of the class of the rational stochastic languages. However we prove the opposite in this paper. A two-tape qusideterministic language exists, the projection of which on the first tape is a nonstochastic language.

forallexists^ast-Equational Theory of Context Unification is Pi_1^0-Hard
by Sergei Vorobyov

Context unification is a particular case of second-order unification, where all second-order variables are *unary* and only *linear* functions are sought for as solutions. Its decidability is an *open* problem. We present the simplest (currently known) undecidable quantified fragment of the theory of context unification by showing that for every signature containing a more-than-unary symbol one can construct a context equation E[p,r,F,w] with parameter p, first-order variables r, w, and context variables F such that the set of true sentences of the form forall r exists F exists w E[p,r,F,w] is \Pi_1^0-hard (i.e., every co-r.e. set is many-one reducible to it), as p ranges over finite words of a binary alphabet.
Moreover, the existential prefix above contains just 5 context and 3 first-order variables (this can be further improved). It follows, in particular, that the forall exists^8-equational theory of context unification is undecidable.

Tree decompositions of small diameter
by Hans L. Bodlaender, Torben Hagerup

Motivated by applications in parallel and dynamic graph algorithms, we investigate the tradeoff between width and diameter of tree decompositions. For all integers n, k and K with 1 <= k <= K <= n-1, denote by D(n,k,K) the maximum, over all n-vertex graphs G of treewidth k, of the smallest diameter of a tree decomposition of G of width K. We determine D(n,k,K), up to a constant factor, for all values of n, k and K. When K is bounded by a constant (the case of greatest practical relevance), D(n,k,K) is Theta(n) for K <= 2 k-1, Theta(sqrt(n)) for 2 k <= K <= 3 k-2, and Theta(log n) for K >= 3 k-1. We provide much more accurate bounds for the case K <= 2 k-1.

Speeding-up Nondeterministic Single-Tape Off-Line Computations by One Alterantion
by Jiri Wiedermann

It is shown that for a well-behaved function T(n) any nondeterministic single-tape off-line Turing amchine of time complexity T(n) can be speeded-up by one extra alternation by the factor log log n/\sqrt{T(n)}. This leads to the seaparation of the respective time bounded classes within the respective \Sigma hierarchy. Analogous result holds also for the complementary classes in the \Pi hierarchy. This is the first occasion where such separation results have been proved for a restricted type of multitape nondeterministic machines. For the general case of multitape nondeterministic machines similar results are not known to hold.

Iterated Length-Preserving Transductions
by Michel Latteux, David Simplot, Alain Terlutte

The purpose of this paper is the study of the smallest family of transductions containing length-preserving rational transductions and closed under union, composition and iteration. We give several characterizations of this class using restricted classes of length-preserving transductions, by showing the connections with ``context-sensitive transductions'' and transductions associated with recognizable picture languages. We also study the class obtained by only using length-preserving rational functions and we show the relations with ``deterministic context-sensitive transductions''.

Comparison between the complexity of a function and the complexity of its graph
by Bruno Durand, Sylvain Porrot

This paper investigates in terms of Kolmogorov complexity the differences between the complexity of a recursive function and the complexity of its graph. Our first result is that the complexity of the initial parts of the graph of a recursive function, although bounded, has almost never a limit. The second result is that the complexity of these initial parts approximate the complexity of the function itself in most cases (and in the average) but not always.

Representing Hyper-Graphs by Regular Languages
by Salvatore La Torre, Margherita Napoli

A new compact representation of infinite graphs is investigated. Regular languages are used to represent labelled hyper-graphs which can be also multi-graphs. Our approach is similar to that used by A. Ehrenfeucht, J. Engelfriet and G. Rozenberg for finite graphs since we use a regular prefix-free language as set of vertices, but it differs from th at in the representation of the edges. In fact, we use a regular language for the edges instead of a finite loop-free graph. Our approach preserves the finite representation of the edges and of the corresponding labelling mapping and yields to a higher expressive power. As a matter of fact, our graph representation results to be more powerful than the equational graphs introduced by B. Courcelle. Moreover, the use of a regular prefix-free language to represent the vertices allows (fixed the language of the edges) to express a graph by a labelled tree. The advantage to represent graphs by trees is that properties of graphs can be verified by induction on the tree, often leading to efficient algorithms.

Computing epsilon-Free NFA from Regular Expressions in O(n log^2(n)) Time
by Christian Hagenah, Anca Muscholl

The standard procedure to transform a regular expression to an \epsilon-free NFA yields a quadratic blow-up of the number of transitions. For a long time this was viewed as an unavoidable fact, until Hromkovi\u{c}[hsw97] exhibited recently a construction yielding \epsilon-free NFA with O(n \log^2(n)) transitions. However, the complexity of the construction was left open. In this paper we present optimal sequential and parallel algorithms for the construction described in [hsw97].

Reducing AC-Termination to Termination
by Maria Ferreira, Delia Kesner, Laurence Puel

We present a new technique for proving AC-termination. We show that if certain conditions are met, AC-termination can be reduced to termination, i. e., termination of a TRS S modulo an AC-theory can be inferred from termination of another TRS R with no AC-theory involved. This is a new perspective and opens new possibilities to deal with AC-termination.

About Synchronization Languages
by Isabelle Ryl, Yves Roos, Mireille Clerbout

Synchronization languages are a model used to describe the behaviors of distributed applications whose synchronization constraints are expressed by synchronization expressions. Synchronization languages were conjectured by Guo, Salomaa and Yu to be characterized by a rewriting system. We have shown that this conjecture is not true. This negative result has led us to extend the rewriting system and Salomaa and Yu to extend the definition of synchronization languages. The aim of this paper is to establish the link between these two extensions, we show that the behaviors expressed by the two families of synchronization languages are only separated by morphisms.

A (non-elementary) modular decision procedure for LTrL
by Paul Gastin, Raphael Meyer, Antoine Petit

Thiagarajan and Walukiewicz have defined a temporal logic LTrL on Mazurkiewicz traces, patterned on the famous propositional temporal logic of linear time LTL defined by Pnueli. They have shown that this logic is equal in expressive power to the first order theory of finite and infinite traces. The hopes to get an ``easy'' decision procedure for LTrL, as it is the case for LTL, vanished very recently due to a result of Walukiewicz who showed that the decision procedure for LTrL is non-elementary. However, tools like Mona or Mosel show that it is possible to handle non-elementary logics on significant examples. Therefore, it appears worthwhile to have a direct decision procedure for LTrL; in this paper we propose such a decision procedure, in a modular way. Since the logic LTrL is not pure future, our algorithm constructs by induction a finite family of Buchi automata for each LTrL-formula. As expected by a recent results of Walukiewicz, the main difficulty comes from the ``Until'' operator.

When Can an Equational Simple Graph Be Generated by Hyperedge Replacement?
by Klaus Barthelmann

Infinite hypergraphs with sources arise as the canonical solutions of certain systems of recursive equations written with operations on graphs. There are basically two different sets of such operations known from the literature, HR and VR. VR is strictly more powerful than HR on simple graphs. Necessary conditions are known ensuring that a VR-equational simple graph is also HR-equational. We prove that two of them, namely having finite tree-width or not containing the infinite bipartite graph, are also sufficient. This shows that equational graphs behave like context-free sets of finite graphs.
Using an alternate characterization of VR-equational simple graphs [Barthelmann1997], this result provides a (necessary and) sufficient condition and an effective procedure to translate a language-theoretic definition of an infinite graph [Caucal1996] into an operational one based on substitution [Courcelle1989].

Positive Turing and Truth-Table Completeness for NEXP Are Incomparable
by Levke Bentzien

Using ideas introduced by Buhrman et al. ([BHT91], [BST93]) to separate various completeness notions for NEXP=NTIME(2^{poly}), positive Turing complete sets for NEXP are studied. In contrast to many-one completeness and bounded truth-table completeness with norm 1 which are known to coincide on NEXP ([BST93]), whence any such set for NEXP is positive Turing complete, we give sets A and B such that \begin{itemize} \item[(1)] A is bT(2)-complete but not posT-complete for NEXP \item[(2)] B is posT-complete but not tt-complete for NEXP. \end{itemize} These results come close to optimality since a further strengthening of (1), as was done by Buhrman in [Bu93] for EXP=DTIME(2^{poly}), seems to require the assumption NEXP=co-NEXP.

Improved Time and Space Hierarchies of One-Tape Off-Line TMs
by Kazuo Iwama, Chuzo Iwamoto

This paper presents improved time and space hierarchies of one-tape off-line Turing Machines (TMs), which have a single worktape and a two-way input tape: (i) For any time-constructible functions t_1(n) and t_2(n) such that \inf_{n\rightarrow\infty}\frac{t_1(n)\log\log t_1(n)}{t_2(n)}=0 and t_1(n)=n^{O(1)}, there is a language which can be accepted by a t_2(n)-time TM, but not by any t_1(n)-time TM. (ii) For any space-constructible function s(n) and positive constant \epsilon, there is a language which can be accepted in space s(n)+\log s(n)+(2+\epsilon)\log\log s(n) by a TM with two worktape-symbols, but not in space s(n) by any TM with the same worktape-symbols. The (\log\log t_1(n))-gap in~(i) substantially improves the Hartmanis and Stearns' (\log t_1(n))-gap which survived more than 30 years.

Deadlocking States in Context-free Process Algebra
by Jiri Srba

Recently it has been shown that the class of BPA (or context-free) processes can be widely used to describe sequential processes and to define their semantics. This class has been intensively studied. Bisimilarity and regularity appeared to be decidable within the BPA processes (see \cite{CHHS:BPA-bisimilarity-IC,BCS:elementaryBPA, BCS:BPA-regularity}). We extend these processes with a deadlocking state into \BPAd systems. Bosscher has proved that bisimilarity and regularity remain decidable [bosscher:PhD]. In this paper we continue with the study initiated by Bosscher. We generalise his approach introducing strict and nonstrict version of bisimilarity. We show that the \BPAd class is more expressive w.r.t. (both strict and nonstrict) bisimilarity but it remains language equivalent to BPA. Finally we give a characterisation of those \BPAd processes which can be equivalently (up to bisimilarity) described within the `pure' BPA syntax.

Expressive Completeness of Temporal Logic of Action
by Alexander Rabinovich

The paper compares the expressive power of monadic second order logic of order, a fundamental formalism in mathematical logic and theory of computation, with that of a fragment of Temporal Logic of Actions introduced by Lamport for specifying th e behavior of concurrent systems.

On the Complexity of Wavelength Converters
by Vincenzo Auletta, Ioannis Caragiannis, Christos Kaklamanis, Pino Persiano

In this paper the capabilities of an all--optical network model that supports wavelength conversion are investigated. The model applies to tree--shaped optical networks and was established in [sirocco]. A few wavelength converters are maintained at each non--leaf network node. We present a greedy wavelength routing algorithm that allocates a total bandwidth of w(l) wavelengths to any set of requests of load l (where load is defined as the maximum number of requests that go through any directed fiber link) and we give sufficient conditions for correct operation of the algorithm when applied to binary tree networks. We exploit properties of (explicitly constructed) Ramanujan graphs to show that (for the case of binary tree networks) our algorithm increases the bandwidth utilized compared to the algorithm presented in [gargano]. Furthermore, we use another class of graphs called dispersers, for which almost optimal explicit constructions are known, to implement wavelength converters of asymptotically optimal complexity with respect to their size (the number of all possible conversions). We prove that their use leads to optimal and nearly--optimal bandwidth allocation even in a greedy manner.

Randomness vs. Completeness: On the Diagonalization Strength of Resource-Bounded Random Sets
by Klaus Ambos-Spies, Steffen Lempp, Gunther Mainhardt

We show that the question whether the p-tt-complete or p-T-complete sets for the deterministic time classes {\bf E} and {\bf EXP} have measure 0 in these classes in the sense of Lutz's resource-bounded measure connot be decided by relativizable techniques. On the other hand we obtain the following absolute results if we bound the norm, i.e. the number of oracle queries of the reductions: For r=tt,T, \[\mu_p(\{C:\: C\: \mbox{p-r(kn)-complete for {\bf E}}\})=0\] and \[\mu_{p_2}(\{C:\: C\: \mbox{p-r(n^k)-complete for {\bf EXP} }\})=0.\] In the second part of the paper we investigate the diagonalization strength of random sets in an abstract way by relating randomness to a new genericity concept. This provides an alternative quite elegant and powerful approach for obtainig results on resource-bounded measures like the ones in the first part of the paper.

A Parallelization of Dijkstra's Shortest Path Algorithm
by A. Crauser, K. Mehlhorn, U. Meyer, P. Sanders

Despite much effort the single source shortest path (SSSP) problem has resisted parallel solutions which are fast and simultaneously work-efficient. We propose simple criteria which divide Dijkstra's sequential SSSP algorithm into a number of phases, such that the operations within a phase can be savely done in parallel. We give a PRAM algorithm based on these criteria and analyze its performance on random digraphs with random edge weights uniformly distributed in [0,1]. We use the G(n,d/n) model: the graph consists of n nodes and each edge is chosen with probability d/n. Our PRAM algorithm needs O(n^(1/3) log n) time and O(n log n + dn) work with high probability (whp). We also give extensions to external memory computation: we derive an algorithm which needs O(n/D + dn/(DB) log_(S/B) dn/(DB)) I/Os whp and can use up to D=O(min{ n^(2/3)/log n , S/B }) independent disks. The blocksize is given by B, S denotes the size of internal memory. Simulations show the applicability of our approach even on non-random graphs.

D0L-Systems and Surface Automorphisms
by Luis-Miguel Lopez, Philippe Narbel

We introduce a new relationship between language theory and surface theory. More specifically, we show how substitutions on words can represent automorphisms of surfaces. This fact is then applied to construct and analyze non-periodic irreducible automorphisms. This is obtained by using results about D0L-systems, mainly the decidability of the non-repetitiveness of a D0L-language. We also show how properties about substitutions like primitivity and non-cyclicity can be checked through topological means.

Probabilistic Concurrent Constraint Programming: Towards a Fully Abstract Model
by Alessandra Di Pierro, Herbert Wiklicky

This paper presents a Banach space based approach towards a denotational semantics of a probabilistic constraint programming language. The existence of fixed-points is guaranteed by the Brouwer-Schauder Fixed-Point Theorem. A concrete fixed-point construction is also presented which corresponds to a notion of observables capturing the exact results of both finite and infinite results.

Embedding of Hypercubes into Grids
by Sergej Bezrukov,Joe Chavez,Larry Harper,Markus Roettger,Ulf-Peter Schroeder

We consider one-to-one embeddings of the n-dimensional hypercube into grids with 2^n vertices and present lower and upper bounds and asymptotic estimates for minimal dilation, edge-congestion, and their mean values. We also introduce and study two new cost-measures for these embeddings, namely the sum over i=1,...,n of dilations and the sum of edge-congestions caused by the hypercube edges of the ith dimension. It is shown that, in the simulation via the embedding approach, such measures are much more suitable for evaluating the slowdown of uniaxial hypercube algorithms then the traditional cost measures.

Approximating Maximum Independent Sets in Uniform Hypergraphs
by Thomas Hofmeister,Hanno Lefmann

We consider the problem of approximating the independence number and the chromatic number of k-uniform hypergraphs on n vertices. For fixed integers k \geq 2, we obtain for both problems that one can achieve in polynomial time approximation ratios of at most O(n/(\log^{(k-1)} n)^2). This extends results of Boppana and Halld\'orsson [BH92] who showed for the graph case that an approximation ratio of O(n/(\log n)^2) can be achieved in polynomial time. On the other hand, assuming NP \neq ZPP, one cannot obtain in polynomial time for the independence number and the chromatic number of k-uniform hypergraphs an approximation ratio of n^{1-\epsilon} for fixed \epsilon > 0.

Iterated Function Systems and Control Languages
by Henning Fernau, Ludwig Staiger

The paper shows an application of formal language theory to fractals. Here we consider fractals generated by iterated function systems (IFS). It is known that introducing a structure (device) controlling the sequence of applications of the functions in the IFS allows for a wider range of representable fractals.
One of the major tasks in the analysis of fractals is the estimation of their dimension (Hausdorff dimension). In the present paper we investigate IFS with languages as control structures, that is, the set of allowed ``addresses'' (w.r.t. the IFS) of points in the fractal is restricted according to the underlying language.
We show that under some well-known assumption from fractal geometry (the so called Open Set Condition) on the IFS the fractal dimension can be easily estimated from a generalization of the entropy of languages.
We proceed in three steps:
First we investigate the so-called \beta-entropy, which is a generalization of the usual entropy of languages introduced by Chomsky and Miller. The definition of the \beta-entropy takes into account the different weights of the letters of alphabet, which is assigned according to the differing contracting factors of the mappings of the IFS.
Next we apply this result to estimate the fractal dimension (Hausdorff dimension) in the space of addresses.
In the subsequent section we investigate in more detail the relationships between the control language and the mappings of the IFS. Here our main result asserting that the real Hausdorff dimension of the fractal equals the Hausdorff dimension in the address space provided the IFS fulfills the Open Set Condition is proved.
KEYWORDS: entropy of languages, iterated function systems, fractals, dimension,

Additive Cellular Automata over {Z}_p and the Bottom of (CA,leq)
by I. Rapaport, J. Mazoyer

In a previous work we began to study the question of how to compare cellular automata (CA). In this context it was introduced a preorder (CA,\leq) admitting a global minimum and it was shown that on the bottom of (CA,\leq) are located all the CA satisfying very simple dynamical properties as nilpotency or periodicity. In this paper we prove that also the (algebraically amenable) additive CA over \Z_p are located on the bottom of (CA,\leq). This result encourages our conjecture that says that ``being on the bottom of (CA,\leq)'' means ``being simple'' or, in a more general way, that the ``distance'' from the minimum could represent a measure of ``complexity'' on CA. We also prove that the additive CA over \Z_p with p primes are two by two incomparable. This fact improves considerably our understanding of (CA,\leq) because it means that the minimum, even in the canonical order compatible with \leq, has infinite outdegree.

On the Composition Problem for OBDDs With Different Variable Orderings
by Anna Slobodova

Ordered Binary Decision Diagram is the favorite data structure used for representation Boolean functions in computer-aided synthesis and verification of digital systems. The secret of their success is the efficiency of the algorithms for Boolean operations, satisfiability and equivalence check. However, the algorithms work well under condition only that the variable ordering of considered OBDDs is the same.
In this paper, we discuss the problem of Boolean operations on OBDDs with different variable orderings, which naturally appears, e.g., in the connection with OBDD minimization techniques that are based on variable reordering. Our goal is to place the problem with respect to its complexity and to point out the difficulties in finding an acceptable solution.

A Computational Interpretation of the lambdamu-calculus
by G.M. Bierman

This paper proposes a simple computational interpretation of Parigot's \lambda\mu-calculus. The \lambda\mu-calculus is an extension of the typed \lambda-calculus which corresponds via the Curry-Howard correspondence to classical logic. Whereas other work has given computational interpretations by translating the \lmc\ into other calculi, I wish to propose here that the \lmc\ itself suggests a novel computational interpretation. This interpretation is best given as a single-step semantics which, in particular, leads to a relatively simple, but powerful, operational theory.

Complete Abstract Interpretations made Constructive
by Roberto Giacobazzi, Francesco Ranzato, Francesca Scozzari

Completeness is a desirable, although uncommon, property in abstract interpretation, formalizing the intuition that, relatively to the underlying abstract domains, the abstract semantics is as precise as possible. We consider here the most general form of completeness, where concrete semantic functions can have different domains and ranges, a case particularly relevant in functional programming. In this setting, our main contributions are as follows. (i) Under the weak and reasonable hypothesis of continuous semantic functions, a constructive characterization of the least complete extension and the greatest complete restriction of an abstract interpretation is given. The existence of more restricted forms of similar abstractions was recently proved by the first two authors. (ii) In projection-based program analysis, our results show that the so-called least backward abstractions of co-continuous semantic functions always exist and can be constructively characterized. This improves considerably over previous works in the field. (iii) Our results generalize the notion of quotient of abstract domains, a tool introduced by Cortesi et al. for comparing the expressive power of abstract interpretations. Fairly severe hypotheses are required for Cortesi et al.'s quotients to exist. We prove instead that continuity of the semantic functions guarantees the existence of our generalized quotients.

On Boolean vs. Modular Arithmetic for Circuits and Communication Protocols
by Carsten Damm

We compare two computational models that appeared in the literature in a Boolean setting and in an analog setting based on modular arithmetic. We prove that in both cases the arithmetic version can to some extend simulate the Boolean version. Although the models are very different, the proofs rely on the same idea based on the Schwartz-Zippel-Theorem.
In the first part we give a new simulation of semi-unbounded Boolean circuits by semiunbounded circuits with unbounded parity gates. Our simulation is simpler and more efficient with respect to depth than the original simulation of G\'al and Wigderson [GalWigderson]. In the second part we prove, that two-party parity communication protocols can approximate nondeterministic communication protocols. A strict simulation of one by the other is impossible as was shown in [DKMW97+].

Model Checking Real-Time Properties of Symmetric Systems
by E. Allen Emerson, Richard J. Trefler

We develop efficient algorithms for model checking quantitative properties of symmetric reactive systems in the general framework of a Real-Time Mu-calculus. Previous work has been limited to qualitative correctness properties. Our work not only permits handling of quantitative correctness, but it provides a strictly more expressive framework for qualitative correctness since the Mu-calculus strictly subsumes, e.g, CTL*. Unlike the previous ``group-theoretic'' approaches of [CEFJ96] and [ES96] and the technical ``automata-theoretic'' approach of [ES97], our new approach may be viewed as ``model-theoretic''.

On counting AC^0 circuits with negative constants
by Andris Ambainis, David Mix Barrington, Huong LeThanh

Continuing the study of the relationship between TC^0, AC^0 and arithmetic circuits, started by Agrawal et al., we answer a few questions left open in this paper. Our main result is that the classes DiffAC^0 and GapAC^0 coincide, under poly-time, log-space, or log-time uniformity. From that we can derive that under logspace uniformity, the following equalities hold: \[C_=AC^0=PAC^0=TC^0.\]

Reconstructing Polyatomic Structures from Discrete X-Rays: NP-Completeness Proof for Three Atoms
by Marek Chrobak, Christoph Durr

We address a discrete tomography problem arising in the study of the atomic structure of crystal lattices. A polyatomic structure T is an integer lattice in dimension D>=2, whose points may be occupied by c types of atoms. To ``analyze'' T, we conduct l measurements that we refer to as _discrete X-rays_. A discrete X-ray in direction xi determines the number of atoms of each type on each line parallel to xi. Given such l non-parallel X-rays, we wish to reconstruct T.
The complexity of the problem for c=1 (one atom) has been completely determined by Gardner, Gritzmann and Prangerberg, who proved that the problem is NP-complete for any dimension D>=2 and l>=3 non-parallel X-rays, and that it can be solved in polynomial time otherwise.
The NP-completeness result above clearly extends to any c>=2, and therefore when studying the polyatomic case we can assume that l = 2. As shown in another article by the same authors, this problem is also NP-complete for c>=6 atoms, even for dimension D=2 and for the axis-parallel X-rays. The authors of that article conjecture that the problem remains NP-complete for c =3,4,5.
We resolve this conjecture by proving that the problem is indeed NP-complete for c>=3 in 2D, even for the axis-parallel X-rays. Our construction relies heavily on some structure results for the realizations of 0-1 matrices with given row and column sums.

Polymorhic subtyping without distributivity
by Jacek Chrzaszcz

The subtyping relation in the polymorphic second-order lambda-calculus was introduced by John C. Mitchell in 1988. It is known that this relation is undecidable, but all known proofs of this fact strongly depend on the distributivity axiom. Nevertheless it has been conjectured that this axiom does not influence the undecidability.
The present paper shows undecidability of subtyping when we remove distributivity from its definition. Furthermore, the full equational axiomatisation of the corresponding equivalence relation is given. Both results follow from an analysis of rewriting-style subtyping derivations.

One guess one-way cellular arrays
by Thomas Buchholz, Andreas Klein, Martin Kutrib

One-way cellular automata with restricted nondeterminism are investigated. The number of allowed nondeterministic state transitions is limited to a constant. It is shown that a limit to exactly one step does not decrease the language accepting capabilities. We prove a speed-up result that allows any linear-time computation to be sped-up to real-time. Some relationships to deterministic arrays are considered. Finally we prove several closure properties of the real-time languages.

Timed Bisimulation and Open Maps
by Thomas Hune, Mogens Nielsen

Open maps have been used for defining bisimulations for a number of models, but none of these have modelled real-time. We define a category of timed transition systems, and use the general framework of open maps to obtain a notion of bisimulation. We show this to be equivalent to the standard notion of timed bisimulation. Thus the abstract results from the theory of open maps apply, e.g. the existence of canonical models and characteristic logics. Here, we provide an alternative proof of decidability of bisimulation for finite timed transition systems in terms of open maps, and illustrate the use of the open maps in presenting bisimulations.

Optimizing OBDDs Is Still Intractable for Monotone Functions
by Kazuo Iwama, Mitsushi Nozoe

Optimizing the size of Ordered Binary Decision Diagrams is shown to be NP-complete for monotone Boolean functions. The same result for general Boolean functions was obtained by Bollig and Wegener recently.

Tarskian set constraints are in NEXPTIME
by Pawel Mielniczuk, Leszek Pacholski

In this paper we show that satisfiability of Tarskian set of constraints can be decided in exponential time thus filling the "main gap" left in the paper "Tarskian set constraints" by Givan, Kozen, McAllester and Witty.

The Head Hierarchy for Oblivious Finite Automata with Polynomial Advice Collapses
by Holger Petersen

We show that the hierarchy of classes of languages accepted by finite multi-head automata with oblivious head movements that receive polynomial advice strings collapses to the fifth level. A characterization of nondeterministic logarithmic space with polynomial advice is simplified. In the presence of polynomial advice, the question whether deterministic and nondeterministic logarithmic space are equivalent can be reduced to the question whether simple nondeterministic automata can be simulated deterministically. Polynomial time can be characterized by a one-head device.
For automata without advice we prove that multi-head counter automata, stack automata and non-erasing stack automata do not lose power by the restriction to oblivious head movements.

A Separation of Planar Circuits
by B. Csaba, A. Pluhar, T. Szeles

There are several lower bounds for planar circuit complexity of Boolean functions. Here we are interested in that if planar circuits with all input and output nodes are located on the outer face are less powerfull than planar circuits in general. Using a special basis B, we shall give an `n against n^3/2' separation between the above mentioned two models. That is we exhibit a sequence of functions f_n, such that the computation of f_n by a planar circuit needs O(n) gates over the basis B, while it needs \Omega(n^{3/2}) in the restricted model. It is also shown that this is the worst case since, over any reasonable basis, a planar circuit of size O(n) can be transformed to a restricted one of size O(n^{3/2}).