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 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.

We separate monotone analogues of L and NL by proving that any monotone switching network solving directed connectivity on a set V(G) of n vertices must have size at least n^{&(\og n)}

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.

Stateless model checking is a powerful method for program verification, which however suffers from an exponential growth in the number of explored executions. A successful technique for reducing this number, while still maintaining complete coverage, is Dynamic Partial Order Reduction (DPOR), an algorithm originally introduced by Flanagan and Godefroid in 2005 and since then not only used as a point of reference but also extended by various researchers. In this article, we present a new DPOR algorithm, which is the first to be provably optimal in that it always explores the minimal number of executions. It is based on a novel class of sets, called source sets, which replace the role of persistent sets in previous algorithms. We begin by showing how to modify the original DPOR algorithm to work with source sets, resulting in an efficient and simple to implement algorithm, called source-DPOR. Subsequently, we enhance this algorithm with a novel mechanism, called wakeup trees, that allows the resulting algorithm, called optimal-DPOR, to achieve optimality. Both algorithms are then extended to computational models where processes may disable each other, e.g., via locks. Finally, we discuss trade-offs of the source- and optimal-DPOR algorithm and present programs that illustrate significant time and space performance differences between them. We have implemented both algorithms in a publicly available stateless model checking tool for Erlang programs. Experiments show that source sets significantly increase the performance of stateless model checking compared to using the original DPOR algorithm and that wakeup trees incur only a small overhead in both time and space in practice.