Foundations of Software Technology and Theoretical Computer Science

Descriptive Complexity [I98] is an approach to complexity that measures the richness of a language or sentence needed to describe a given property. There is a profound relationship between the traditional computational complexity of a problem and the descriptive complexity of the problem. In this setting, the finite object being worked on is treated as a logical structure. Thus descriptive complexity is part of finite model theory [EF95].

Let G=(V,E) be a complete undirected graph with vertex set V, edge set E, and edge weights l(e) satisfying triangle inequality. The vertex set V is partitioned into clustersV₁, ..., V _k . The clustered traveling salesman problem (CTSP) is to compute a shortest Hamiltonian cycle (tour) that visits all the vertices, and in which the vertices of each cluster are visited consecutively. Since this problem is a generalization of the traveling salesman problem, it is NP-hard. In this paper, we consider several variants of this basic problem and provide polynomial time approximation algorithms for them.

The problem of Radio Labelling is to assign distinct integer labels to all the vertices of a graph, such that adjacent vertices get labels at distance at least two. The objective is to minimize the label span. Radio labelling is a combinatorial model for frequency assignment in case that the transmitters are not allowed to operate at the same channel.We show that radio labelling is related to TSP(1,2). Hence, it is ${\cal NP}$-complete and MAX-SNP-hard. Then, we present a polynomial-time algorithm for computing an optimal radio labelling, given a coloring of the graph with constant number of colors. Thus, we prove that radio labelling is in ${\cal P}$ for planar graphs. We also obtain a $\frac{3}{2}$-approximation ${\cal NC}$ algorithm and we prove that approximating radio labelling in graphs of bounded maximum degree is essentially as hard as in general graphs.We obtain similar results for TSP(1,2). In particular, we present the first $\frac{3}{2}$-approximation ${\cal NC}$ algorithm for TSP(1,2), and we prove that dense instances of TSP(1,2) do not admit a PTAS, unless ${\cal P}= {\cal NP}$.

We define a new type system for lambda calculi with resources which characterizes the flat operational semantics that distinguishes deadlock from divergence. The system follows the intersection style but with a special management of structural rules. The novel feature in comparison with previous works is the introduction of a controlled form of weakening that allows to deal with deadlock. To show the adequacy result we apply the realizability technique on a decorated calculus where the resources to be consumed are explicitly indicated.

This paper is about the encoding of pπ, the polyadic π-calculus, in mπ, the monadic π-calculus. A type system for mπ processes is introduced which captures the interaction regime underlying the encoding of pπ processes respecting a sorting. A full-abstraction result is shown: two pπ processes are typed barbed congruent iff their mπ encodings are monadic-typed barbed congruent.

In this paper we study the Steiner tree problem in graphs for the case when vertices as well as edges have weights associated with them. A greedy approximation algorithm based on “spider decompositions” was developed by Klein and Ravi for this problem. This algorithm provides a worst case approximation ratio of 2 ln k, where k is the number of terminals. However, the best known lower bound on the approximation ratio is (1 − o(1))ln k, assuming that $NP \not\subseteq DTIME[n^{O(\log \log n)}]$, by a reduction from set cover.We show that for the unweighted case we can obtain an approximation factor of ln k. For the weighted case we develop a new decomposition theorem, and generalize the notion of “spiders” to “branch-spiders”, that are used to design a new algorithm with a worst case approximation factor of 1.5 ln k. We then generalize the method to yield an approximation factor of (1.35 + ε) ln k, for any constant ε> 0. These algorithms, although polynomial, are not very practical due to their high running time; since we need to repeatedly find many minimum weight matchings in each iteration. We also develop a simple greedy algorithm that is practical and has a worst case approximation factor of 1.6103 ln k. The techniques developed for this algorithm imply a method of approximating node weighted network design problems defined by 0-1 proper functions as well.These new ideas also lead to improved approximation guarantees for the problem of finding a minimum node weighted connected dominating set. The previous best approximation guarantee for this problem was 3 ln n due to Guha and Khuller. By a direct application of the methods developed in this paper we are able to develop an algorithm with an approximation factor of (1.35 + ε) ln n for any fixed ε> 0.

We address the problem of I/O scheduling of read-once reference strings in a multiple-disk parallel I/O system. We present a novel on-line algorithm, Red-Black Prefetching (RBP), for parallel I/O scheduling. In order to perform accurate prefetching RBP uses L-block lookahead. The performance of RBP is analyzed in the standard parallel disk model with D independent disks and a shared I/O buffer of size M. We show that the number of parallel I/Os performed by RBP is within a factot $\Theta(\max \{\sqrt{MD/L}, D^{1/3}\})$ of the number of I/Os done by the optimal off-line algorithm. This ratio is within a canstant factor of the best possible when L is L=O(MD1/3).

Synchronous languages are well suited for the design of dependable real-time systems: they enable a very high-level specification and an extremely modular implementation of complex systems by structurally decomposing them into elementary synchronous processes. To maximize the support for the generic implementation and the dynamic reconfigurability of reactive systems, we introduce a semantics of higher-order processes in a seamless extension of the synchronous language SIGNAL. To enable the correct specification and the modular implementation of systems, we introduce an expressive type inference system for characterizing their temporal and causal invariants.

We study testing preorders for an asynchronous version of CCS called TACCS, where message emission is non blocking. We first give a labelled transition system semantics for this language, which includes both external and internal choice operators. By applying the standard definitions of may and must testing to this semantics we obtain two behavioural preorders based on asynchronous observations, $\mathbin{\mathbin{\raisebox{-.65ex}{\raisebox{.97ex}{\(\sqsubset\)} \(\!\!\!\!\!\sim\)}}_{may}}$ and $\mathbin{\mathbin{\raisebox{-.65ex}{\raisebox{.97ex}{\(\sqsubset\)} \(\!\!\!\!\!\sim\)}}_{must}}$. We present alternative behavioural characterisations of these preorders, which are subsequently used to obtain equational theories for the finite fragment of the language.

Molecular Computation (MC) is massively parallel computation where data is stored and processed within objects of molecular size. Biomolecular Computation (BMC) is MC using biotechnology techniques, e.g. recombinant DNA operations. In contrast, Quantum Computation (QC) is a type of computation where unitary and measurement operations are executed on linear superpositions of classical states. Both BMC and QC may be executed at the micromolecular scale by a variety of methodologies and technologies. This paper surveys various methods for doing BMC and QC and discusses the considerable theoretical and practical advances in BMC and QC made in the last few years. We compare bounds on key resource such as time, volume (number of molecules times molecular density), energy and error rates achievable, taking particular note of the scalability of these methods with the size of the problem solved. In addition to NP search problems and database search problems, we enumerate a wide variety of further potential practical applications of BMC and QC. We observe that certain problems if solved with polynomial time bounds appear to require exponentially large volume for BMC (e.g., NP search problems) and QC (e.g., the observation operation). We discuss techniques for decreasing errors in BMC (e.g., annealing errors) and QC (e.g., decoherence errors), and volume where possible, to insure the scalability of BMC and QC to problems of large input size. In addition, we consider how BMC might be used to assist QC (e.g., to do observation operations for Bulk QC) and also how quantum techniques might be used to assist BMC (e.g., to do exquisite detection of very small quantities of a molecule in solution within a large volume).

We propose a construction that augments the precomputation step of a regular tree pattern matching algorithm to include cost analysis. The matching device generated is a pushdown automaton in contrast with the conventionally generated tree pattern matching automaton. Our technique can handle a larger class of cost augmented regular tree grammars than can be preprocessed by conventional methods, and has been tested on some input problem instances representing instruction sets for processors.

We deal with matching and locating of patterns in forests of variable arity. A pattern consists of a structural and a contextual condition for subtrees of a forest, both of which are given as tree or forest regular languages. We use the notation of constraint systems to uniformly specify both kinds of conditions. In order to implement pattern matching we introduce the class of pushdown forest automata. We identify a special class of contexts such that not only pattern matching but also locating all of a forest’s subtrees matching in context can be performed in a single traversal. We also give a method for computing the reachable states of an automaton in order to minimize the size of transition tables.

We present a technique to prevent the construction of intermediate data structures in functional programs, which is based on results from the theory of tree transducers. We first decompose function definitions, which correspond to macro tree transducers, into smaller pieces. Under certain restrictions these pieces can be composed to an attributed tree transducer using a composition result for attribute grammars. The same construction can be used to compose the attributed tree transducers, which represent the initial function definitions.

The failure detectors discussed in the literature are either impossible to implement in an asynchronous system, or their exact guarantees have not been discussed. We introduce an infinitely often accurate failure detector which can be implemented in an asynchronous system. We provide one such implementation and show its application to the fault-tolerant server maintenance problem. We also show that some natural timeout based failure detectors implemented on Unix are not sufficient to guarantee infinitely often accuracy.

BRICS is a research centre and international PhD school in theoretical computer science, based at the University of Aarhus, Denmark. The centre has recently become engaged in quantum information processing in cooperation with the Department of Physics, also University of Aarhus.This extended abstract surveys activities at BRICS with special emphasis on the activities in quantum information processing.

We use Martingale inequalities to give a simple and uniform analysis of two families of distributed randomised algorithms for edge colouring graphs.

We first give a representation of a suffix tree that uses $n \lg n + O(n)$ bits of space and supports searching for a pattern in the given text (from a fixed size alphabet) in O(m) time, where n is the size of the text and m is the size of the pattern. The structure is quite simple and answers a question raised by Muthukrishnan in [17]. Previous compact representations of suffix trees had a higher lower order term in space and had some expectation assumption [3], or required more time for searching [5]. Then, surprisingly, we show that we can even do better, by developing a structure that uses a suffix array (and so $n \lceil \lg n \rceil $ bits) and an additional o(n) bits. String searching can be done in this structure also in O(m) time. Besides supporting string searching, we can also report the number of occurrences of the pattern in the same time using no additional space. In this case the space occupied by the structures is much less compared to many of the previously known structures to do this. When the size of the alphabet k is not a constant, our structures can be easily extended, using standard tricks, to those that use the same space but take $O(m \lg k)$ time for string searching or to those that use an additional $O(m \lg k)$ bits but take the same O(m) time for searching.

The verification of concurrent systems with a large number of interacting components poses a significant challenge to the existing verification methodologies. We consider in this paper the formal verification of buffer cache algorithms of SVR3-type Unix systems using PVS.

We introduce three new notions of infinite testing for probabilistic processes, namely, simple, Büchi and fair infinite testing. We carefully examine their distinguishing power and show that all three have the same power as finite tests. We also consider Büchi tests in the non-probabilistic setting and show that they have the same distinguishing power as finite tests. Finally, we show that finite probabilistic tests are stronger than nondeterministic fair tests.

We present a conceptually simple algorithm to generate an ordering of the vertices of an undirected graph. The ordering generated turns out to be a strong elimination ordering if and only if the given graph is a strongly chordal graph. This algorithm makes use of maximum cardinality search and lexicographic breadth first search algorithms which are used to generate perfect elimination orderings of a chordal graph. Our algorithm takes O(k2n) time where k is the size of the largest minimal vertex separator and n denotes the number vertices in the graph. The algorithm provides a new insight into the structure of strongly chordal graphs and also gives rise to a new algorithm of the same time complexity for recognition of strongly chordal graphs.

We show a parallel algorithm that produces a triangulation which is within a constant factor longer than the Minimum Weight Triangulation (MWT) in time O(logn) using O(n) processors and linear space in the CRCW PRAM model. This is done by developing a relaxed version of the quasi-greedy triangulation algorithm. The relaxed version produces edges that are at most (1+ε) longer than the shortest diagonal, where ε is some positive constant smaller than 1, still outputs a triangulation which is within a constant factor longer that the minimum weight triangulation. However, if the same method is applied to the straight-forward greedy algorithm the approximation behavior may deteriorate dramatically, i.e. Ω(n) longer than a minimum weight triangulation, if the lengths of the edges are not computed with high precision.

In this paper we provide a complete characterization of the class of properties of (networks of) timed automata for which model checking can be reduced to reachability checking in the context of testing automata.

The Mean-Value Calculus, MVC, of Zhou and Li [19] is extended with the least and the greatest fixed point operators. The resulting logic is called μMVC. Timed behaviours with naturally recursive structure can be elegantly specified in this logic. Some examples of such usage are given. The expressive power of the logic is also studied. It is shown that the propositional fragment of the logic, even with discrete time, is powerful enough to encode the computations of nondeterministic turing machines. Hence, the satisfiability of propositional μMVC over both dense and discrete times is undecidedable.

Model checking is emerging as a practical tool for detecting logical errors in early stages of system design. We investigate the model checking of hierarchical (nested) systems, i.e. finite state machines whose states themselves can be other machines. This nesting ability is common in various software design methodologies and is available in several commercial modeling tools. The straightforward way to analyze a hierarchical machine is to flatten it (thus, incurring an exponential blow up) and apply a model checking tool on the resulting ordinary FSM.

Model checking is an automated technique for verifying temporal properties of finite-state systems. The technique can be used, for example, to verify the finite control parts of computer hardware designs and communication protocols. However, because it requires exhaustively searching the state space of a system to be verified, it cannot generally be applied directly to systems manipulating data, even if the data types are finite. For unbounded or uninterpreted data types, the model checking problem becomes undecidable.Nonetheless, reductions akin to “program slicing” can be used to reduce the verification of large systems with unbounded data to model checking problems over tractably small models with finite data types. Such a reduction can be obtained, for example, by enumerating the possible paths of a data item through a system. Symmetry can then be exploited to reduce the cases to a tractable number. Use of model checking in this way can greatly simplify proofs by eliminating the need for global invariants.This talk will show how a system of three inference rules – circular assume/guarantee, temporal case splitting, and symmetry reduction – can be used in conjunction with model checking to yield quite concise proofs of systems that manipulate data.

Partial order methods have been introduced to avoid the state explosion problem in verification resulting from the representation of multiple interleavings of concurrent transitions. The basic idea is to build a reduced state space on which certain properties hold if and only if they hold for the full state space. Most often, the considered properties are linear-time properties. In this paper we suggest novel branching time reduction techniques which allow checking bisimulation equivalence on reduced state spaces. Our reduction takes place on bisimulation game graphs, thus jointly treating the systems under consideration. We show that reduction preserves winning strategies of the two players in the bisimulation game.

This work presents a first-order model checking procedure that verifies systems with large or even infinite data spaces with respect to first-order CTL specifications. The procedure relies on a partition of the system variables into control and data. While control values are expanded into BDD-representations, data values enter in form of their properties relevant to the verification task. The algorithm is completely automatic. If the algorithm terminates, it has generated a first-order verification condition on the data space which characterizes the system’s correctness. Termination can be guaranteed for a class that properly includes the data-independent systems, defined in [10].This work improves [5], where we extended explicit model checking algorithms. Here, both the control part and the first-order conditions are represented by BDDs, providing the full power of symbolic model checking for control aspects of the design.

We consider the problem of deciding whether a given graph G has an automorphism which moves at least k vertices (where k is a function of ∣ V(G) ∣), a question originally posed by Lubiw (1981). Here we show that this problem is equivalent to the one of deciding whether a graph has a nontrivial automorphism, for k ∈ O(logn / loglogn ).It is commonly believed that deciding isomorphism between two graphs is strictly harder than deciding whether a graph has a nontrivial automorphism. Indeed, we show that an isomorphism oracle would improve the above result slightly–using such an oracle, one can decide whether there is an automorphism which moves at least k′ vertices, where k′ ∈ O(logn).If P $\ne$ NP and Graph Isomorphism is not NP-complete, the above results are fairly tight, since it is known that deciding if there is an automorphism which moves at least nε vertices, for any fixed ε ∈ (0, 1) , is NP-complete. In other words, a substantial improvement of our result would settle some fundamental open problems about Graph Isomorphism.

We revisit the notion of graph complexity introduced by Pudlák, Rödl, and Savický [PRS]. Using their framework, we show that sufficiently strong superlinear monotone lower bounds for the very special class of 2-slice functions would imply superpolynomial lower bounds for some other functions. Given an n-vertex graph G, the corresponding 2-slice function f _G on n variables evaluates to zero on inputs with less than two 1’s and evaluates to one on inputs with more than two 1’s. On inputs with exactly two 1’s, f _G evaluates to 1 exactly when the pair of variables set to 1 corresponds to an edge in G. Combining our observations with those from [PRS], we can show, for instance, that a lower bound of n1 + Ω(1) on the (monotone) formula size of an explicit 2-slice function f on n variables would imply a 2Ω(l) lower bound on the formula size of another explicit function g on l variables, where $l={\it \Theta}(\log n)$.We consider lower bound questions for depth-3 bipartite graph complexity. We prove some weak lower bounds on this measure using algebraic methods. For instance, our results give a lower bound of Ω((logn/ loglogn)2) for bipartite graphs arising from Hadamard matrices, such as the Paley-type bipartite graphs. A lower bound of nΩ(1) on the depth-3 complexity of an explicit bipartite graph would give superlinear size lower bounds on log-depth boolean circuits for an explicit function. Similarly, a lower bound of $2^{(\log n)^{\Omega(1)}}$ would give an explicit language outside the class $\Sigma_{\rm 2}^{cc}$ of the two-party communication complexity.

In [NO88], a particular trace monoid M is constructed such that for the class of length-reducing trace rewriting systems over M, confluence is undecidable. In this paper, we show that this result holds for every trace monoid, which is neither free nor free commutative. Furthermore we will present a new criterion for trace rewriting systems that implies decidability of confluence.

This paper introduces Thue specifications, an approach for string-rewriting description of infinite graphs. It is shown that strongly reduction-bounded and unitary reduction-bounded rational Thue specifications have the same expressive power and both characterize the context-free graphs of Muller and Schupp. The problem of strong reduction-boundedness for rational Thue specifications is shown to be undecidable but the class of unitary reduction-bounded rational Thue specifications, that is a proper subclass of strongly reduction-bounded rational Thue specifications, is shown to be recursive.

We consider several classes of rewriting automata with a restart operation and the monotonicity property of computations by such automata. It leads to three natural definitions of (right) monotonicity of automata. Besides the former monotonicity, two new types, namely a-monotonicity and g-monotonicity, for such automata are introduced. We provide a taxonomy of the relevant language classes, and answer the (un)decidability questions concerning these properties.

This paper extends automata-theoretic techniques to unbounded parallel behaviour, as seen for instance in Petri nets. Languages are defined to be sets of (labelled) series-parallel posets – or, equivalently, sets of terms in an algebra with two product operations: sequential and parallel. In an earlier paper, we restricted ourselves to languages of posets having bounded width and introduced a notion of branching automaton. In this paper, we drop the restriction to bounded width. We define rational expressions, a natural generalization of the usual ones over words, and prove a Kleene theorem connecting them to regular languages (accepted by finite branching automata). We also show that recognizable languages (inverse images by a morphism into a finite algebra) are strictly weaker.

Quantum computation is a fascinating new area that touches upon the foundations of both quantum physics and computer science. Quantum computers can perform certain tasks, such as factoring, exponentially faster than classical computers. This talk will describe the principles underlying the fundamental quantum algorithms.The power of quantum computation lies in the exponentially many hidden degrees of freedom in the state of an n quantum bit system – whereas 2n – 1 complex numbers are necessary to specify the state, Holevo’s theorem states that n quantum bits cannot be used to communicate any more than n classical bits. Nevertheless, there are communication tasks in which these hidden degrees of freedom can be tapped into.Finally, the state of a quantum system is particularly fragile to noise and decoherence. However, there are beautiful techniques – quantum error-correcting codes – for protecting a given quantum state (with its exponentially many degrees of freedom) against noise and decoherence. These codes can be used to create fault-tolerant quantum circuits – which are immune to a constant rate of decoherence.