We are organizing a workshop series at the DISC conference. Please find all information at the CELL page.
In this talk, I outline the notion of local checkability and point at various ways this has proven useful. Local checking (or local verification, or local decision, or local detection, or...) and locally checkable predicates (or languages, or labeling, or ...) were suggested (by Afek, K., and Yuvan, 1990) in the context of self-stabilization. The motivation was the "easy" detection that program malfunctions so that it can be restarted. It was contrasted with the "costly" (i.e. global) checking suggested by Katz and Perry.
It was pointed out that this notion also resembles "easy" checking (or decision, or ...), i.e. polynomial vs. "costly" computing. Indeed, the use of this notion has spread beyond self-stabilization to various fields such as (distributed) complexity theory, distributed testing and peer to peer computing.
We will survey the relations between three classic models of distributed computing: the local model, the congest model, and the congested clique model.
We will then outline two links between the congested clique model, and two other computational models. The first is a reduction from Boolean circuits, which sheds some light on the inability to prove lower bounds for the congested clique. The second is an adaptation of parallel matrix multiplication algorithms to the congested clique, a result which allows fast distance computation and triangle detection.
In this talk I will present a new kind of computing device that uses biochemical reactions networks as building blocks to implement logic gates. The architecture of a computing machine relies on these generic and composable building blocks, computation units, that can be used in multiple instances to perform complex boolean functions. Standard logical operations are implemented by biochemical networks, encapsulated and insulated within synthetic vesicles called protocells. These protocells are capable of exchanging energy and information with each other through transmembrane electron transfer.
In the paradigm of computation we propose, protoputing, a machine can solve only one problem and therefore has to be built specifically. Thus, the programming phase in the standard computing paradigm is represented in our approach by the set of assembly instructions (specific attachments) that directs the wiring of the protocells that constitute the machine itself.
To demonstrate the computing power of protocellular machines, we apply it to solve a NP-complete problem, known to be very demanding in computing power, the 3-SAT problem. We show how to program the assembly of a machine that can verify the satisfiability of a given boolean formula. Then we show how to use the massive parallelism of these machines to verify in less than twenty minutes all the valuations of the input variables and output a fluorescent signal when the formula is satisfiable or no signal at all otherwise.
Gene insertion and deletion are basic operations occurring in DNA recombination in molecular biology. Errors in DNA recombination cause mutation that plays a part in normal/abnormal biological processes such as cancer, the immune system, protein synthesis and evolution. Since mutational damage may not be easily identifiable, site-directed mutagenesis that deliberately creates mutation under enzymatic activities in vitro has been studied. From a formal language viewpoint, we characterize site-directed insertion and deletion technique into operations on strings: Given two strings x and y, site-directed insertion inserts y into x if an outfix of y matches to infix of x, and site-directed deletion partially deletes a substring of x guided by the string y. We study closure properties of regular and context-free languages under site-directed insertion/deletion operations, and present efficient algorithms for decision problems related to the operations.
Visualisation techniques can enhance the understanding of circuit behaviour and their operating environment. Visualisation enables exploration of massive quantities of data from a high-level overview right down to low-level detail. During the presentation I will show two short animated movies that address clock domain crossing circuits, and whole-chip clock distribution. These visualisation aids are used to tune and debug designs, and have uncovered problems not found by the standard development tools.
Ian completed his PhD in Electrical Engineering at Imperial College, London in 1986. He was introduced to asynchronous circuit and systems design while working with Sutherland, Sproull and Associates, Inc. In 1987 Ian went to work in the Advanced Technology Group at Apple Computer. At Apple he helped develop a software-programmable gate array chip prototype -- one of his few clocked chip designs. He joined Sun Labs in 1992, which became Oracle Labs in 2010, where he has continued research work focusing on high speed asynchronous circuits and clock domain crossing circuits. Ian works closely with designers in product divisions, applying asynchronous circuit techniques to help improve their products.
Population protocols are a well established model of distributed computation by mobile finite-state agents with very limited storage. A classical result establishes that population protocols compute exactly predicates definable in Presburger arithmetic. We initiate the study of the minimal amount of memory required to compute a given predicate as a function of its size. We present results on the predicates x \geq n for n>0, and more generally on the predicates corresponding to systems of linear inequalities. We show that they can be computed by protocols with O(log n) states (or, more generally, logarithmic in the coefficients of the predicate), and that, surprisingly, some families of predicates can be computed by protocols with O(\log\log n) states. We give essentially matching lower bounds for the class of 1-aware protocols.
This is a seminar of the INFINI research team: http://www.lsv.fr/axes/INFINI/infini?l=en
Population protocols (Angluin et al., PODC 2004) are a formal model of sensor networks consisting of identical, finite-stae mobile devices. When two devices come into the range of each other, they interact and change their states. Computations are infinite sequences of pairwise interactions where the interacting processes are picked by a fair scheduler.
A population protocol is well specified if for every initial configuration C of devices and for every fair computation starting at C, all devices eventually agree on a consensus value that only depends on C. If a protocol is well-specified, then it is said to compute the predicate that assigns to each initial configuration its consensus value. The main two verification problems for population protocols are: Is a given protocol well-specified? Does a given protocol compute a given predicate ?
While the class of predicates computable by population protocols was already established in 2007 (Angluin et al., Distributed Computing), the decidability of the verification problems remained open until 2015, when my colleagues and I finally proved it (Esparza et al., CONCUR 2015, improved version to appear in Acta Informatica). However, the complexity of our decision procedures is very high. We have recently identified a class of procotols that, while being as expressive as the complete class, is far more tractable. I report on these results, and on some experimental results.
Rapid developements in circuit design over the last decades have not only led to an increased performance at lower area requirements but also increased the complexity to accurately model the signal traces, such that analog simulation tools like SPICE nowadays quickly reach their limit with increasing size. Therefore high level approaches, which abstract certain parts of the circuit, are required to achieve a reasonable computational effort while still maintaining an adequate accuracy.
In this talk I will present our digital involution delay model that faithfully predicts signal delays in electronic circuits. Faithful in this sense means that a circuit can only be modelled if it can be implemented in actual hardware and vice versa. The delay of a single transition is determined as a function f(T) with T being the previous-output-to-input transition time difference and f(.) an involution, i.e., fulfilling -f(-f(T)) = T. Compared to the established pure and inertial delay our approach allows accurate modeling of pulse degradation effects, which become very important for example for power estimations.
Despite the good results we already achieved the model is far from being finished. I will therefore also present some extensions we are currently investigating such as introducing non-determinism, reducing the characterization effort or increasing the accuracy.
Intracellular variability is a major obstacle to the fidelity required for a genetic circuit to execute a series of "pre-programmed" instructions. Over the past five years we have explored how determinism can arise from the synchronization of a large number of cells; in other words, synchronize gene circuits operating in individual cells and view the colony as the primary design element. We are currently using our understanding of these processes to engineer bacteria for the safe production and delivery of anti-tumor toxins. The long-held monolithic view of bacteria as pathogens has given way to an appreciation of the widespread prevalence of functional microbes within the human body. Given this vast milieu, it is perhaps inevitable that certain bacteria would evolve to preferentially grow in environments that harbor disease and thus provide a natural platform for the development of engineered therapies. We have engineered a clinically relevant bacterium to lyse synchronously at a threshold population density and to release genetically encoded cargo. Following quorum lysis, a small number of surviving bacteria reseed the growing population, thus leading to pulsatile de- livery cycles. Working with Sangeeta Bhatia (MIT) and Tal Danino (Columbia), we have begun to demonstrate the therapeutic potential of the bacteria in animal models using luciferase to monitor in vivo bacterial population dynamics. This work represents our early progress in transversing the scales of Synthetic Biology from the level of mathematically designed circuitry to therapeutically relevant animal models.
See here for details: https://parsys.lri.fr/seminar-hasty.html