FST TCS 2000: Foundations of Software Technology and Theoretical Computer Science

Model checking is an automatic method for verifying correctness of reactive programs. Originally proposed as part of the dissertation work of the author, model checking is based on efficient algorithms searching for the presence or absence of temporal patterns. In fact, model checking rests on a theoretical foundation of basic principles from modal logic, lattice theory, as well as automata theory that permits program reasoning to be completely automated in principle and highly automated in practice. Because of this automation, the practice of model checking is nowadays well-developed, and the range of successful applications is growing. Model checking is used by most major hardware manufacturers to verify microprocessor circuits, while there have been promising advances in its use in software verification as well. The key obstacle to applicability of model checking is, of course, the state explosion problem. This paper discusses part of our ongoing research program to limit state explosion. The relation of theory to practice is also discussed.

This document proposes an algebra for XML Query. The algebra has been submitted to the W3CXM L Query Working Group. A novel feature of the algebra is the use of regular-expression types, similar in power to DTDs or XML Schemas, and closely related to Hasoya, Pierce, and Vouillon’s work on Xduce. The iteration construct involves novel typing rules not encountered elsewhere (even in Xduce).

In 1935, van der Corput asked the following question: Given an infinite sequence of reals in [0, 1], define $$ D(n) = \mathop {\sup }\limits_{o \leqslant x \leqslant 1} \left| {|S_n \cap [0,x]| - nx} \right|,$$ where S_n consists of the first n elements in the sequence. Is it possible for D(n) to stay in O(1)? Many years later, Schmidt proved that D(n) can never be in o(log n). In other words, there are limitations on how well the discrete distribution, x → ∣S_n ∩ [0, x] |, can simulate the continuous one, x → nx. The study of this intriguing phenomenon and its numerous variants related to the irregularities of distributions has given rise to discrepancy theory. The relevance of the subject to complexity theory is most evident in the study of probabilistic algorithms. Suppose that we feed a probabilistic algorithm not with a perfectly random sequence of bits (as is usually required) but one that is only pseudorandom or even deterministic. Should performance necessarily suffer? In particular, suppose that one could trade an exponential-size probability space for one of polynomial size without letting the algorithm realize the change. This form of derandomization can be expressed by saying that a very large distribution can be simulated by a small one for the purpose of the algorithm. Put differently, there exists a measure with respect to which the two distributions have low discrepancy. The study of discrepancy theory predates complexity theory and a wealth of mathematical techniques can be brought to bear to prove nontrivial derandomization results. The pipeline of ideas that flows from discrepancy theory to complexity theory constitutes the discrepancy method. We give a few examples in this survey. A more thorough treatment is given in our book [15]. We also briefly discuss the relevance of the discrepancy method to complexity lower bounds.

A metalogical framework is a logic with an associated methodology that is used to represent other logics and to reason about their metalogical properties. We propose that logical frameworks can be good metalogical frameworks when their logics support reflective reasoning and their theories always have initial models.We present a concrete realization of this idea in rewriting logic. Theories in rewriting logic always have initial models and this logic supports reflective reasoning. This implies that inductive reasoning is valid when proving properties about the initial models of theories in rewriting logic, and that we can use reflection to reason at the metalevel about these properties. In fact, we can uniformly reflect induction principles for proving metatheorems about rewriting logic theories and their parameterized extensions. We show that this reflective methodology provides an effective framework for different, non-trivial, kinds of formal metatheoretic reasoning; one can, for example, prove metatheorems that relate theories or establish properties of parameterized classes of theories. Finally, we report on the implementation of an inductive theorem prover in the Maude system, whose design is based on the results presented in this paper.References

Wireless communication technology is the basis of radio and television broadcasting, it is used in satellite-based cellular telephone systems, in point-to-multipoint radio access systems, and in terrestrial mobile cellular networks, to mention a few such systems (see [5] for more detailed information).Wireless communication networks employ radio frequencies to establish communication links. The available radio spectrum is very limited. To meet today’s radio communication demand, this resource has to be administered and reused carefully in order to controlmutual interference. The reuse can be organized via separation in space, time, or frequency, for example. The problem, therefore, arises to distribute frequencies to links in a “reasonable manner”. This is the basic form of the frequency assignment problem. What “reasonable” means, how to quantify this measure of quality, which technical side constraints to consider cannot be answered in general. The exact specification of this task and its mathematical model depend heavily on the particular application considered.

The ease with which one can copy and transform data on the Web, has made it increasingly difficult to determine the origins of a piece of data. We use the term data provenance to refer to the process of tracing and recording the origins of data and its movement between databases. Provenance is now an acute issue in scientific databases where it is central to the validation of data. In this paper we discuss some of the technical issues that have emerged in an initial exploration of thetopic.

The problem of computing the strength and performing optimal reinforcement for an edge-weighted graph G(V, E,w) is well-studied [1],[2],[3],[6],[7],[9]. In this paper, we present fast (sequential linear time and parallel logarithmic time) on-line algorithms for optimally reinforcing the graph when the reinforcement material is available continuosly online. These are first on-line algortithms for this problem. Although we invest some time in preprocessing the graph before the start of our algorithms, it is also shown that the output of our on-line algorithms is as good as that of the off-line algorithms, making our algorithms viable alternatives to the fastest off-line algorithms in situtations when a sequence of more than O(|V|) reinforcement problems need to be solved. In such a situation the time taken for preprocessing the graph is less that the time taken for all the invocations of the fastest off-line algorithms. Thus our algorithms are also efficient in the general sense. The key idea is to make use of the theory of Principal Partition of a Graph. Our results can be easily generalized to the general setting of principal partition of nondecreasing submodular functions.

We investigate a variant of on-line edge-coloring in which there is a fixed number of colors available and the aim is to color as many edges as possible. We prove upper and lower bounds on the performance of different classes of algorithms for the problem. Moreover, we determine the performance of two specific algorithms, First-Fit and Next-Fit.

We investigate polynomial-time approximability of the problems related to edge dominating sets of graphs. When edges are unitweighted, the edge dominating set problem is polynomially equivalent to the minimum maximal matching problem, in either exact or approximate computation, and the former problem was recently found to be approximable within a factor of 2 even with arbitrary weights. It will be shown, in contrast with this, that the minimum weight maximal matching problem cannot be approximated within any polynomially computable factor unless P=NP.The connected edge dominating set problem and the connected vertex cover problem also have the same approximability when edges/vertices are unit-weighted, and the former problem is known to be approximable, even with general edge weights, within a factor of 3.55. We will show that, when general weights are allowed, 1) the connected edge dominating set problem can be approximated within a factor of 3 + ∈, and 2) the connected vertex cover problem is approximable within a factor of ln n + 3 but cannot be within (1 - ∈) lnn for any ∈ > 0 unless NP ⊂ DTIME(nO(log log n)).

A pushdown system is a graph G(P) of configurations of a pushdown automaton P. The model checking problem for a logic L is: given a pushdown automaton P and a formula ? ∈ L decide if ? holds in the vertex of G(P) which is the initial configuration of P. Computation Tree Logic (CTL) and its fragment EF are considered. The model checking problems for CTL and EF are shown to be EXPTIME-complete and PSPACE-complete, respectively.

Timed computation tree logic (Tctl) extends Ctl by allowing timing constraints on the temporal operators. The semantics of Tctl is defined on a dense tree. The satisfiability of Tctl-formulae is undecidable even if the structures are restricted to dense trees obtained from timed graphs. According to the known results there are two possible causes of such undecidability: the denseness of the underlying structure and the equality in the timing constraints. We prove that the second one is the only source of undecidability when the structures are defined by timed graphs. In fact, if the equality is not allowed in the timing constraints of Tctl-formulae then the finite satisfiability in Tctl is decidable. We show this result by reducing this problem to the emptiness problem of timed tree automata, so strengthening the already well-founded connections between finite automata and temporal logics.

Equivalence between designs is a fundamental notion in verification. The linear and branching approaches to verification induce different notions of equivalence. When the designs aremodeled by fair state-transition systems, equivalence in the linear paradigm corresponds to fair trace equivalence, and in the branching paradigm corresponds to fair bisimulation. In this work we study the expressive power of various types of fairness conditions. For the linear paradigm, it is known that the Büchi condition is sufficiently strong (that is, a fair system that uses Rabin or Streett fairness can be translated to an equivalent Büchi system). We show that in the branching paradigm the expressiveness hierarchy depends on the types of fair bisimulation one chooses to use. We consider three types of fair bisimulation studied in the literature: ∃- bisimulation, game-bisimulation, and ∀-bisimulation. We show that while game- bisimulation and ∀-bisimulation have the same expressiveness hierarchy as tree automata, ∃-bisimulation induces a different hierarchy. This hierarchy lies between the hierarchies of word and tree automata, and it collapses at Rabin conditions of index one, and Streett conditions of index two.

This paper addresses the problems of counting proof trees (as introduced by Venkateswaran and Tompa) and counting proof circuits, a related but seemingly more natural question. These problems lead to a common generalization of straight-line programs which we call polynomial replacement systems. We contribute a classification of these systems and we investigate their complexity. Diverse problems falling in the scope of this study include, for example, counting proof circuits, and evaluating ∪,+-circuits over the natural numbers. The former is shown #P-complete, the latter to be equivalent to a particular problem for replacement systems.

We consider the problem of computing the second elementary symmetric polynomial $$ S_n^2 (X) \triangleq \sum _{1 \leqslant i < j \leqslant n} X_i X_j $$ using depth-three arithmetic circuits of the form $$ \sum _{i = 1}^r \prod _{j = 1}^{S_i } L_{ij} (X)$$, where each L_ij is a linear form. We consider this problem over several fields and determine exactly the number of multiplication gates required. The lower bounds are proved for inhomogeneous circuits where the Lij ’s are allowed to have constants; the upper bounds are proved in the homogeneous model. For reals and rationals the number of multiplication gates required is exactly n - 1; in most other cases, it is [n/2].This problem is related to the Graham-Pollack theorem in algebraic graph theory. In particular, our results answer the following question of Babai and Frankl: what is the minimum number of complete bipartite graphs required to cover each edge of a complete graph an odd number of times? We show that for infinitely many n, the answer is [n/2].

Here we deal with the question of definability of infinite graphs up to isomorphism by weakmo nadic second-order formulæ. In this respect, we prove that the quantifier alternation bounded hierarchy of equational graphs is infinite. Two proofs are given: the first one is based on the Ehrenfeucht-Fraissé games; the second one uses the arithmetical hierarchy. Next, we give a new proof of the Thomas’s result according to which the bounded hierarchy of the weakmo nadic second-order logic of the complete binary tree is infinite.

This paper reports on results concerning the combination of non-standard semantics via interpreters. We define what a semantics combination means and identify under which conditions a combination can be realized by computer programs (robustness, safely combinable). We develop the underlying mathematical theory and examine the meaning of several non-standard interpreter towers. Our results suggest a technique for the implementation of a certain class of programming language dialects by composing a hierarchy of non-standard interpreters.

We consider a general prescriptive type system with parametricp olymorphism and subtyping for logic programs. The property of subject reduction expresses the consistency of the type system w.r.t. the execution model: if a program is “well-typed”, then all derivations starting in a “well-typed” goal are again “well-typed”. It is well-established that without subtyping, this property is readily obtained for logicp rograms w.r.t. their standard (untyped) execution model. Here we give syntactic conditions that ensure subject reduction also in the presence of general subtyping relations between type constructors. The idea is to consider logic programs with a fixed dataflow, given by modes.

We present a framework for decision making under uncertainty where the priorities of the alternatives can depend on the situation at hand. We design a logic-programming language, DOP-CLP, that allows the user to specify the static priority of each rule and to declare, dynamically, all the alternatives for the decisions that have to be made. In this paper we focus on a semantics that reflects all possible situations in which the decision maker takes the most rational, possibly probabilistic, decisions given the circumstances. Our model theory, which is a generalization of classical logic-programming model theory, captures uncertainty at the level of total Herbrand interpretations. We also demonstrate that DOP-CLPs can be used to formulate game theoretic concepts.

We describe some new, simple and apparently general methods for designing FPT algorithms, and illustrate how these can be used to obtain a significantly improved FPT algorithm for the Maximum LeafSpanning Tree problem. Furthermore, we sketch how the methods can be applied to a number of other well-known problems, including the parametric dual of Dominating Set (also known as Nonblocker), Matrix Domination, Edge Dominating Set, and Feedback Vertex Set for Undirected Graphs. The main payoffs of these new methods are in improved functions f(k) in the FPT running times, and in general systematic approaches that seem to apply to a wide variety of problems.

We present a new scheme for storing a planar graph in external memory so that any online path can be traversed in an I-O efficient way. Our storage scheme significantly improves the previous results for planar graphs with bounded face size. We also prove an upper bound on I-O efficiency of any storage scheme for well-shaped triangulated meshes. For these meshes, our storage scheme achieves optimal performance.

The paper presents an extension μHDC of Higher-order Duration Calculus (HDC,[ZGZ99]) by a polyadic least fixed point (μ) operator and a class of non-logical symbols with a finite variability restriction on their interpretations, which classifies these symbols as intermediate between rigid symbols and flexible symbols as known in DC. The μ operator and the new kind of symbols enable straightforward specification of recursion and data manipulation by HDC. The paper contains a completeness theorem about an extension of the proof system for HDC by axioms about μ and symbols of finite variability for a class of simple μHDC formulas. The completeness theorem is proved by the method of local elimination of the extending operator μ, which was earlier used for a similar purpose in [Gue98].

In this paper we present a complete proof system for timed automata. It extends our previous axiomatisation of timed bisimulation for the class of loop-free timed automata with unique fixpoint induction. To our knowledge, this is the first algebraic theory for the whole class of timed automata with a completeness result, thus fills a gap in the theory of timed automata. The proof of the completeness result relies on the notion of symbolic timed bisimulation, adapted from the work on value-passing processes.

In this paper, we investigate a text sparsification technique based on the identification of local maxima. In particular, we first show that looking for an order of the alphabet symbols that minimizes the number of local maxima in a given string is an Np-hard problem. Successively, we describe how the local maxima sparsification technique can be used to filter the access to unstructured texts. Finally, we experimentally show that this approach can be successfully used in order to create a space efficient index for searching a DNA sequence as quickly as a full index.

Let a text string T of n symbols and a pattern string P of m symbols from alphabet ∑ be given. A swapped version P′ of P is a length m string derived from P by a series of local swaps, (i.e. p′_ℓ← p_ℓ+1 and p_′ℓ+1 ← p_ℓ) where each element can participate in no more than oneswap. The Pattern Matching with Swaps problem is that of finding all locations i of T for which there exists a swapped version P′ of P with an exact matching of P′ in location i of T.Recently, some efficient algorithms were developed for this problem. Their time complexity is better than the best known algorithms for pattern matching with mismatches. However, the Approximate PatternMatching with Swaps problem was not known to be solved faster than the pattern matching with mismatches problem.In the Approximate Pattern Matching with Swaps problem the output is, for every text location i where there is a swapped match of P, the number of swaps necessary to create the swapped version that matches location i. The fastest known method to-date is that of counting mismatches and dividing by two. The time complexity of this method is $$ O(n\sqrt {m\log m} )$$ for a general alphabet ∑.In this paper we show an algorithm that counts the number of swaps at every location where there is a swapped matching in time O(n log m log σ), where σ = min(m, ∣∑∣). Consequently, the total time for solving the approximate pattern matching with swaps problem is O(f(n,m) +n log m log σ), where f(n,m) is the time necessary for solving the pattern matching with swaps problem.

This paper extends DeNicola and Hennessy’s testing theory from labeled transition system to Büchi processes and establishes a tight connection between the resulting Büchi must-preorder and satisfaction of linear-time temporal logic (LTL) formulas. An example dealing with the design of a communications protocol testifies to the utility of the theory for heterogeneous system design, in which some components are specified as labeled transition systems and others are given as LTL formulas.

This paper presents the first formal verification of the Ricart- Agrawala algorithm [RA81] for distributed mutual exclusion of an arbitrary number of nodes. It uses the Temporal Methodology of [MP95a]. We establish both the safety property of mutual exclusion and the liveness property of accessibility. To establish these properties for an arbitrary number of nodes, parameterized proof rules are used as presented in [MP95a] (for safety) and [MP94] (for liveness). A new and efficient notation is introduced to facilitate the presentation of liveness proofs by verification diagrams.The proofs were carried out using the Stanford Temporal Prover (STeP) [BBC+95], a software package that supports formal verification of temporal specifications of concurrent and reactive systems.

We consider a weak version of pseudorandom function generators and show that their existence is equivalent to the non-learnability of Boolean circuits in Valiant’s pac-learning model with membership queries on the uniform distribution. Furthermore, we show that this equivalence holds still for the case of non-adaptive membership queries and for any (non-trivial) p-samplable distribution.

In this paper we present an approach for proving Θp_in2sup-completeness. There are several papers in which different problems of logic, of combinatorics, and of approximation are stated to be complete for parallel access to NP, i.e.Θp_in2sup-complete.There is a special acceptance concept for nondeterministic Turing machines which allows a characterization of Θp_in2supas a polynomial-time bounded class.This characterization is the starting point of this paper. It makes a master reduction from that type of Turing machines to suitable boolean formula problems possible. From the reductions we deduce a couple of conditions that are sufficient for proving Θp_in2sup-hardness. These new conditions are applicable in a canonical way. Thus we are able to do the following: (i) we can prove the Θp_in2supfor different combinatorial problems (e.g. max-card-clique compare) as well as for optimization problems (e.g. the Kemeny voting scheme), (ii) we can simplify known proofs for Θp_in2sup(e.g. for the Dodgson voting scheme), and (iii) we can transfer this technique for proving Δp_in2sup-completeness (e.g. TSPcompare).

We investigate the question whether there is a (p-)optimal proof system for SAT or for TAUT and its relation to completeness and collapse results for nondeterministic function classes. A p-optimal proof system for SAT is shown to imply (1) that there exists a complete function for the class of all total nondeterministic multi-valued functions and (2) that any set with an optimal proof system has a p-optimal proof system. By replacingthe assumption of the mere existence of a (p-) optimal proof system by the assumption that certain proof systems are (p-)optimal we obtain stronger consequences, namely collapse results for various function classes. Especially we investigate the question whether the standard proof system for SAT is p-optimal. We show that this assumption is equivalent to a variety of complexity theoretical assertions studied before, and to the assumption that every optimal proof system is p-optimal. Finally, we investigate whether there is an optimal proof system for TAUT that admits an effective interpolation, and show some relations between various completeness assumptions.

A general framework for typing graph rewriting systems is presented: the idea is to statically derive a type graph from a given graph. In contrast to the original graph, the type graph is invariant under reduction, but still contains meaningful behaviour information. We present conditions, a type system for graph rewriting should satisfy, and a methodology for proving these conditions. In two case studies it is shown how to incorporate existing type systems (for the polyadic π-calculus and for a concurrent object-oriented calculus) into the general framework.

The definition of open bisimilarity on the x-processes does not give rise to a sensible relation on the x-processes with the mismatch operator. The paper proposes ground open congruence as a principal open congruence on the x-processes with the mismatch operator. The algebraic properties of the ground congruence is studied. The paper also takes a close look at barbed congruence. This relation is similar to the ground congruence. The precise relationship between the two is worked out. It is pointed out that the sound and complete system for the ground congruence can be obtained by removing one tau law from the complete system for the barbed congruence.

We propose an object-oriented calculus with internal concurrency and class-based inheritance that is built upon the join calculus. Method calls, locks, and states are handled in a uniform manner, using labeled messages. Classes are partial message definitions that can be combined and transformed. We design operators for behavioral and synchronization inheritance. Our model is compatible with the JoCaml implementation of the join calculus.

The problem we consider is motivated by allocating bandwidth slots to communication requests on a satellite channel under real time constraints. Accepted requests must be scheduled on non-intersecting rectangles in the time/bandwidth Cartesian space with the goal of maximizing the benefit obtained from accepted requests. This problem turns out to be equal to the maximization version of the well known Dynamic Storage Allocation problem when storage size is limited and requests must be accommodated within a prescribed time interval.We present constant approximation algorithms for the problem introduced in this paper using as a basic step the solution of a fractional Linear Programming formulation.This problem has been independently studied by Bar-Noy et al [BNBYF+00] with different techniques. Our approach gives an improved approximation ratio for the problem.

For the classic dynamic storage/spectrum allocation problem, we show that knowledge of the durations of the requests is of no great use to an online algorithm in the worst case. This answers an open question posed by Naor, Orda, and Petruschka [9]. More precisely, we show that the competitive ratio of every randomized algorithm against an oblivious adversary is Ω(log x/log log x ), where x may be any of several different parameters used in the literature. It is known that First Fit, which does not require knowledge of the durations of the task, is logarithmically competitive in these parameters.

We study models of the untyped lambda calculus in the setting of game semantics. In particular, we show that, in the category of games G, introduced by Abramsky, Jagadeesan and Malacaria, all categorical α-models can be partitioned in three disjoint classes, and each model in a class induces the same theory (i.e. the set of equations between terms), that are the theory H., the theory which identifies two terms if they have the same Böhm tree and the theory which identifies all the terms which have the same Lévy-Longo tree.

Typed symmetric α-calculus is a simple computational interpretation of classical logic with an involutive negation. Its main distinguishing feature is to be a true non-confluent computational interpretation of classical logic. Its non-confluence reflects the computational freedom of classical logic (as compared to intuitionistic logic). Barbanera and Berardi proved in [1],[2] that first order typed symmetric α-calculus enjoys the strong normalization property and showed in [3] that it can be used to derive symmetric programs.In this paper we prove strong normalization for second order typed symmetric α-calculus.

We propose a polynomial time approximation scheme for scheduling a set of dedicated tasks on a constant number m of processors in order to minimize the sum of completion times $$ Pm\left| {fix_j } \right|\sum {C_j } $$ . In addition we give a polynomial time approximation scheme for the weighted preemptive problem with release dates, $$ Pm\left| {fix_j pmtn,r_j } \right|\sum {w_j C_j } $$ .

Evidence indicates that members of many gene families in the genome of an organism tend to have homologues both within their own genome and in the genomes of other organisms. Amongst these homologues, typically only one or a few per genome perform an analogous function in their genome. Finding subsets of these genes which show evidence of performing a common function is an important first step towards, for instance, the creation of phylogenetic trees, multiple sequence alignments and secondary structure predictions. Given a collection of taxa P = P₁...P₂......,P_k where P_i contains genes p _i, 1...p_i, 2......,p_i,n _i, we ask to choose one gene from each of the taxa P _i such that these chosen vertices most agree We define most agreeing in three distinct ways:most tree-like,pairwise closest,and pairwise most similar. We show these problems to be computationally hard from almost every angle via classical,parameterized and approximation complexity theory. However,on the positive side,we give randomized approximation algorithms following ideas from [GGR98]for the srpairwise closest and pairwise most similar variants.

In this paper we present a solution to the ‘Latest Gossip Problem’ for a shared memory distributed system. The Latest Gossip Problem is essentially one of bounded timestamping in which processes must locally keep track of the ‘latest’ information, direct or indirect, about all other processes. A solution to the Latest Gossip Problem is fundamental to the understanding of information flow in a distributed computation, and has applications to problems such as global state detection and mutual exclusion. Our solution is along the lines of that for message passing systems in [6], and for synchronously communicating systems [8].Our algorithm uses a modified version of the consume and update protocols of Dwork and Waarts [3], where these were introduced to construct a ‘Bounded Concurrent Timestamping System (BCTS)’. As applications of our Gossip Protocol, we also indicate another construction of a BCTS and a solution to the global state detection problem, which, we believe, are improvements over older solutions.

Vector and matrix clocks are exte sively used i asy chroous distributed systems.This paper asks,“how does the clock abstractio generalize?” and casts the problem in terms of concurrent knowledge. To this end, the paper motivates and proposes logical clocks of arbitrary dimensions. It then identifies and explores the conceptual link betwee such clocks and knowledge. It establishes the necessary and sufficient conditions on the size and dimension of clocks required to declare k -level concurrent knowledge about the most recent global facts for which this is possible without using control messages. It the gives algorithms to compute the latest global fact about which a specified level of knowledge is attainable in a given state, and to compute the earliest state in which a specified level of knowledge about a given global fact is attainable.

We introduce a strict hierarchy $$ \{ \mathbb{L}_n^\mathcal{B} \} $$ of language classes which exhausts the class of starfree regular languages. It is shown for all n ≥ 0 that the classes $$ \mathbb{L}_n^\mathcal{B} $$ have decidable membership problems. As the main result, we prove that our hierarchy is levelwise comparable by inclusion to the dot-depth hierarchy, more precisely, $$ \mathbb{L}_n^\mathcal{B} $$ contains all languages having dot-depth n +1...2. This yields a lower bound algorithm for the dot-depth of a given language. The same results hold for a hierarchy $$ \left\{ {\mathbb{L}_n^\mathcal{L} } \right\}$$ and the Straubing-Thérien hierarchy.

Church-Rosser languages are mainly based on confluent length reducing string rewriting systems. In general, the prefix language of a Church-Rosser language may not be describable by such a system, too. In this paper it is shown that under certain conditions it is possible to give a construction for a system defining the prefix language and to prove its correctness. The construction also gives a completion of prefixes to full words in the original language. This is an interesting property for practical applications, as it shows potential for error recovery strategies in parsers.