Automata, Languages and Programming

The basic polarized process algebra is completed yielding as a projective limit a cpo which also comprises infinite processes. It is shown that this model serves in a natural way as a semantics for several program algebras. In particular, the fully abstract model of the program algebra axioms of [2] is considered which results by working modulo behavioral congruence. This algebra is extended with a new basic instruction, named ‘entry instruction’ and denoted with ‘@’. Addition of @ allows many more equations and conditional equations to be stated. It becomes possible to find an axiomatization of program inequality. Technically this axiomatization is an infinite final algebra specification using conditional equations and auxiliary objects.

We describe several computational problems on prediction and design of RNA molecules.

In this survey talk we discuss several problems related to peer to peer networks. A host of issues arises in the context of peer to peer networks, including efficiency issues, censorship issues, anonymity issues, etc. While many of these problems have been studied in the past, the file swapping application has taken over the Internet, given these problems renewed impetus. I will discuss papers co-authored with J. Saia, E. Cohen, H. Kaplan, R. Berman, A. Ta-Sham, and others.

The data structure SPQR-tree represents the decomposition of a biconnected graph with respect to its triconnected components. SPQR-trees have been introduced by Di Battista and Tamassia [13] based on ideas by Bienstock and Monma [[9], [10]]. For planar graphs, SPQR-trees have the nice property to represent the set of all its combinatorial embeddings. Therefore, the data structure has mainly (but not only) been used in the area of planar graph algorithms and graph layout.The techniques are quite manifold, reaching from special purpose algorithms that merge the solutions of the triconnected components in a clever way to a solution of the original graph, to general branch-and-bound techniques and integer linear programming techniques. Applications reach from Steiner tree problems, to on-line problems in a dynamic setting as well as problems concerned with planarity and graph drawing. This paper gives a survey on the use of SPQR-trees in graph algorithms, with a focus on graph drawing.

Model checking is a technique for automatically checking properties of models of systems. We present here several combinations of model checking with testing techniques. This allows checking systems when no model is given, when the model is inaccurate, or when only a part of its description is given.

There are non-context-free languages which are recognizable by randomized pushdown automata even with arbitrarily small error probability. We give an example of a context-free language which cannot be recognized by a randomized pda with error probability smaller than $$ \frac{1} {2} - O\left( {\frac{{\log _2 n}} {n}} \right) $$ for input size n. Hence nondeterminism can be stronger than probabilism with weakly-unbounded error.Moreover, we construct two deterministic context-free languages whose union cannot be accepted with error probability smaller than 1/3 − 2−Ω(n), where n is the input length. Since the union of any two deterministic context-free languages can be accepted with error probability 1/3, this shows that 1/3 is a sharp threshold and hence randomized pushdown automata do not have amplification.One-way two-counter machines represent a universal model of computation. Here we consider the polynomial-time classes of multicounter machines with a constant number of reversals and separate the computational power of nondeterminism, randomization and determinism.

Group Testing refers to the situation in which one is given a set of objects $$ \mathcal{O} $$, an unknown subset $$ \mathcal{P} \subseteq \mathcal{O} $$, and the task is to determine $$ \mathcal{P} $$ by asking queries of the type “does $$ \mathcal{P} $$ intersect $$ \mathcal{Q} $$?”, where $$ \mathcal{Q} $$ is a subset of $$ \mathcal{O} $$. Group testing is a basic search paradigm that occurs in a variety of situations such as quality control in product testing, searching in storage systems, multiple access communications, and software testing, among the others. Group testing procedures have been recently applied in Computational Molecular Biology, where they are used for screening library of clones with hybridization probes and sequencing by hybridization.Motivated by particular features of group testing algorithms used in biological screening, we study the efficiency of two-stage group testing procedures. Our main result is the first optimal two-stage algorithm that uses a number of tests of the same order as the information theoretic lower bound on the problem. We also provide efficient algorithms for the case in which there is a Bernoulli probability distribution on the possible sets $$ \mathcal{P} $$, and an optimal algorithm for the case in which the outcome of tests may be unreliable because of the presence of “inhibitory” items in $$ \mathcal{O} $$. Our results depend on a combinatorial structure introduced in this paper. We believe that it will prove useful in other contexts too.

We consider error-correction over the Non-Binary Symmetric Channel (NBSC) which is a natural probabilistic extension of the Binary Symmetric Channel (BSC). We propose a new decoding algorithm for interleaved Reed-Solomon Codes that attempts to correct all “interleaved” codewords simultaneously. In particular, interleaved encoding gives rise to multi-dimensional curves and more specifically to a variation of the Polynomial Reconstruction Problem, which we call Simultaneous Polynomial Reconstruction. We present and analyze a novel probabilistic algorithm that solves this problem. Our construction yields a decoding algorithm for interleaved RS-codes that allows efficient transmission arbitrarily close to the channel capacity in the NBSC model.

We provide an answer to an open question, posed by van Glabbeek [4], regarding the axiomatizability of ready trace semantics. We prove that if the alphabet of actions is finite, then there exists a (sound and complete) finite equational axiomatization for the process algebra BCCSP modulo ready trace semantics. We prove that if the alphabet is infinite, then such an axiomatization does not exist. Furthermore, we present finite equational axiomatizations for BCCSP modulo ready simulation and failure trace semantics, for arbitrary sets of actions.

μKlaim is a process language that permits programming distributed systems made up of several mobile components interacting through multiple distributed tuple spaces. We present the language and a type system for controlling the activities, e.g. access to resources and mobility, of the processes in a net. By dealing with privileges acquisition, the type system enables dynamic variations of security policies. We exploit a combination of static and dynamic type checking, and of in-lined reference monitoring, to guarantee absence of run-time errors due to lack of privileges and state two type soundness results: one involves whole nets, the other is relative to subnets of larger nets.

We investigate the expressive power of two alternative approaches used to express infinite behaviours in process calculi, namely, replication and recursive definitions. These two approaches are equivalent in the full π-calculus, while there is a common agreement that this is not the case when name mobility is not allowed (as in the case of CCS), even if no formal discriminating results have been proved so far.We consider a hierarchy of calculi, previously proposed by Sangiorgi, that spans from a fragment of CCS (named “the core of CCS”) to the π-calculus with internal mobility. We prove the following discrimination result between replication and recursive definitions: the termination of processes is an undecidable property in the core of CCS, provided that recursive process definitions are allowed, while termination turns out to be decidable when only replication is permitted. On the other hand, this discrimination result does not hold any longer when we move to the next calculus in the hierarchy, which supports a very limited form of name mobility.

In this paper we present improved combinatorial approximation algorithms for the k-level facility location problem. First, by modifying the path reduction developed in [2], we obtain a combinatorial algorithm with a performance factor of 3.27 for any k ≥ 2, thus improving the previous bound of 4.56. Then we develop another combinatorial algorithm that has a better performance guarantee and uses the first algorithm as a subroutine. The latter algorithm can be recursively implemented and achieves a guarantee factor h(k), where h(k) is strictly less than 3.27 for any k and tends to 3.27 as k goes to δ. The values of h(k) can be easily computed with an arbitrary accuracy: h(2) ≈ 2.4211, h(3) ≈ 2.8446, h(4) ≈ 3.0565, h(5) ≈ 3.1678 and so on. Thus, for the cases of k = 2 and k = 3 the second combinatorial algorithm ensures an approximation factor significantly better than 3, which is currently the best approximation ratio for the k-level problem provided by the non-combinatorial algorithm due to Aardal, Chudak, and Shmoys [1].

We consider the asymmetric traveling salesperson problem with γ-parameterized triangle inequality for γ ∈ [1/2, 1). That means, the edge weights fulfill w(u, v) ≤ γ · (w(u, x) + w(x, v)) for all nodes u, v, x. Chandran and Ram [6] recently gave the first constant factor approximation algorithm with polynomial running time for this problem. They achieve performance ratio γ/1−γ. We devise an approximation algorithm with performance ratio $$ \frac{1} {{1 - \frac{1} {2}\left( {\gamma + \gamma ^3 } \right)}} $$, which is better than the one by Chandran and Ram for γ ∈ [0.6507, 1), that is, for the particularly interesting large values of γ.

In this paper we study the capacitated vertex cover problem, a generalization of the well-known vertex cover problem. Given a graph G = (V, E), the goal is to cover all the edges by picking a minimum cover using the vertices. When we pick a vertex, we can cover up to a pre-specified number of edges incident on this vertex (its capacity). The problem is clearly NP-hard as it generalizes the well-known vertex cover problem. Previously, 2-approximation algorithms were developed with the assumption that multiple copies of a vertex may be chosen in the cover. If we are allowed to pick at most a given number of copies of each vertex, then the problem is significantly harder to solve. Chuzhoy and Naor (Proc. IEEE Symposium on Foundations of Computer Science, 481–489, 2002) have recently shown that the weighted version of this problem is at least as hard as set cover; they have also developed a 3-approximation algorithm for the unweighted version. We give a 2-approximation algorithm for the unweighted version, improving the Chuzhoy-Naor bound of 3 and matching (up to lower-order terms) the best approximation ratio known for the vertex cover problem.

We develop a quasi-polynomial time approximation scheme for the Euclidean version of the Degree-restricted MST by adapting techniques used previously for approximating TSP. Given n points in the plane, d = 2 or 3, and ∈ > 0, the scheme finds an approximation with cost within 1 + ∈ of the lowest cost spanning tree with the property that all nodes have degree at most d. We also develop a polynomial time approximation scheme for the Euclidean version of the Red-Blue Separation Problem.

We consider the Steiner k-cut problem, which is a common generalization of the k-cut problem and the multiway cut problem: given an edge-weighted undirected graph G = (V,E), a subset of vertices X$$ \subseteq $$V called terminals, and an integer k ≤ |X|, the objective is to find a minimum weight set of edges whose removal results in k disconnected components, each of which contains at least one terminal. We give two approximation algorithms for the problem: a 2 − 2/k-approximation based on Gomory-Hu trees, and a 2 − 2/|X|-approximation based on LP rounding. The latter algorithm is based on rounding a generalization of a linear programming relaxation suggested by Naor and Rabani [8]. The rounding uses the Goemans and Williamson primal-dual algorithm (and analysis) for the Steiner tree problem [4] in an interesting way and differs from the rounding in [8]. We use the insight from the rounding to develop an exact bi-directed formulation for the global minimum cut problem (the k-cut problem with k = 2).

We consider the MAX k-CUT problem in random graphs G_n,p. First, we estimate the probable weight of a MAX k-CUT using probabilistic counting arguments and by analyzing a simple greedy heuristic. Then, we give an algorithm that approximates MAX k-CUT within expected polynomial time. The approximation ratio tends to 1 as np→ ∞. As an application, we obtain an algorithm for approximating the chromatic number of G_n,p, 1/n≤ p ≤ 1/2, within a factor of $$ O\left( {\sqrt {np} } \right) $$ in polynomial expected time, thereby answering a question of Krivelevich and Vu, and extending a result of Coja-Oghlan and Taraz. We give similar algorithms for random regular graphs G_n,r.

Consider a network of processors modeled by an n-vertex directed graph G = (V,E). Assume that the communication in the network is synchronous, i.e., occurs in discrete “rounds”, and in every round every processor is allowed to pick one of its neighbors, and to send him a message. The telephone k-multicast problem requires to compute a schedule with minimal number of rounds that delivers a message from a given single processor, that generates the message, to all the processors of a given set $$ \tau \subseteq V,\left| \tau \right| = k $$. The processors of V \ $$ \tau $$ may be left uninformed. The telephone multicast is a basic primitive in distributed computing and computer communication theory. In this paper we devise an algorithm that constructs a schedule with O(max{log k, log n/log k} • br* + k1/2) rounds for the directed k-multicast problem, where br* is the value of the optimum solution. This significantly improves the previously best-known approximation ratio of O(k1/3 • log n • br* + k2/3) due to [EK03].We show that our algorithm for the directed multicast problem can be used to derive an algorithm with a similar ratio for the directed minimum poise Steiner arborescence problem, that is, the problem of constructing an arborescence that spans a collection $$ \tau $$ of terminals, minimizing the sum of height of the arborescence plus maximum out-degree in the arborescence.

We define a calculus for investigating the interactions between mixin modules and computational effects, by combining the purely functional mixin calculus CMS witha monadic metalanguage supporting the two separate notions of simplification (local rewrite rules) and computation (global evaluation able to modify the store). This distinction is important for smoothly integrating the CMS rules (which are all local) withth e rules dealing withth e imperative features.In our calculus mixins can contain mutually recursive computational components which are explicitly computed by means of a new mixin operator whose semantics is defined in terms of a Haskell-like recursive monadic binding. Since we mainly focus on the operational aspects, we adopt a simple type system like that for Haskell, that does not detect dynamic errors related to bad recursive declarations involving effects. The calculus serves as a formal basis for defining the semantics of imperative programming languages supporting first class mixins while preserving the CMS equational reasoning.

The paper studies resolved systems of language equations that allow the use of all Boolean operations in addition to concatenation. Existence and uniqueness of solutions are shown to be their nontrivial properties, these properties are given characterizations by first order formulae, and the position of the corresponding decision problems in the arithmetical hierarchy is determined. The class of languages defined by components of unique solutions of such systems is shown to coincide with the class of recursive languages.

Since its introduction, more than a decade ago, rewriting logic has attracted the interest of both theorists and practitioners, who have contributed in showing its generality as a semantic and logical framework and also as a programming paradigm. The experimentation conducted in these years has suggested that some significant extensions to the original definition of the logic would be very useful in practice. In particular, the Maude system now supports subsorting and conditions in the equational logic for data, and also frozen arguments to block undesired nested rewritings; moreover, it allows equality and membership assertions in rule conditions. In this paper, we give a detailed presentation of the inference rules, model theory, and completeness of such generalized rewrite theories.

The Kolmogorov structure function divides the smallest program producing a string in two parts: the useful information present in the string, called sophistication if based on total functions, and the remaining accidental information. We revisit the notion of sophistication due to Koppel, formalize a connection between sophistication and a variation of computational depth (intuitively the useful or nonrandom information in a string), prove the existence of strings with maximum sophistication and show that they encode solutions of the halting problem, i.e., they are the deepest of all strings.

Resource-bounded dimension is a complexity-theoretic extension of classical Hausdorff dimension introduced by Lutz (2000) in order to investigate the fractal structure of sets that have resource-bounded measure 0. For example, while it has long been known that the Boolean circuit-size complexity class SIZE(α2n/n) has measure 0 in ESPACE for all 0 ≤ α ≤ 1, we now know that SIZE(α2n/n) has dimension α in ESPACE for all 0 ≤ α ≤ 1. The present paper furthers this program by developing a natural hierarchy of “rescaled” resource-bounded dimensions. For each integer i and each set X of decision problems, we define the ithdimension of X in suitable complexity classes. The 0th-order dimension is precisely the dimension of Hausdorff (1919) and Lutz (2000). Higher and lower orders are useful for various sets X. For example, we prove the following for 0 ≤ α ≤ 1 and any polynomial q(n) ≥ n2. 1.The class SIZE(2αn) and the time- and space-bounded Kolmogorov complexity classes KTq(2αn) and KSq(2αn) have 1st-order dimension α in ESPACE.2.The classes $$ SIZE\left( {2^{n^\alpha } } \right) $$, $$ KT^q \left( {2^{n^\alpha } } \right) $$, and $$ KS^q \left( {2^{n^\alpha } } \right) $$ have 2nd-order dimension α in ESPACE.3.The classes KTq(2n(1 − 2−αn)) and KSq(2n(1 − 2−αn) have −1st-order dimension α in ESPACE.

Suppose we have n algorithms, quantum or classical, each computing some bit-value with bounded error probability. We describe a quantum algorithm that uses O($$ \sqrt n $$) repetitions of the base algorithms and with high probability finds the index of a 1-bit among these n bits (if there is such an index). This shows that it is not necessary to first significantly reduce the error probability in the base algorithms to O(1/poly(n)) (which would require O($$ \sqrt n \log n $$ log n) repetitions in total). Our technique is a recursive interleaving of amplitude amplification and error-reduction, and may be of more general interest. Essentially, it shows that quantum amplitude amplification can be made to work also with a bounded-error verifier. As a corollary we obtain optimal quantum upper bounds of O($$ \sqrt N $$) queries for all constant-depth AND-OR trees on N variables, improving upon earlier upper bounds of O($$ \sqrt N $$ polylog(N)).

We prove lower bounds for the direct sum problem for two-party bounded error randomised multiple-round communication protocols. Our proofs use the notion of information cost of a protocol, as defined by Chakrabarti et al. [CSWY01] and refined further by Bar- Yossef et al. [BJKS02]. Our main technical result is a ‘compression’ theorem saying that, for any probability distribution µ over the inputs, a k-round private coin bounded error protocol for a function f with information cost c can be converted into a k-round deterministic protocol for f with bounded distributional error and communication cost O(kc). We prove this result using a Substate Theorem about relative entropy and a rejection sampling argument. Our direct sum result follows from this ‘compression’ result via elementary information theoretic arguments. We also consider the direct sum problem in quantum communication. Using a probabilistic argument, we show that messages cannot be compressed in this manner even if they carry small information.

We consider the issues of implicitness and cache-obliviousness in the classical dictionary problem for n distinct keys over an unbounded and ordered universe. One finding in this paper is that of closing the longstanding open problem about the existence of an optimal implicit dictionary over an unbounded universe. Another finding is motivated by the antithetic features of implicit and cache-oblivious models in data structures. We show how to blend their best qualities achieving O(log n) time and O(log_Bn) block transfers for searching and for amortized updating, while using just n memory cells like sorted arrays and heaps. As a result, we avoid space wasting and provide fast data access at any level of the memory hierarchy.

We show lower bounds in the cell probe model for the redundancy/query time tradeoff of solutions to static data structure problems.

We investigate the problem of succinctly representing an arbitrary permutation, π, on {0, . . ., n − 1} so that πk(i) can be computed quickly for any i and any (positive or negative integer) power k. A representation taking (1 + ∈)n lg n + O(1) bits suffices to compute arbitrary powers in constant time. A representation taking the optimal ⌈lg n!⌉ + o(n) bits can be used to compute arbitrary powers in O(lg n/lg lg n) time, or indeed in a minimal O(lg n) bit probes.

We consider space-efficient solutions to two dynamic data structuring problems. We first give a representation of a set $$ S \subseteq U = \left\{ {0,...,m - 1} \right\},\left| S \right| = n $$ that supports membership queries in O(1) worst case time and insertions into/deletions from S in O(1) expected amortised time. The representation uses $$ \mathcal{B} + o\left( \mathcal{B} \right) $$ bits, where $$ \mathcal{B} = \left\lceil {\lg \left( \begin{gathered} m \hfill \\ n \hfill \\ \end{gathered} \right)} \right\rceil $$ is the information-theoretic minimum space to represent S. This improves upon the O($$ \left( \mathcal{B} \right) $$)-bit solutions of Brodnik and Munro [2] and Pagh [16], and uses up to a log-factor less space than search trees or hash tables. The representation can also associate satellite data with elements of S.We also show that a binary tree on n nodes, where each node has b = O(lg n)-bit data stored at it, can be maintained under node insertions while supporting navigation in O(1) time and updates in O((lg lg n)1+∈) amortised time, for any constant ∈ > 0. The space used is within o(n) bits of the information-theoretic minimum. This improves upon the equally space-efficient structure of Munro et al. [15], in which updates take O(lgcn) time, for some c ≥ 1.

This paper studies β-approximate distance labeling schemes, which are composed of a marker algorithm for labeling the vertices of a graph with short labels, coupled with a decoder algorithm allowing one to compute a β-approximation of the distance between any two vertices directly from their labels (without using any additional information). As most applications for informative labeling schemes in general, and distance labeling schemes in particular, concern large and dynamically changing networks, it is of interest to focus on distributed dynamic labeling schemes. The paper considers the problem on dynamic weighted trees and cycles where the vertices of the tree (or the cycle) are fixed but the (positive integral) weights of the edges may change. The two models considered are the fully dynamic model, where from time to time some edge changes its weight by a fixed quanta, and the increasing dynamic model in which edge weights can only grow. The paper presents distributed β-approximate distance labeling schemes for the two models, for β > 1, and establishes upper and lower bounds on the required label size and the communication complexity involved in updating the labels following a weight change.

Let G(V,E) be an undirected weighted graph with |V| = n, and |E| = m. A t-spanner of the graph G(V,E) is a sub-graph G(V,E_S) such that the distance between any pair of vertices in the spanner is at most t times the distance between the two in the given graph. A 1963 girth conjecture of Erdős implies that Ω(n1+1/k) edges are required in the worst case for any (2k − 1)-spanner, which has been proved for k = 1, 2, 3, 5. There exist polynomial time algorithms that can construct spanners with the size that matches this conjectured lower bound, and the best known algorithm takes O(mn1/k) expected running time. In this paper, we present an extremely simple linear time randomized algorithm that constructs (2k − 1)-spanner of size matching the conjectured lower bound.Our algorithm requires local information for computing a spanner, and thus can be adapted suitably to obtain efficient distributed and parallel algorithms.

Flow variation over time is an important feature in network flow problems arising in various applications such as road or air traffic control, production systems, communication networks (e.g., the Internet), and financial flows. The common characteristic are networks with capacities and transit times on the arcs which specify the amount of time it takes for flow to travel through a particular arc. Moreover, in contrast to static flow problems, flow values on arcs may change with time in these networks.While the ‘maximum s-t-flow over time’ problem can be solved efficiently and ‘min-cost flows over time’ are known to be NP-hard, the complexity of (fractional) ‘multicommodity flows over time’ has been open for many years. We prove that this problem is NP-hard, even for series-parallel networks, and present new and efficient algorithms under certain assumptions on the transit times or on the network topology. As a result, we can draw a complete picture of the complexity landscape for flow over time problems.

We consider requests for capacity in a given tree network T = (V,E) where each edge of the tree has some integer capacity u_e. Each request consists of an integer demand d_f and a profit w_f which is obtained if the request is satisfied. The objective is to find a set of demands that can be feasibly routed in the tree and which provide a maximum profit. This generalizes well-known problems including the knapsack and b-matching problems.When all demands are 1, we have the integer multicommodity flow problem. Garg, Vazirani, and Yannakakis [5] had shown that this problem is NP-hard and gave a 2-approximation algorithm for the cardinality case (all profits are 1) via a primal-dual algorithm. In this paper we establish for the first time that the natural linear programming relaxation has a constant factor gap, a factor of 4, for the case of arbitrary profits.We then discuss the situation for arbitrary demands. When the maximum demand d_max is at most the minimum edge capacity u_min, we show that the integrality gap of the LP is at most 48. This result is obtained showing that the integrality gap for demand version of such a problem is at most 12 times that for the unit demand case. We use techniques of Kolliopoulos and Stein [8], [9] to obtain this. We also obtain, via this method, improved algorithms for the line and ring networks. Applications and connections to other combinatorial problems are discussed.

We investigate finite-state systems with costs. Departing from classical theory, in this paper the cost of an action does not only depend on the state of the system, but also on the time when it is executed. We first characterize the terminating behaviors of such systems in terms of rational formal power series. This generalizes a classical result of Schützenberger.Using the previous results, we also deal with nonterminating behaviors and their costs. This includes an extension of the Büchi-acceptance condition from finite automata to weighted automata and provides a characterization of these nonterminating behaviors in terms of ω-rational formal power series. This generalizes a classical theorem of Büchi.

Whether there exists an exponential gap between the size of a minimal deterministic two-way automaton and the size of a minimal nondeterministic two-way automaton for a specific regular language is a long standing open problem and surely one of the most challenging problems in automata theory. Twenty four years ago, Sipser [M. Sipser: Lower bounds on the size of sweeping automata. ACM STOC ’79, 360–364] showed an exponential gap between nondeterminism and determinism for the so-called sweeping automata which are automata whose head can reverse direction only at the endmarkers. Sweeping automata can be viewed as a special case of oblivious two-way automata with a number of reversals bounded by a constant.Our first result extends the result of Sipser to general oblivious two-way automata with an unbounded number of reversals. Using this extension we show our second result, namely an exponential gap between determinism and nondeterminism for two-way automata with the degree of non-obliviousness bounded by o(n) for inputs of length n. The degree of non-obliviousness of a two-way automaton is the number of distinct orders in which the tape cells are visited.

A stochastic generalisation of residual languages and operations on Probabilistic Finite Automata (PFA) are studied. When these operations are iteratively applied to a subclass of PFA called PRFA, they lead to a unique canonical form (up to an isomorphism) which can be efficiently computed from any equivalent PRFA representation.

Recently, a large number of equivalences for probabilistic automata has been proposed in the literature. Except for the probabilistic bisimulation of Larsen & Skou, none of these equivalences has been characterized in terms of an intuitive testing scenario. In our view, this is an undesirable situation: in the end, the behavior of an automaton is what an external observer perceives. In this paper, we propose a simple and intuitive testing scenario for probabilistic automata and we prove that the equivalence induced by this scenario coincides with the trace distribution equivalence proposed by Segala.

We introduce new tools allowing to deal with the equality-problem for prefix-free languages. We illustrate our ideas by showing that, for every fixed integer t ≥ 1, the equivalence problem for t-turn deterministic pushdown automata is co-NP. This complexity result refines those of [Val74, Bee76].

Flip-pushdown automata are pushdown automata with the additional power to flip or reverse its pushdown, and were recently introduced by Sarkar [13]. We solve most of Sarkar’s open problems. In particular, we show that k+1 pushdown reversals are better than k for both deterministic and nondeterministic flip-pushdown automata, i.e., there are languages which can be recognized by a deterministic flip-pushdown automaton with k+1 pushdown reversals but which cannot be recognized by a k-flip-pushdown (deterministic or nondeterministic). Furthermore, we investigate closure and non-closure properties as well as computational complexity problems such as fixed and general membership.

We study the number of steps required to reach a pure Nash Equilibrium in a load balancing scenario where each job behaves selfishly and attempts to migrate to a machine which will minimize its cost. We consider a variety of load balancing models, including identical, restricted, related and unrelated machines. Our results have a crucial dependence on the weights assigned to jobs. We consider arbitrary weights, integer weights, K distinct weights and identical (unit) weights. We look both at an arbitrary schedule (where the only restriction is that a job migrates to a machine which lowers its cost) and specific efficient schedulers (such as allowing the largest weight job to move first).

We study the problem of n users selfishly routing traffic through a network consisting of m parallel related links. Users route their traffic by choosing private probability distributions over the links with the aim of minimizing their private latency. In such an environment Nash equilibria represent stable states of the system: no user can improve its private latency by unilaterally changing its strategy.Nashification is the problem of converting any given non-equilibrium routing into a Nash equilibrium without increasing the social cost. Our first result is an O(nm2) time algorithm for Nashification. This algorithm can be used in combination with any approximation algorithm for the routing problem to compute a Nash equilibrium of the same quality. In particular, this approach yields a PTAS for the computation of a best Nash equilibrium. Furthermore, we prove a lower bound of $$ \Omega \left( {2^{\sqrt n } } \right) $$ and an upper bound of O(2n) for the number of greedy selfish steps for identical link capacities in the worst case.In the second part of the paper we introduce a new structural parameter which allows us to slightly improve the upper bound on the coordination ratio for pure Nash equilibria in [3]. The new bound holds for the individual coordination ratio and is asymptotically tight. Additionally, we prove that the known upper bound of $$ \frac{{1 + \sqrt {4m - 3} }} {2} $$ on the coordination ratio for pure Nash equilibria also holds for the individual coordination ratio in case of mixed Nash equilibria, and we determine the range of m for which this bound is tight.

This paper considers the many-to-many version of the original stable marriage problem posed by Gale and Shapley [1]. Each man and woman has a strict preference ordering on the members of the opposite sex and wishes to be matched with upto his or her specified number of partners. In this setup, a polynomial time algorithm for finding a stable matching that minimizes the sum of partner ranks across all men and women is provided. It is argued that this sum can be used as an optimality criterion for minimizing total dissatisfaction if the preferences over partner-combinations satisfy a no-complementarities condition. The results in this paper extend those already known for the one-to-one version of the problem.

Given two finite sets of points $$ \mathcal{X},\mathcal{Y} $$ in ℝn which can be separated by a nonnegative linear function, and such that the componentwise minimum of any two distinct points in $$ \mathcal{X} $$ is dominated by some point in $$ \mathcal{Y} $$, we show that $$ \left| \mathcal{X} \right| \leqslant n\left| \mathcal{Y} \right| $$. As a consequence of this result, we obtain quasi-polynomial time algorithms for generating all maximal integer feasible solutions for a given monotone system of separable inequalities, for generating all p-inefficient points of a given discrete probability distribution, and for generating all maximal empty hyper-rectangles for a given set of points in ℝn. This provides a substantial improvement over previously known exponential algorithms for these generation problems related to Integer and Stochastic Programming, and Data Mining. Furthermore, we give an incremental polynomial time generation algorithm for monotone systems with fixed number of separable inequalities, which, for the very special case of one inequality, implies that for discrete probability distributions with independent coordinates, both p-efficient and p-inefficient points can be separately generated in incremental polynomial time.

We consider two-player parity games played on transition graphs of higher order pushdown automata. They are “game-equivalent” to a kind of model-checking game played on graphs of the infinite hierarchy introduced recently by Caucal. Then in this hierarchy we show how to reduce a game to a graph of lower level. This leads to an effective solution and a construction of the winning strategies.

We show that checking weak bisimulation equivalence of 1-counter nets (Petri nets with only one unbounded place) is undecidable. This implies the undecidability of weak bisimulation equivalence for 1-counter machines. The undecidability result carries over to normed 1-counter nets/machines.

We study the behavioural theory of Cardelli and Gordon’s Mobile Ambients. We give an LTS based operational semantics, and a labelled bisimulation based equivalence that coincides with reduction barbed congruence. We also provide up-to proof techniques and prove a set of algebraic laws, including the perfect firewall equation.

According to Barthelman and Blumensath, the following families of infinite graphs are isomorphic: (1) prefix-recognisable graphs, (2) graph solutions of VR equational systems and (3) MS interpretations of regular trees. In this paper, we consider the extension of prefix-recognisable graphs to prefix-recognisable structures and of graphs solutions of VR equational systems to structures solutions of positive quantifier free definable (PQFD) equational systems. We extend Barthelman and Blumensath’s result to structures parameterised by infinite graphs by proving that the following families of structures are equivalent: (1) prefix-recognisable structures restricted by a language accepted by an infinite deterministic automaton, (2) solutions of infinite PQFD equational systems and (3) MS interpretations of the unfoldings of infinite deterministic graphs. Furthermore, we show that the addition of a fuse operator, that merges several vertices together, to PQFD equational systems does not increase their expressive power.

Adaptive raising by successive trials t₀ < t₁ < ... until some unknown goal g > 1 has been found by t_n ≥ g, causingtotal cost T(g) = t₀+...+t_n, is studied for optimizing T(g)/g. For corregames, where player G setting g and ‘finder’ F choosing t₀, t₁, . . . are playing mixed strategies, we prove a “Law of optimal adapting factor e”. Section 2 is more general about adaptive raising on several tracks, in Sect. 3 we add proofs for the optimal competitive factors under corresponding worst case analysis.— Methods and results are similar to those about searching for a point on a line or on many rays, see [[1], [3], [4], [5], [6]].

We consider the general on-line two server problem in which at each step both servers receive a request, which is a point in a metric space. One of the servers has to be moved to its request. The special case where the requests are points on the real line is known as the CNN-problem. It has been a well-known open question if an algorithm with a constant competitive ratio exists for this problem. We answer this question in the affirmative sense by providing the first constant competitive algorithm for the general two-server problem on any metric space.

We consider the problem of Online Facility Location, where demands arrive online and must be irrevocably assigned to an open facility upon arrival. The objective is to minimize the sum of facility and assignment costs. We prove that the competitive ratio for Online Facility Location is Θ(log n/log log n). On the negative side, we show that no randomized algorithm can achieve a competitive ratio better than Ω(log n/log log n) against an oblivious adversary even if the demands lie on a line segment. On the positive side, we present a deterministic algorithm achieving a competitive ratio of O(log n/log log n). The analysis is based on a hierarchical decomposition of the optimal facility locations such that each component either is relatively well-separated or has a relatively large diameter, and a potential function argument which distinguishes between the two kinds of components.

Document caching and connection caching are extensively studied problems. In document caching, one has to maintain caches containing documents accessible in a network. In connection caching, one has to maintain a set of open network connections that handle data transfer. Previous work investigated these two problems separately while in practice the problems occur together: In order to load a document, one has to establish a connection between network nodes if the required connection is not already open.In this paper we present the first study that integrates document and connection caching. We first consider a very basic model in which all documents have the same size and the cost of loading a document or establishing a connection is equal to 1. We present deterministic and randomized online algorithms that achieve nearly optimal competitive ratios unless the size of the connection cache is extremely small. We then consider general settings where documents have varying sizes. We investigate a Fault model in which the loading cost of a document is 1 as well as a Bit model in which the loading cost is equal to the size of the document.

A κ-system consists of κ quadratic Diophantine equations over nonnegative integer variables s₁, ..., s_m, t₁, ..., t_n of the form: $$ \begin{array}{*{20}c} {\sum\limits_{1 \leqslant j \leqslant l} {B_{1j} \left( {t_1 , \ldots ,t_n } \right)A_{1j} \left( {s_1 , \ldots ,s_m } \right) = C_1 \left( {s_1 , \ldots ,s_m } \right)} } \\ \vdots \\ {\sum\limits_{1 \leqslant j \leqslant l} {B_{kj} \left( {t_1 , \ldots ,t_n } \right)A_{kj} \left( {s_1 , \ldots ,s_m } \right) = C_k \left( {s_1 , \ldots ,s_m } \right)} } \\ \end{array} $$ where l, n, m are positive integers, the B’s are nonnegative linear polynomials over t₁, ..., t_n (i.e., they are of the form b₀ + b₁t₁ + ... + b_nt_n, where each b_i is a nonnegative integer), and the A’s and C’s are nonnegative linear polynomials over s₁, ..., s_m. We show that it is decidable to determine, given any 2-system, whether it has a solution in s₁, ..., s_m, t₁, ..., t_n, and give applications of this result to some interesting problems in verification of infinite-state systems. The general problem is undecidable; in fact, there is a fixed k > 2 for which the k-system problem is undecidable. However, certain special cases are decidable and these, too, have applications to verification.

We delimit the boundary between decidability versus undecidability of the weak monadic second-order logic of one successor (WS1S) extended with linear cardinality constraints of the form |X₁|+...+|X_r| < |Y₁|+...+|Y_s|, where the X_is and Y_js range over finite subsets of natural numbers. Our decidability and undecidability results are based on an extension of the classic logic-automata connection using a novel automaton model based on Parikh maps.

The μ-calculus is an expressive specification language in which modal logic is extended with fixpoint operators, subsuming many dynamic, temporal, and description logics. Formulas of μ-calculus are classified according to their alternation depth, which is the maximal length of a chain of nested alternating least and greatest fixpoint operators. Alternation depth is the major factor in the complexity of μ-calculus model-checking algorithms. A refined classification of μ-calculus formulas distinguishes between formulas in which the outermost fixpoint operator in the nested chain is a least fixpoint operator (Σ_i formulas, where i is the alternation depth) and formulas where it is a greatest fixpoint operator (∏_i formulas). The alternation-free μ-calculus (AFMC) consists of μ-calculus formulas with no alternation between least and greatest fixpoint operators. Thus, AFMC is a natural closure of Σ₁ ∪ ∏₁, which is contained in both Σ₂ and ∏₂. In this work we show that Σ₂ ∩ ∏₂≡ AFMC. In other words, if we can express a property ξ both as a least fixpoint nested inside a greatest fixpoint and as a greatest fixpoint nested inside a least fixpoint, then we can express ξ also with no alternation between greatest and least fixpoints. Our result refers to μ-calculus over arbitrary Kripke structures. A similar result, for directed μ-calculus formulas interpreted over trees with a fixed finite branching degree, follows from results by Arnold and Niwinski. Their proofs there cannot be easily extended to Kripke structures, and our extension involves symmetric nondeterministic Büchi tree automata, and new constructions for them.

We prove an upper bound result for the first-order theory of a structure W of queues, i.e. words with two relations: addition of a letter on the left and on the right of a word. Using complexity-tailored Ehrenfeucht games we show that the witnesses for quantified variables in this theory can be bound by words of an exponential length. This result, together with a lower bound result for the first-order theory of two successors [6], proves that the first-order theory of W is complete in LATIME(2O(n)): the class of problems solvable by alternating Turing machines runningin exponential time but only with a linear number of alternations.

Recently, Fabrikant, Koutsoupias and Papadimitriou [7] introduced a natural and beautifully simple model of network growth involving a trade-off between geometric and network objectives, with relative strength characterized by a single parameter which scales as a power of the number of nodes. In addition to giving experimental results, they proved a power-law lower bound on part of the degree sequence, for a wide range of scalings of the parameter. Here we prove that, despite the FKP results, the overall degree distribution is very far from satisfying a power law.First, we establish that for almost all scalings of the parameter, either all but a vanishingly small fraction of the nodes have degree 1, or there is exponential decay of node degrees. In the former case, a power law can hold for only a vanishingly small fraction of the nodes. Furthermore, we show that in this case there is a large number of nodes with almost maximum degree. So a power law fails to hold even approximately at either end of the degree range. Thus the power laws found in [7] are very different from those given by other internet models or found experimentally [8].

We introduce a concept of similarity between vertices of directed graphs. Let G_A and G_B be two directed graphs with respectively n_A and n_B vertices. We define a n_A × n_Bsimilarity matrixS whose real entry s_ij expresses how similar vertex i (in G_A) is to vertex j (in G_B) : we say that s_ij is their similarity score. In the special case where G_A = G_B = G, the score s_ij is the similarity score between the vertices i and j of G and the square similarity matrix S is the self-similarity matrix of the graph G. We point out that Kleinberg’s “hub and authority” method to identify web-pages relevant to a given query can be viewed as a special case of our definition in the case where one of the graphs has two vertices and a unique directed edge between them. In analogy to Kleinberg, we show that our similarity scores are given by the components of a dominant vector of a non-negative matrix and we propose a simple iterative method to compute them.

We study algorithmic problems that are motivated by bandwidth trading in next generation networks. Typically, bandwidth trading involves sellers (e.g., network operators) interested in selling bandwidth pipes that offer to buyers a guaranteed level of service for a specified time interval. The buyers (e.g., bandwidth brokers) are looking to procure bandwidth pipes to satisfy the reservation requests of end-users (e.g., Internet subscribers). Depending on what is available in the bandwidth exchange, the goal of a buyer is to either spend the least amount of money to satisfy all the reservations made by its customers, or to maximize its revenue from whatever reservations can be satisfied.We model the above as a real-time non-preemptive scheduling problem in which machine types correspond to bandwidth pipes and jobs correspond to the end-user reservation requests. Each job specifies a time interval during which it must be processed and a set of machine types on which it can be executed. If necessary, multiple machines of a given type may be allocated, but each must be paid for. Finally, each job has a revenue associated with it, which is realized if the job is scheduled on some machine.There are two versions of the problem that we consider. In the cost minimization version, the goal is to minimize the total cost incurred for scheduling all jobs, and in the revenue maximization version the goal is to maximize the revenue of the jobs that are scheduled for processing on a given set of machines. We consider several variants of the problems that arise in practical scenarios, and provide constant factor approximations.

We show that the satisfiability problem for CTL+, the branching time logic that allows boolean combinations of path formulas inside a path quantifier but no nesting of them, is 2-EXPTIME-hard. The construction is inspired by Vardi and Stockmeyer’s 2-EXPTIME-hardness proof of CTL*’s satisfiability problem. As a consequence, there is no subexponential reduction from CTL+ to CTL which preserves satisfiability.

Hierarchical and recursive state machines are suitable abstract models for many software systems. In this paper we extend a model recently introduced in literature, by allowing atomic propositions to label all the kinds of vertices and not only basic nodes. We call the obtained models context-dependent hierarchical/recursive state machines. We study on such models cycle detection, reachability and Ltl model-checking. Despite of a more succinct representation, we prove that Ltl model-checking can be done in time linear in the size of the model and exponential in the size of the formula, as for standard Ltl model-checking. Reachability and cycle detection become NP-complete, and if we place some restrictions on the representation of the target states, we can decide them in time linear in the size of the formula and the size of the model.

A special class of oracle circuits with tree-vector form is introduced. It is shown that they can be evaluated in deterministic polynomial-time with a polylog number of adaptive queries to an NP oracle. This framework allows us to evaluate the precise computational complexity of model checking for some branching-time logics where it was known that the problem is NP-hard and coNP-hard.

A spanning spider for a graph G is a spanning tree T of G with at most one vertex having degree three or more in T. In this paper we give densitycriteria for the existence of spanning spiders in graphs. We constructivelypro ve the following result: Given a graph G with n vertices, if the degree sum of anyindep endent triple of vertices is at least n − 1, then there exists a spanning spider in G. We also studythe case of bipartite graphs and give densityconditions for the existence of a spanning spider in a bipartite graph. All our proofs are constructive and implythe existence of polynomial time algorithms to construct the spanning spiders. The interest in the existence of spanning spiders originallyarises in the realm of multicasting in optical networks. However, the graph theoretical problems discussed here are interesting in their own right.

A graph G is R-role assignable if there is a locally surjective homomorphism from G to R, i.e. a vertex mapping r : V_G → V_R, such that the neighborhood relation is preserved: r(N_G (u)) = N_R(r(u)). Kristiansen and Telle conjectured that the decision problem whether such a mapping exists is an NP-complete problem for any connected graph R on at least three vertices. In this paper we prove this conjecture, i.e. we give a complete complexity classification of the role assignment problem for connected graphs. We show further corollaries for disconnected graphs and related problems.

The (k, r)-center problem asks whether an input graph G has ≤ k vertices (called centers) such that every vertex of G is within distance ≤ r from some center. In this paper we prove that the (k, r)-center problem, parameterized by k and r, is fixed-parameter tractable (FPT) on planar graphs, i.e., it admits an algorithm of complexity f(k, r)nO(1) where the function f is independent of n. In particular, we show that $$ f\left( {k,r} \right) = 2^{O\left( {r\log r} \right)\sqrt k } $$, where the exponent of the exponential term grows sublinearly in the number of centers. Moreover, we prove that the same type of FPT algorithms can be designed for the more general class of map graphs introduced by Chen, Grigni, and Papadimitriou. Our results combine dynamic-programming algorithms for graphs of small branchwidth and a graph-theoretic result bounding this parameter in terms of k and r. Finally, a byproduct of our algorithm is the existence of a PTAS for the r-domination problem in both planar graphs and map graphs.Our approach builds on the seminal results of Robertson and Seymour on Graph Minors, and as a result is much more powerful than the previous machinery of Alber et al. for exponential speedup on planar graphs. To demonstrate the versatility of our results, we show how our algorithms can be extended to general parameters that are “large” on grids. In addition, our use of branchwidth instead of the usual treewidth allows us to obtain much faster algorithms, and requires more complicated dynamic programming than the standard leaf/introduce/forget/join structure of nice tree decompositions. Our results are also unique in that they apply to classes of graphs that are not minor-closed, namely, constant powers of planar graphs and map graphs.

We study the fixed-parameter tractability, subexponential time computability, and approximability of the well-known NP-hard problems: Independent Set, Vertex Cover, and Dominating Set. We derive tight results and show that the computational complexity of these problems, with respect to the above complexity measures, is dependent on the genus of the underlying graph. For instance, we show that, under the widely-believed complexity assumption W[1] ≠ FPT, Independent Set on graphs of genus bounded by g₁(n) is fixed parameter tractable if and only if g₁(n) = o(n2), and Dominating Set on graphs of genus bounded by g₂(n) is fixed parameter tractable if and only if g₂(n) = no(1). Under the assumption that not all SNP problems are solvable in subexponential time, we show that the above three problems on graphs of genus bounded by g₃(n) are solvable in subexponential time if and only if g₃(n) = o(n).

Modern hardware designs are typically based on multiple clocks. While a singly-clocked hardware design is easily described in standard temporal logics, describing a multiply-clocked design is cumbersome. Thus it is desirable to have an easier way to formulate properties relatedto clocks in a temporal logic. We present a relatively simple solution built on top of the traditional ltl-basedseman tics, study the properties of the resulting logic, andcompare it with previous solutions.

We give an analysis of various classical axioms and characterize a notion of minimal classical logic that enforces Peirce’s law without enforcing Ex Falso Quodlibet. We show that a “natural” implementation of this logic is Parigot’s classical natural deduction. We then move on to the computational side and emphasize that Parigot’s λµ corresponds to minimal classical logic. A continuation constant must be added to λµ to get full classical logic. We then map the extended λµ to anew theory of control, λ-C−-top, which extends Felleisen’s reduction theory. λ-C−-top allows one to distinguish between aborting and throwing to a continuation. It is also in correspondence with the proofs of a refinement of Prawitz’s natural deduction.

A major hurdle in the algorithmic verification and control of systems is the need to find suitable abstract models, which omit enough details to overcome the state-explosion problem, but retain enough details to exhibit satisfaction or controllability with respect to the specification. The paradigm of counterexample-guided abstraction refinement suggests a fully automatic way of finding suitable abstract models: one starts with a coarse abstraction, attempts to verify or control the abstract model, and if this attempt fails and the abstract counterexample does not correspond to a concrete counterexample, then one uses the spurious counterexample to guide the refinement of the abstract model. We present a counterexample-guided refinement algorithm for solving ω-regular control objectives. The main difficulty is that in control, unlike in verification, counterexamples are strategies in a game between system and controller. In the case that the controller has no choices, our scheme subsumes known counterexample-guided refinement algorithms for the verification of ω-regular specifications. Our algorithm is useful in all situations where ω-regular games need to be solved, such as supervisory control, sequential and program synthesis, and modular verification. The algorithm is fully symbolic, and therefore applicable also to infinite-state systems.

Axiomatic criteria are given for the existence of higher-order maps over subobjects and quotients. These criteria are applied in showing the soundness of a method for proving specification refinement up to observational equivalence. This generalises the method to handle data types with higher-order operations, using standard simulation relations. We also give a direct setoid-based model satisfying the criteria. The setting is the second-order polymorphic lambda calculus and the assumption of relational parametricity.

We show how to support efficient back traversal in a unidirectional list, using small memory and with essentially no slowdown in forward steps. Using O(lg n) memory for a list of size n, the i’th back-step from the farthest point reached so far takes O(lg i) time worst case, while the overhead per forward step is at most epsilon for arbitrary small constant ε > 0. An arbitrary sequence of forward and back steps is allowed. A full trade-off between memory usage and time per back-step is presented: k vs. kn1/k and vice versa. Our algorithm is based on a novel pebbling technique which moves pebbles on a “virtual binary tree” that can only be traversed in a pre-order fashion.The list traversal synopsis extends to general directed graphs, and has other interesting applications, including memory efficient hash-chain implementation. Perhaps the most surprising application is in showing that for any program, arbitrary rollback steps can be efficiently supported with small overhead in memory, and marginal overhead in its ordinary execution. More concretely: Let P be a program that runs for at most T steps, using memory of size M. Then, at the cost of recording the input used by the program, and increasing the memory by a factor of O(lg T) to O(M lg T), the program P can be extended to support an arbitrary sequence of forward execution and rollback steps, as follows. The i’th rollback step takes O(lg i) time in the worst case, while forward steps take O(1) time in the worst case, and 1 + ε amortized time per step.

We introduce a new matching criterion — function matching — that captures several different applications. The function matching. problem has as its input a text T of length n over alphabet Σ_T and a pattern P = P[1]P[2] ... P[m] of length m over alphabet Σ_T. We seek all text locations i for which, for some function f: Σ_T → Σ_T (f may also depend on i), the m-length substring that starts at i is equal to f(P[1])f(P[2]) ... f(P[m]).We give a randomized algorithm which, for any given constant k, solves the function matching problem in time O(n log n) with probability $$ \frac{1} {{n^k }} $$ of declaring a false positive.W e give a deterministic algorithm whose time is O(n|Σ_T| logm) and show that it is almost optimal in the newly formalized convolutions model. Finally, a variant of the third problem is solved by means of two-dimensional parameterized matching, for which we also give an efficient algorithm.

A suffix array represents the suffixes of a string in sorted order. Being a simpler and more compact alternative to suffix trees, it is an important tool for full text indexing and other string processing tasks. We introduce the skew algorithm for suffix array construction over integer alphabets that can be implemented to run in linear time using integer sorting as its only nontrivial subroutine: 1.recursively sort suffixes beginning at positions i mod 3 ≠ 0.2.sort the remaining suffixes using the information obtained in step one.3.merge the two sorted sequences obtained in steps one and two.The algorithm is much simpler than previous linear time algorithms that are all based on the more complicated suffix tree data structure. Since sorting is a well studied problem, we obtain optimal algorithms for several other models of computation, e.g. external memory with parallel disks, cache oblivious, and parallel. The adaptations for BSP and EREW-PRAM are asymptotically faster than the best previously known algorithms.

The sequent calculus used in this paper is interesting because (1) it is equivalent to the standard formulation (natural) for Pure Type System (PTS), and (2) the corresponding cut-free subsystem makes it possible to introduce a notion of Cut Elimination (CE). This property has a deep impact on PTS and in logical frameworks based in PTS. CE is an open problem for normalizing generic PTS. Likewise, other proposed versions of cut elimination have not been solved in dependent type systems.Another interesting problem is Expansion Postponement (EP), posed by Henk Barendregt in August 1990. Except for PTS with important restrictions, EP is thus far an open problem, even for normalizing PTS. Surprisingly, in this paper we prove that EP is a consequence of CE.

We investigate the protection of migrating agents against the untrusted sites they traverse. The resulting calculus provides a formal framework to reason about protection policies and security protocols over distributed, mobile infrastructures, and aims to stand to ambients as the spi calculus stands to π. We present a type system that separates trusted and untrusted data and code, while allowing safe interactions with untrusted sites. We prove that the type system enforces a privacy property, and show the expressiveness of the calculus via examples and an encoding of the spicalculus.

It is known that a finite category can have all its base monoids in a variety V (i.e. be locally V, denoted ℓV) without itself dividing a monoid in V (i.e. be globally V, denoted gV). This is in particular the case when V=Com, the variety of commutative monoids. Our main result provides a combinatorial characterization of locally commutative categories. This is the first such theorem dealing with a variety for which local differs from global. As a consequence, we show that ℓCom⊂gV for every variety V that strictly contains the commutative monoids.

The problem of constructing a semi-pullback in a category is intimately connected to the problem of establishing the transitivity of bisimulations. Edalat shows that a semi-pullback can be constructed in the category of Markov processes on Polish spaces, when the underlying transition probability functions are universally measurable, and the morphisms are measure preserving continuous maps. We demonstrate that the simpler assumption of Borel measurability suffices. Markov processes are in fact a special case: we consider the category of stochastic relations over Standard Borel spaces. At the core of the present solution lies a selection argument from stochastic dynamic optimization. An example demonstrates that (weak) pullbacks do not exist in the category of Markov processes.

Many protocols are designed to operate correctly even in the case where the underlying communication medium is faulty. To capture the behaviour of such protocols, lossy channel systems (LCS) [3] have been proposed.In an LCS the communication channels are modelled as FIFO buffers which are unbounded, but also unreliable in the sense that they can nondeterministically lose messages.Recently, several attempts [[5], [1]Here we consider a more challenging problem, namely to calculate the probability by which a certain property is satisfied. Our main result is an algorithm for the following Quantitative model checking problem: Instance: A PLCS, its state s, a finite state ω-automaton $$ \mathcal{A} $$, and a rational θ > 0.Task: Find a rational r such that the probability of the set of computations that start at s and are accepted by $$ \mathcal{A} $$ is between r and r + θ.

Discounting the future means that the value, today, of a unit payoffis 1 if the payoffo ccurs today, a if it occurs tomorrow, a2 if it occurs the day after tomorrow, and so on, for some real-valued discount factor 0 < a < 1. Discounting (or inflation) is a key paradigm in economics and has been studied in Markov decision processes as well as game theory. We submit that discounting also has a natural place in systems engineering: for nonterminating systems, a potential bug in the far-away future is less troubling than a potential bug today. We therefore develop a systems theory with discounting. Our theory includes several basic elements: discounted versions of system properties that correspond to the ω-regular properties, fixpoint-based algorithms for checking discounted properties, and a quantitative notion of bisimilarity for capturing the difference between two states with respect to discounted properties. We present the theory in a general form that applies to probabilistic systems as well as multicomponent systems (games), but it readily specializes to classical transition systems. We show that discounting, besides its natural practical appeal, has also several mathematical benefits. First, the resulting theory is robust, in that small perturbations of a system can cause only small changes in the properties of the system. Second, the theory is computational, in that the values of discounted properties, as well as the discounted bisimilarity distance between states, can be computed to any desired degree of precision.

We consider games where the players have perfect information about the game’s state and history, and we focus on the information exchange that takes place at each round as the players choose their moves. The abilityof a player to gather information on the opponent’s choice of move in a round determines her ability to counteract the move, and win the game. When the game is played between teams, rather than single players, the amount of intra-team communication determines the ability of the team members to coordinate their moves and win the game. We consider games with quantitative bounds on inter-team and intra-team information flow, and we provide algorithms and complexity bounds for their solution.

It is just amazing that both of the mean hitting time and the cover time of a random walk on a finite graph, in which the vertex visited next is selected from the adjacent vertices at random with the same probability, are bounded by O(n3) for any undirected graph with order n, despite of the lack of global topological information. Thus a natural guess is that a better transition matrix is designable if more topological information is available. For any undirected connected graph G = (V,E), let P(β) = (p_uv(β))_u,v∈V be a transition matrix defined by $$ p_{uv}^{\left( \beta \right)} = \frac{{\exp \left[ { - \beta U\left( {u,v} \right)} \right]}} {{\sum _{w \in N\left( u \right)} \exp \left[ { - \beta U\left( {u,w} \right)} \right]}}foru \in V,v \in N\left( u \right), $$ where β is a real number, N(u) is the set of vertices adjacent to a vertex u, deg(u) = |N(u)|, and U(•, •) is a potential function defined as U(u, v) = log (max {deg(u), deg(v)}) for u ∈ V, v ∈ N(u). In this paper, we show that for any undirected graph with order n, the cover time and the mean hitting time with respect to P(1) are bounded by O(n2 log n) and O(n2), respectively. We further show that P(1) is best possible with respect to the mean hitting time, in the sense that the mean hitting time of a path graph of order n, with respect to any transition matrix, is Ω (n2).

Although evolutionary algorithms (EAs) are widely used in practical optimization, their theoretical analysis is stillin its infancy. Up to now results on the (expected) runtime are limited to discrete search spaces, yet EAs are mostly applied to continuous optimization problems. So far results on the runtime of EAs for continuous search spaces rely on validation by experiments/simulations since merely a simplifying model of the respective stochastic process is investigated.Here a first algorithmic analysis of the expected runtime of a simple, but fundamental EA for the search space IRn is presented. Namely, the so-called (1+1) Evolution Strategy ((1+1) ES) is investigated on unimodal functions that are monotone with respect to the distance between search point and optimum. A lower bound on the expected runtime is proven under the only assumption that isotropic distributions are used to generate the random mutation vectors. Consequently, this bound holds for any mutation adaptation mechanism. Finally, we prove that the commonly used “Gauss mutations” in combination with the socalled 1/5-rule for the mutation adaptation do achieve asymptotically optimal expected runtime.

We present a bijection between the set of plane triangulations (aka. maximal planar graphs) and a simply defined subset of plane trees with two leaves per inner node. The construction takes advantage of the minimal realizer (or Schnyder tree decomposition) of a plane triangulation.This yields a simple interpretation of the formula for the number of plane triangulations with n vertices. Moreover the construction is simple enough to induce a linear random sampling algorithm, and an explicit information theory optimal encoding.

We present an expected polynomial time algorithm to generate a labeled planar graph uniformly at random. To generate the planar graphs, we derive recurrence formulas that count all such graphs with n vertices and m edges, based on a decomposition into 1-, 2-, and 3- connected components. For 3-connected graphs we apply a recent random generation algorithm by Schaeffer and a counting formula by Mullin and Schellenberg.

We provide a new simpler approach to the on-line load balancing problem in the case of restricted assignment of temporary weighted tasks. The approach is very general and allows to derive online distributed algorithms whose competitive ratio is characterized by some combinatorial properties of the underlying graph representing the problem.The effectiveness of our approach is shown by the hierarchical server model introduced by Bar-Noy et al ’99. In this case, our method yields simpler and distributed algorithms whose competitive ratio is at least as good as the existing ones. Moreover, the resulting algorithms and their analysis turn out to be simpler. Finally, in all cases the algorithms are optimal up to a constant factor.Some of our results are obtained via a combinatorial characterization of those graphs for which our technique yields O($$ \sqrt n $$)-competitive algorithms.

Suppose that we are given a set of jobs, where each job has a processing time, a non-negative weight, and a set of possible time intervals in which it can be processed. In addition, each job has a processing cost. Our goal is to schedule a feasible subset of the jobs on a single machine, such that the total weight is maximized, and the cost of the schedule is within a given budget. We refer to this problem as budgeted real-time scheduling (BRS). Indeed, the special case where the budget is unbounded is the well-known real-time scheduling problem. The second problem that we consider is budgeted real-time scheduling with overlaps (BRSO), in which several jobs may be processed simultaneously, and the goal is to maximize the time in which the machine is utilized. Our two variants of the real-time scheduling problem have important applications, in vehicle scheduling, linear combinatorial auctions and QoS management for Internet connections. These problems are the focus of this paper.Both BRS and BRSO are strongly NP-hard, even with unbounded budget. Our main results are (2 + ε)-approximation algorithms for these problems. This ratio coincides with the best known approximation factor for the (unbudgeted) real-time scheduling problem, and is slightly weaker than the best known approximation factor of e/(e − 1) for the (unbudgeted) real-time scheduling with overlaps, presented in this paper. We show that better ratios (or simpler approximation algorithms) can be derived for some special cases, including instances with unit-costs and the budgeted job interval selection problem (JISP). Budgeted JISP is shown to be APX-hard even when overlaps are allowed and with unbounded budget. Finally, our results can be extended to instances with multiple machines.

We study a scheduling problem involving the optimal placement of advertisement images in a shared space over time. The problem is a generalization of the classical scheduling problem P∥C_max, and involves scheduling each job on a specified number of parallel machines (not necessarily simultaneously) with a goal of minimizing the makespan. In 1969 Graham showed that processing jobs in decreasing order of size, assigning each to the currently-least-loaded machine, yields a 4/3-approximation for P∥C_max. Our main result is a proof that the natural generalization of Graham’s algorithm also yields a 4/3-approximationto the minimum-space advertisement scheduling problem. Previously, this algorithm was only known to give an approximation ratio of 2, and the best known approximation ratio for any algorithm for the minimum-space ad scheduling problem was 3/2. Our proof requires a number of new structural insights, which leads to a new lower bound for the problem and a non-trivial linear programming relaxation. We also provide a pseudo-polynomial approximation scheme for the problem (polynomial in the size of the problem and the number of machines).

In this paper we consider the problem of routing packets in dynamically changing networks, using the anycast mode. In anycasting, a packet may have a set of destinations but only has to reach any one of them. This set of destinations may just be given implicitly by some anycast address. For example, each service (such as DNS) may be given a specific anycast address identifying it, and computers offering this service will associate themselves with this address. This allows communication to be made transparent from node addresses, which makes anycasting particularly interesting for dynamic networks, in which redundancy and transparency are vital to cope with a dynamically changing set of nodes. However, so far not much is known from a theoretical point of view about how to efficiently support anycasting in dynamic networks. This paper formalizes the anycast routing and admission control problem for arbitrary traffic in arbitrary dynamic networks, and provides first competitive solutions. In particular, we show that a simple local load balancing approach allows to achieve a near-optimal throughput if the available buffer space is sufficiently large compared to an optimal algorithm. Furthermore, we show via lower bounds and instability results that allowing admission control (i.e. dropping some of the injected packets) tremendously helps in keeping the buffer resources necessary to compete with optimal algorithms low.

In this paper we present efficient dynamic algorithms for approximation of kth, 1 ≤ k ≤ $$ \left( \begin{gathered} n \hfill \\ 2 \hfill \\ \end{gathered} \right) $$ distance defined by some pair of points from a given set S of n points in d-dimensional space, for every fixed d. Our technique is based on dynamization of well-separated pair decomposition proposed in [11], computing approximate nearest and farthest neighbors [[23], [26]] and use of persistent search trees [18].

Consider a set of n > 2 simple autonomous mobile robots (decentralized, asynchronous, no common coordinate system, no identities, no central coordination, no direct communication, no memory of the past, deterministic) moving freely in the plane and able to sense the positions of the other robots. We study the primitive task of gathering them at a point not fixed in advance (Gathering Problem). In the literature, most contributions are simulation-validated heuristics. The existing algorithmic contributions for such robots are limited to solutions for n ≤ 4 or for restricted sets of initial configurations of the robots. In this paper, we present the first algorithm that solves the Gathering Problem for any initial configuration of the robots.