ACM DL

Journal of the ACM (JACM)

Menu
Latest Articles

A Temporal Logic Approach to Binding-Time Analysis

This article demonstrates that there is a fundamental relationship between temporal logic and languages that involve multiple stages, such as those... (more)

Upward Max-Min Fairness

Often one would like to allocate shared resources in a fair way. A common and well-studied notion of fairness is Max-Min Fairness, where we first maximize the smallest allocation, and subject to that the second smallest, and so on. We consider a networking application where multiple commodities compete over the capacity of a network. In our... (more)

Instance-Optimal Geometric Algorithms

We prove the existence of an algorithm A for computing 2D or 3D convex hulls that is optimal for every point set in the following sense: for every sequence σ of n points and for every algorithm A′ in a certain class A, the running time of A on input σ is at most a constant factor times the running time of A′ on the worst... (more)

Coloring 3-Colorable Graphs with Less than n1/5 Colors

We consider the problem of coloring a 3-colorable graph in polynomial time using as few colors as possible. We first present a new combinatorial... (more)

Amplifiers for the Moran Process

The Moran process, as studied by Lieberman, Hauert, and Nowak, is a randomised algorithm modelling the spread of genetic mutations in populations. The algorithm runs on an underlying graph where individuals correspond to vertices. Initially, one vertex (chosen uniformly at random) possesses a mutation, with fitness r > 1. All other individuals... (more)

NEWS

Important Note on P/NP: Some submissions purport to solve a long-standing open problem in complexity theory, such as the P/NP problem. Many of these turn out to be mistaken, and such submissions tax JACM volunteer editors and reviewers. JACM remains open to the possibility of eventual resolution of P/NP and related questions, and continues to welcome submissions on the subject. However, to mitigate the burden of repeated resubmissions due to incremental corrections of errors identified during editorial review, no author may submit more than one such paper to JACM, ACM Trans. on Algorithms, or ACM Trans. on Computation in any 24-month period, except by invitation of the Editor-in-Chief. This applies to resubmissions of previously rejected manuscripts. Please consider this policy before submitting a such a paper.

About JACM

The Journal of the ACM (JACM) provides coverage of the most significant work on principles of computer science, broadly construed. The scope of research we cover encompasses contributions of lasting value to any area of computer science. To be accepted, a paper must be judged to be truly outstanding in its field.  JACM is interested  in work in core computer science and at the boundaries, both the boundaries of subdisciplines of computer science and the boundaries between computer science and other fields.

read more
Forthcoming Articles
The freezing threshold for k-colourings of a random graph

We determine the exact value of the freezing threshold, r_k, for k-colourings of a random graph when k g 14. We prove that for random graphs with density above r_k, almost every colouring is such that a linear number of vertices are frozen, meaning that their colours cannot be changed by a sequence of alterations whereby we change the colours of o(n) vertices at a time, always obtaining another proper colouring. When the density is below r_k, then almost every colouring is such that every vertex can be changed by a sequence of alterations where we change O(log n) vertices at a time. Frozen vertices are a key part of the clustering phenomena discovered using methods from statistical physics. The value of the freezing threshold was previously determined by the non-rigorous cavity method.

Monadic Decomposition

Monadic predicates play a prominent role in many decidable cases, including decision procedures for symbolic automata. We are here interested in discovering whether a formula can be rewritten into a Boolean combination of monadic predicates. Our setting is quantifier-free formulas whose satisfiability is decidable, such as linear arithmetic and we here develop a semi-decision procedure for extracting a monadic decomposition of a formula when it exists.

Plane Formation by Synchronous Mobile Robots in the Three Dimensional Euclidean Space

Creating a swarm of mobile computing entities frequently called robots, agents or sensor nodes, with self-organization ability is a contemporary challenge in distributed computing. Motivated by this, we investigate the plane formation problem that requires a swarm of robots moving in the three dimensional Euclidean space to land on a common plane. The robots are fully synchronous and endowed with visual perception. But they do not have identifiers, nor access to the global coordinate system, nor any means of explicit communication with each other. Though there are plenty of results on the agreement problem for robots in the two dimensional plane, for example, the point formation problem, the pattern formation problem, and so on, this is the first result for robots in the three dimensional space. This paper presents a necessary and sufficient condition for fully-synchronous robots to solve the plane formation problem that does not depend on obliviousness i.e., the availability of local memory at robots. An implication of the result is somewhat counter-intuitive: The robots cannot form a plane from most of the semi-regular polyhedra, while they can form a plane from every regular polyhedron (except a regular icosahedron), whose symmetry is usually considered to be higher than any semi-regular polyhedron.

Constant-rate coding for multiparty interactive communication is impossible

We study coding schemes for multiparty interactive communication over synchronous networks that suffer from stochastic noise, where each bit is independently flipped with probability µ. We analyze the minimal overhead that must be added by the coding scheme in order to succeed in performing the computation despite the noise. Our main result is a lower bound on the communication of any noise-resilient protocol over a synchronous star network with n-parties (where all parties communicate in every round). Specifically, we show a task that can be solved by communicating T bits over the noise-free network, but for which any protocol with success probability of 1  o(1) must communicate at least ©(T log n / log log n ) bits when the channels are noisy. By a 1994 result of Rajagopalan and Schulman, the slowdown we prove is the highest one can obtain on any topology, up to a log log n factor. We complete our lower bound with a matching coding scheme that achieves the same overhead; thus, the capacity of (synchronous) star networks is ˜(log log n / log n). Our bounds prove that, despite several previous coding schemes with rate ©(1) for certain topologies, no coding scheme with constant rate ©(1) exists for arbitrary n-party noisy networks.

Verifying Increasingly Expressive Temporal Logics for Infinite-State Systems

Temporal logic is a formal system for specifying and reasoning about propositions qualified in terms of time. It offers a unified approach to program verification as it applies to both sequential and parallel programs and provides a uniform framework for describing a system at any level of abstraction. Thus a number of automated systems have been proposed to exclusively reason about either Computation-Tree Logic (CTL) or Linear Temporal Logic (LTL) in the infinite-state setting. Unfortunately, these logics have significantly reduced expressiveness as they restrict the interplay between temporal operators and path quantifiers, thus disallowing the expression of a many practical properties, for example ``along some future an event occurs infinitely often''. Contrarily, CTL*, a superset of both CTL and LTL, can facilitate the interplay between path-based (temporal) and state-based (path quantification) reasoning. CTL* thus exclusively allows for the expressiveness of properties involving existential system stabilization and ``possibility'' properties. Until now, there have not existed automated systems that allow for the verification of such expressive CTL* properties over infinite-state systems. This paper proposes a method capable of such a task, thus introducing the first known fully automated tool for symbolically proving CTL* properties of (infinite-state) integer programs. The method uses an internal encoding that admits reasoning about the subtle interplay between the nesting of temporal operators and path quantifiers that occurs within CTL* proofs. A precondition synthesis strategy is then used over a program transformation that trades nondeterminism in the transition relation for nondeterminism explicit in variables predicting future outcomes when necessary. This paper demonstrates the viability of our approach in practice, thus leading to a new class of fully-automated tools capable of proving crucial properties that no tool could previously prove. Additionally, we consider the linear-past extension to CTL* for infinite-state systems in which the past is linear and each moment in time has a unique past. We discuss the practice of this extension and how it is further supported through the use of history variables. We have implemented our approach and report our benchmarks carried out on case studies ranging from smaller programs to demonstrate the expressiveness of CTL* specifications, to larger code bases drawn from device drivers and various industrial examples.

Property-Directed Inference of Universal Invariants or Proving Their Absence

We present Universal Property Directed Reachability (PDR), a property-directed semi-algorithm for automatic inference of invariants in a universal fragment of first-order logic. PDR is an extension of Bradley's PDR/IC3 algorithm for inference of propositional invariants. PDR terminates when it either discovers a concrete counterexample, infers an inductive universal invariant strong enough to establish the desired safety property, or finds a proof that such an invariant does not exist. PDR is not guaranteed to terminate. However, we prove that under certain conditions, e.g., when reasoning about programs manipulating singly-linked lists, it does. We implemented an analyzer based on PDR, and applied it to a collection of list-manipulating programs. Our analyzer was able to automatically infer universal invariants strong enough to establish memory safety and certain functional correctness properties, show the absence of such invariants for certain natural programs and specifications, and detect bugs. All this, without the need for user-supplied abstraction predicates.

All ACM Journals | See Full Journal Index

Search JACM
enter search term and/or author name