Current Past Me Papers Talks Artifacts Extra HotPage

Tool Paper [CMSB'2020 Best Tool Paper Award.]
Talk (15min) [CMSB'20]
User Manual

Molecular Programming

The goal of molecular programming is the systematic manipulation of matter at the molecular scale, for applications in engineering + technology and biology + medicine.
Structural DNA/RNA nanotechnology currently provides the only fabrication pipeline for truly programmable molecular structures, in the form of static and dynamic nucleic acid assemblies. But through it we can organize also other forms of matter.

Sequenceable Event Recorders (arXiv'21, Springer'23)
PID Control of Biochemical Reaction Networks (CDC'19, TAC'21)
Chemical Reaction Network Designs for Asynchronous Logic Circuits (DNA22 '16, NaCo '17)
Programming Discrete Distributions with Chemical Reaction Networks (DNA22 '16, NaCo '17)
The Formal Language and Design Principles of Autonomous DNA Walker Circuits (ACS Synthetic Biology'16)
Automated Design and Verification of Localized DNA Computation Circuits (DNA21 '15)
Programmable chemical controllers made from DNA (Nature Nanotech '13)
Two-Domain DNA Strand Displacement (MSCS'13)
Abstractions for DNA circuit design (J.R.S. Interface '12)
Design and Analysis of DNA Strand Displacement Devices using Probabilistic Model Checking (J.R.S. Interface '12)
Strand Algebras for DNA Computing (Natural Computing '11)
A Programming Language for Composable DNA Circuits (J.R.S.Interface '09)
Edited Proceedings
DNA 17
info Telling Molecules What To Do (Lisbon Distinguished Lecture)
info Molecular Programming (ECOOP'14)
info Computing with Molecules (DCM'12)
info Two-Domain DNA Strand Displacement (DCM'10)
info Strand Algebras for DNA Computing (DNA '09)
info DSD - DNA Strand Displacement Simulator (info J.R.S. Interface '13)
info Gener - DNA Strand Displacement Reductions (info Bioinformatics '15)
info Correctness of DNA encodings of chemical reaction networks
info DNA Computing and Molecular Programming Conferences
info NYU • Caltech • UW • Duke • Oxford • Aarhus • Microsoft

info Inner Life of A Cell - Movie
info Powering the Cell: Mitochondria - Movie
info DNA Strand Displacement - Movies
info Nanocrafter - Game
info EteRNA - Game

Systems Biology

Reactive Systems

An abstract machine is a fictional information-processing device that can, in principle, have a number of different physical realizations (mechanical, electronic, biological, or software). Biochemical toolkits in cellular biology (nucleotides, amino acids, and phospholipids) can be seen as abstract machines with appropriate sets of states and operations, corresponding respectively to genes, proteins, and membranes. To understand the functioning of a cell, one must understand (at least) how the various machines interact. This involves considerable difficulties in modeling and simulations because of the drastic differences in the "programming model" of each machine, and in the time and size scales involved.

Lineage Grammars: Describing, Simulating and Analyzing Population Dynamics. (BMC Bioinformatics'14)
An Intuitive Modelling Interface for Systems Biology (DCM'09) (IJSI'13)
Abstract Machines of Systems Biology (TCSB)
Artificial Biochemistry (Algorithmic Bioprocesses)
Can a Systems Biologist Fix a Tamagotchi? (Gilles Kahn Colloquium)
Visualization in Process Algebra Models of Biological Systems (The Fourth Paradigm)
A Compositional Approach to the Stochastic Dynamics of Gene Networks (TCSB)
Compositionality, Stochasticity and Cooperativity in Dynamic Models of Gene Regulation (HFSP ournal)
info Artificial Biochemistry - Graduate Course (Trento, May 22-26 '06)
info Speaking the Language of Molecules (CDE Distinguished Lacture, U.Washington)
info Living Software (L'INRIA a Quarante Ans)
info Artificial Biochemistry (Longo Symposium 2007)
info Can a Systems Biologist Fix a Tamagotchi? (Kahn Colloquium 2007)
info Abstract Machines of Systems Biology (Dagstuhl 2006)
info Languages and Notations for Systems Biology (UPP'04 Invited Talk)
info A Compositional Approach to the Stochastic Dynamics of Gene Networks (Concur '05)
info Adrian Thompson: Evolution of circuits in hardware (archive)

Membrane Computing

The basic physical operations on membranes are local fusion (two patches merging) and local fission (one patch splitting in two). When seen at the global scale of whole membranes, these local operations induce four transformations: in addition to the obvious splitting (Mito) and merging (Mate) of membranes, there are also operation, quite common in reality, that cause a membrane to eat (Endo) or spit (Exo) another subsystem. Although this is an unusual computational model, the membrane operations supports the execution of real algorithms, some of which occur in nature. Some sets of operations are Turing-complete, and can encode the other membrane operations.

Papers on
Brane Calculi
Programming Chemistry in DNA Addressable Bioreactors (Interface '14)
Brane Calculi (ENTCS, CMSB'04)
Bitonal Membrane Systems (TCS)
Where Membranes Meet Complexes (BioConcur '05)
A Universality Result for a (Mem)Brane Calculus Based on Mate/Drip Operations (IJFCS)
Papers on
BioAmbients: An Abstraction for Biological Compartments (TCS)
Bioware Languages (Computing Systems - A Tribute to Roger Needham)
info Membrane Interactions PDF PDF (CSSB School Rovereto, April'04)
info Bitonal Membrane Systems (MeCBIC'06)
info WhereMembranesMeetComplexes (BioConcur'05)
info Biological Systems as Reactive Systems (ECCS'05)

Continuous Markov Processes

We introduce stochastic extensions of process algebras endowed with structural operational semantics expressed in terms of measure theory. The set of processes is organised as a measurable space by the sigma-algebra generated by structural congruence. The structural operational semantics associates to each process a set of measures over the space of processes. The measures encode the rates of the transitions from a process (state of a system) to a measurable set of processes. We prove that stochastic bisimulation is a congruence that extends structural congruence. In addition to an elegant operational semantics, our approach provides a canonic way to define metrics on processes that measure how similar two processes are in terms of behaviour.

Papers on
Continuous Markovian Logic Axiomatization and Quantified Metatheory (LMCS'12)
Modular Markovian Logic (ICALP'11)
Continuous Markovian Logic (CLS'11)
Papers on
Stochastic Pi-Calculus Revisited (ICTAC'13)
The Measurable Space of Stochastic Processes (QEST'10, Fundamenta Informaticae)
info Stochastic Pi-Calculus Revisited (ICTAC'13)
info Continuous Markovian Logic (CSL'11)
info Modular Markovian Logic (ICALP'11)
info The Measurable Space of Stochastic Processes (QEST'10)

Natural Computability

We investigate the question of whether basic chemical kinetics (kinetics of unar yand binary chemical reactions), formulated as a process algebra, is capable of general computation. In particular, we investigate nondeterministic and probabilistic termination problems. The answers to those problems reveal a surprisingly rich picture of what is decidable and undecidable in basic chemistry.
We introduce an algebra for massive concurrent systems, called reversible structures, where terms retain bits of causal dependencies that allow one to reverse computation histories. These bits permit to trace effects of interactions, but not to the point of being able to identify the precise molecule that caused an effect. The algebra and the causal hints match a particular form of DNA computation.

Papers on
Turing Universality of the Biochemical Ground Form (MSCS)
On the Computational Power of Biochemistry (AB'08)
Termination Problems in Chemical Kinetics (CONCUR'08)
Papers on
Reversibility in Massive Concurrent Systems (SACS)
Reversible Structures (CMSB '11)
info Termination Problems in Chemical Kinetics (CONCUR'08)
info On The Computational Power of Biochemistry (AB'08)
info Reversible Structures (CMSB'11)

Molecular Semantics

The semantics of programming languages is based on states and state transitions, through which one can study for example termination, nodeterminism, and concurrency. Adding rates to transitions induces quantitative meanings that can be related to stochastic and continuous dynamical systems, and to their realizations as molecular systems.

Papers on design
A Language for Modeling And Optimizing Experimental Biological Protocols (MDPI Computation'21)
From Electric Circuits to Chemical Networks (Natural Computing'19)
Experimental Biological Protocols with Formal Semantics (CMSB'18)
Molecular Filters for Noise Reduction (Biophysical Journal'18)
Syntax-Guided Optimal Synthesis for Chemical Reaction Networks (CAV'17)

Papers on verification
and approximation
Central Limit Model Checking (TOCL'19)
Reachability Computation for Switching Diffusions (HSCC'17)
A Stochastic Hybrid Approximation for Chemical Kinetics Based on the Linear Noise Approximation (CMSB'15, BioSystems'16)
Approximation of Probabilistic Reachability for Chemical Reaction Networks... (QEST'16)
Stochastic Analysis of Chemical Reaction Networks Using Linear Noise Approximation (CMSB'15)
Papers on morphisms
and bisimulation
Lumpability for Uncertain Continuous-Time Markov Chains.pdf (QEST'21)
Exact Maximal Reduction of Stochastic Reaction Networks by Species Lumping (BioInformatics'21)
Maximal aggregation of polynomial dynamical systems (PNAS'17)
Guaranteed Error Bounds on Approximate Model Abstractions through Reachability Analysis (QEST'18)
Syntactic Markovian Bisimulation for Chemical Reaction Networks (Springer'17)
Comparing Chemical Reaction Networks: A Categorical and Algorithmic Perspective (LICS'16, TCS'17)
ERODE: A Tool for the Evaluation and Reduction of Ordinary Differential Equations (TACAS'17)
Efficient Syntax-Driven Lumping of Differential Equations (TACAS'16)
Symbolic Computation of Differential Equivalences (POPL'16)
Forward and Backward Bisimulations for Chemical Reaction Networks (CONCUR'15)
Morphisms of Reaction Networks that Couple Structure to Function (BMC Systems Biology'14)
Papers on chemistry
via process algebra
On Process Rate Semantics (TCS'08)
A Process Algebra Master Equation (QEST'07)
From Processes to ODEs by Chemistry (IFIP TCS'08)
A Correct Abstract Machine for the Stochastic Pi-calculus (BioConcur'04)
Efficient, Correct Simulation of Biological Processes in Stochastic Pi-calculus (CMSB'07)
A Graphical Representation for Biological Processes in Stochastic Pi-calculus (TCSB)
Processes in Space (CiE'10, TCS 2012)
info On Process Rate Semantics PDF (Warsaw Lectures Extract, March'09)
info Molecules as Automata - Open Lectures PDF PDF PDF PDF (Warsaw, March&May'09)
info Molecules as Automata - Summer School on Natural Computation PDF PDF (BNC'08)
info Process Rate Semantics - Computational and Systems Biology Course (Trento 2008)
info Morphisms of Reaction Networks (CMSB'16)
info Molecules as Automata (DNA'08, ECS'09)
info From Processes to ODEs by Chemistry (TCS'08)
info On Process Rate Semantics (MFPS'08)
info A Graphical Representation for Stochastic ?-Calculus (BioConcur '05)
info A Correct Abstract Machine for the Stochastic pi-calculus (BioConcur '04)
info Processes in Space (CiE'10)
info Pi in the Sky: Spatial Process Algebra for Developmental Biology (MeCBIC'09)
Stochastic Analysis of Chemical Reaction Networks Using Linear Noise Approximation (DNA21'15)
info ERODE - SMT-based Automatic Exact Reduction of Ordinary Differential Equations (POPL '16 Artifact Evaluated)
info CRNReducer - Automatic exact reduction of Chemical Reaction Networks (CONCUR '15)

Biological Models


Coupled Membrane Transporters Reduce Noise (Physical Review E.'20)

Cell Cycle Switch

At the core of the biochemical networks that regulates the cell cycle there is a switch that triggers an irreversible transition from one critical stage of cell division to the next. Its dynamical system behavior is fairly well understood, and could be achieved by many different networks. But in nature, from yeast to us, we find a specific universal structure of the network: what is special about this structure, beyond its required function? To answer this question we shift our perspective from dynamical systems to computing systems. We ask: what does the cell cycle switch compute, and how does it compute it?

Evolution of opposing regulatory interactions underlies the emergence of eukaryotic cell cycle checkpoints (SciRep'21)
Single molecules can operate as primitive biological sensors switches and oscillators (BMC SysBio'18)
Computing with biological switches and clocks (Natural Computing'18)
Efficient Switches in Biology and Computer Science (PLOS CompBio'17)
Noise Reduction in Complex Biological Switches (Scientific Reports'16)
The Cell Cycle Switch Computes Approximate Majority (Scientific Reports'12)
Transcriptional Regulation is a Major Controller of Cell Cycle Transition Dynamics (PLoS ONE)
info The Cell Cycle Switch Computes Approximate Majority Robert Stewart Distinguished Lecture (Iowa State 2014)
Evolution of Simple Systems to Complex Behaviours (King's College PhD Symposium'16)
Analyzing Efficiency of Biological Switches (SSBSS'15)
Evolution of Biological Switches (King's College PhD Symposium'15)


Organisms employ a variety of signalling systems to sense and react to their environment. Among the most basic, commonly found in bacteria, lower eukaryotes and plants, are the so-called phosphorelays. These systems transfer sensor information (typically from the cellular membrane) very economically through a chain of chemical reactions.
Despite their widespread use and simple architecture, we are still far from a full understanding of the signal-processing capabilities of phosphorelays.

Unlimited multistability and Boolean logic in microbial signaling (J.R.S. Interface)
Phosphorelays provide tunable signal processing capabilities for the cell (PLOS CompBio)
Response Dynamics of Phosphorelays Suggest Their Potential Utility in Cell Signaling (J.R.S. Interface)

Immune System

Major Histocompatibility Complex (MHC) class I molecules are a key component of the innate immune system. They continuously select a signature of the cell contents (fragments of any protein present) and present it to the cell surface, where it can be inspected by cytotoxic T lymphocytes that destroy virus-infected and cancerous cells based on such signature. In this mechanism there is a trade-off between speed and accuracy of presentation: we study how various molecular components contribute to optimizing this process.

A Peptide Filtering Relation Quantifies MHC Class I Peptide Optimization (PLoS Computational Biology)
A Stochastic ?-Calculus Models of MHC Class I Antigen Presentation (Computational Biology MPhil Project)
info Selector function of MHC I molecules is determined by protein plasticity
info Computational Modeling of Immune System Processes

Pi-Calculus Models

We use stochastic pi-calculus to represent and then simulate interactions within protein networks. The pi-calculus approach allows a biological system to be programmed in a scalable manner, by allowing models of individual proteins to be directly composed to form subsystems, which can in turn be composed together to form larger systems. This allows new components to be added incrementally without having to re-wire the existing model, which also improves the usability of models. Furthermore, the modular structure of the biological system and the pi-calculus model are in direct correspondence.

Computational Modeling of the EGFR Network Elucidates Control Mechanisms Regulating Signal Dynamics (BMC Systems Biology)
A Process Model of Rho GTP-binding Proteins (FBTC'07) (TCS)
A Process Model of Actin Polymerisation (FBTC'08) (ENTCS)
info Biochemical Systems as Reactive Systems - Bioinformatics Master Course (Cabridge '16)
info Biological Networks in Stochastic Pi-Calculus (Imperial College London 2005)
University of Oxford Computer Science | Automated Verification Group
Microsoft Research Cambridge | Biological Computation Group

| site statistics