@inproceedings{Pauleve:2010:GAM:1839764.1839771, author = {Paulev\'{e}, Lo\"{\i}c and Youssef, Simon and Lakin, Matthew R. and Phillips, Andrew}, title = {A generic abstract machine for stochastic process calculi}, booktitle = {Proceedings of the 8th International Conference on Computational Methods in Systems Biology}, series = {CMSB '10}, year = {2010}, isbn = {978-1-4503-0068-1}, location = {Trento, Italy}, pages = {43--54}, numpages = {12}, url = {http://doi.acm.org/10.1145/1839764.1839771}, doi = {http://doi.acm.org/10.1145/1839764.1839771}, acmid = {1839771}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {bioambient calculus, generic abstract machine, implementation, non-Markovian simulation, stochastic pi-calculus}, } @inproceedings{DBLP:journals/corr/abs-1011-0487, author = {Andrew Phillips and Matthew Lakin and Lo\"{\i}c Paulev{\'e}}, title = {Stochastic Simulation of Process Calculi for Biology}, booktitle = {MeCBIC}, year = {2010}, pages = {1-5}, ee = {http://dx.doi.org/10.4204/EPTCS.40.1}, crossref = {DBLP:journals/corr/abs-1011-0051}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{DBLP:journals/corr/abs-1011-0051, editor = {Gabriel Ciobanu and Maciej Koutny}, title = {Proceedings Fourth Workshop on Membrane Computing and Biologically Inspired Process Calculi 2010}, booktitle = {MeCBIC}, series = {EPTCS}, volume = {40}, year = {2010}, ee = {http://dx.doi.org/10.4204/EPTCS.40}, bibsource = {DBLP, http://dblp.uni-trier.de} } @article{Wang-etal-BMCSB09 ,author = {Dennis YQ Wang and Luca Cardelli and Andrew Phillips and Nir Piterman and Jasmin Fisher} ,title = {Computational modeling of the EGFR network elucidates control mechanisms regulating signal dynamics} ,journal = {BMC Systems Biology} ,year = {2009} ,volume = {3} ,number = {118} ,pages = {} ,month = {December} ,doi = {http://dx.doi.org/10.1186/1752-0509-3-118} ,abstract = { Background: The epidermal growth factor receptor (EGFR) signaling pathway plays a key role in regulation of cellular growth and development. While highly studied, it is still not fully understood how the signal is orchestrated. One of the reasons for the complexity of this pathway is the extensive network of inter-connected components involved in the signaling. In the aim of identifying critical mechanisms controlling signal transduction we have performed extensive analysis of an executable model of the EGFR pathway using the stochastic pi-calculus as a modeling language. Results: Our analysis, done through simulation of various perturbations, suggests that the EGFR pathway contains regions of functional redundancy in the upstream parts; in the event of low EGF stimulus or partial system failure, this redundancy helps to maintain functional robustness. Downstream parts, like the parts controlling Ras and ERK, have fewer redundancies, and more than 50% inhibition of specific reactions in those parts greatly attenuates signal response. In addition, we suggest an abstract model that captures the main control mechanisms in the pathway. Simulation of this abstract model suggests that without redundancies in the upstream modules, signal transduction through the entire pathway could be attenuated. In terms of specific control mechanisms, we have identified positive feedback loops whose role is to prolong the active state of key components (e.g., MEK-PP, Ras-GTP), and negative feedback loops that help promote signal adaptation and stabilization. Conclusions: The insights gained from simulating this executable model facilitate the formulation of specific hypotheses regarding the control mechanisms of the EGFR signaling, and further substantiate the benefit to construct abstract executable models of large complex biological networks. } } @article{Phillips-Cardelli-Interface09 ,author = {Andrew Phillips and Luca Cardelli} ,title = {A programming language for composable DNA circuits} ,journal = {Journal of the Royal Society Interface} ,year = {2009} ,volume = {6} ,number = {S4} ,pages = {419--436} ,month = {August} ,doi = {} ,abstract = { Recently, a range of information-processing circuits have been implemented in DNA by using strand displacement as their main computational mechanism. Examples include digital logic circuits and catalytic signal amplification circuits that function as efficient molecular detectors. As new paradigms for DNA computation emerge, the development of corresponding languages and tools for these paradigms will help to facilitate the design of DNA circuits and their automatic compilation to nucleotide sequences. We present a programming language for designing and simulating DNA circuits in which strand displacement is the main computational mechanism. The language includes basic elements of sequence domains, toeholds and branch migration, and assumes that strands do not possess any secondary structure. The language is used to model and simulate a variety of circuits, including an entropy-driven catalytic gate, a simple gate motif for synthesizing large-scale circuits and a scheme for implementing an arbitrary system of chemical reactions. The language is a first step towards the design of modelling and simulation tools for DNA strand displacement, which complements the emergence of novel implementation strategies for DNA computing. } } @article{Pedersen-Phillips-Interface09 ,author = {Michael Pedersen and Andrew Phillips} ,title = {Towards programming languages for genetic engineering of living cells} ,journal = {Journal of the Royal Society Interface} ,year = {2009} ,volume = {6} ,number = {S4} ,pages = {437--450} ,month = {August} ,doi = {} ,abstract = { Synthetic biology aims at producing novel biological systems to carry out some desired and well-defined functions. An ultimate dream is to design these systems at a high level of abstraction using engineering-based tools and programming languages, press a button, and have the design translated to DNA sequences that can be synthesized and put to work in living cells. We introduce such a programming language, which allows logical interactions between potentially undetermined proteins and genes to be expressed in a modular manner. Programs can be translated by a compiler into sequences of standard biological parts, a process that relies on logic programming and prototype databases that contain known biological parts and protein interactions. Programs can also be translated to reactions, allowing simulations to be carried out. While current limitations on available data prevent full use of the language in practical applications, the language can be used to develop formal models of synthetic systems, which are otherwise often presented by informal notations. The language can also serve as a concrete proposal on which future language designs can be discussed, and can help to guide the emerging standard of biological parts which so far has focused on biological, rather than logical, properties of parts. } } @inbook{Phillips-SSB09 ,author = {Andrew Phillips} ,editors = {Sriram Iyengar} ,chapter = {A Visual Process Calculus for Biology} ,title = {Symbolic Systems Biology: Theory and Methods} ,year = {} ,month = {} ,isbn = {} ,publisher = {Jones and Bartlett} ,note = {In Press} ,abstract = { This chapter presents a visual process calculus for designing and simulating computer models of biological systems. The calculus is based on a graphical variant of stochastic pi-calculus extended with mobile compartments, and the simulation algorithm is based on standard kinetic theory of physical chemistry. The calculus forms the basis of a formal visual programming language for biology. The basic primitives of the calculus are first introduced by a series of examples involving genes and proteins. More complex features of the calculus are then illustrated by examples involving gene networks, cell differentiation, and immune system response. The main benefit of the calculus is its ability to model large systems incrementally, by directly composing simpler models of subsystems. The formal nature of the calculus also facilitates mathematical analysis of models, which in future could help provide insight into some of the underlying properties of biological systems. } } @article{Cardelli-etal-TCS09 ,author = {Luca Cardelli and Emmanuelle Caron and Philippa Gardner and Ozan Kahramanogullari and Andrew Phillips} ,title = {A Process Model of Rho GTP-binding Proteins} ,journal = {Theoretical Computer Science} ,year = {2009} ,volume = {} ,number = {} ,pages = {} ,month = {} ,doi = {} ,note = {In Press} ,abstract = { Rho GTP-binding proteins play a key role as molecular switches in many cellular activities. In response to extracellular stimuli and with the help from regulators (GEF, GAP, Effector, GDI), these proteins serve as switches that interact with their environment in a complex manner. Based on the structure of a published ordinary differential equations (ODE) model, we first present a generic process model for the Rho GTPbinding proteins, and compare it with the ODE model. We then extend the basic model to include the behaviour of the GDIs and explore the parameter space for the extended model with respect to biological data from the literature. We discuss the challenges this extension brings and the directions of further research. In particular, we present techniques for modular representation and refinement of process models, where, for example, different Rho proteins with different rates for regulator interactions can be given as the instances of the same parametric model. } } @article{Phillips-ENTCS09 ,author = {Andrew Phillips} ,title = {An Abstract Machine for the Stochastic Bioambient Calculus} ,journal = {Electronic Notes in Theoretical Computer Science} ,volume = {227} ,number = {} ,year = {2009} ,month = {January} ,issn = {1571-0661} ,pages = {143--159} ,doi = {http://dx.doi.org/10.1016/j.entcs.2008.12.109} ,publisher = {Elsevier} ,abstract = { This paper presents an abstract machine for the stochastic bioambient calculus. The abstract machine is proved sound and complete with respect to a novel stochastic semantics, and is also shown to preserve the reduction probabilities of the calculus. The machine is implemented as an extension to an existing simulator for stochastic pi-calculus. } } @article{Cardelli-etal-ENTCS09 ,author = {Luca Cardelli and Emmanuelle Caron and Philippa Gardner and Ozan Kahramanogullari and Andrew Phillips} ,title = {A Process Model of Actin Polymerisation} ,journal = {Electronic Notes in Theoretical Computer Science} ,volume = {229} ,number = {1} ,year = {2009} ,month = {January} ,issn = {1571-0661} ,pages = {127--144} ,doi = {http://dx.doi.org/10.1016/j.entcs.2009.02.009} ,publisher = {Elsevier} ,abstract = { Actin is the monomeric subunit of actin filaments which form one of the three major cytoskeletal networks in eukaryotic cells. Actin dynamics, be it the polymerisation of actin monomers into filaments or the reverse process, plays a key role in many cellular activities such as cell motility and phagocytosis. There is a growing number of experimental, theoretical and mathematical studies on the components of actin polymerisation and depolymerisation. However, it remains a challenge to develop compositional models of actin dynamics, e.g., by using differential equations. In this paper, we propose compositional process algebra models of actin polymerisation, and present a geometric representation of these models that allows to generate movies reflecting their dynamics. } } @inproceedings{Mugathan-Phillips-Vigliotti-ACSD08 ,author = {Vinod Mugathan and Andrew Phillips and Maria Vigliotti} ,title = {BAM: BioAmbient Machine} ,booktitle = {Application of Concurrency to System Design} ,year = {2008} ,month = {June} ,issn = {1550-4808} ,pages = {45--49} ,doi = {http://dx.doi.org/10.1109/ACSD.2008.4574594} ,publisher = {IEEE Computer Society} ,abstract = { In recent years it has become clear that techniques developed for concurrent programming are in fact very useful for the analysis of complex systems in biology. To some level of abstraction, it is possible to regard biological phenomena, such as gene transcription, protein interaction and communication among cells, as concurrent entities that compute according to the rules of chemical reactions. In this paper we present a tool for representing and stochastically simulating complex biological systems with mobile compartments. BAM, our tool, implements a stochastic version of the BioAmbient calculus and helps in understanding and reasoning about the multiple interconnections between components in bioregulatory networks. } } @inbook{Phillips-PDPA08 ,author = {Andrew Phillips} ,editors = {Michael Alexander and William Gardner} ,chapter = {Specifying and Implementing Secure Mobile Applications} ,title = {Process Algebra for Parallel and Distributed Processing} ,year = {2008} ,month = {December} ,isbn = {978-1-4200-6486-5} ,publisher = {Chapman & Hall/CRC} } @article{Blossey-Cardelli-Phillips-HFSP08 ,author = {Ralf Blossey and Luca Cardelli and Andrew Phillips} ,title = {Compositionality, Stochasticity and Cooperativity in Dynamic Models of Gene Regulation} ,journal = {HFSP Journal} ,year = {2008} ,month = {February} ,volume = {2} ,number = {1} ,pages = {17--28} ,doi = {http://dx.doi.org/10.2976/1.2804749} ,publisher = {HFSP Publishing} ,abstract = { We present an approach for constructing dynamic models for the simulation of gene regulatory networks from simple computational elements. Each element is called a "gene gate" and defines an input/output-relationship corresponding to the binding and production of transcription factors. The proposed reaction kinetics of the gene gates can be mapped onto stochastic processes and the standard ode-description. While the ode-approach requires fixing the system�s topology before its correct implementation, expressing them in stochastic pi-calculus leads to a fully compositional scheme: network elements become autonomous and only the input/output relationships fix their wiring. The modularity of our approach allows to pass easily from a basic first-level description to refined models which capture more details of the biological system. As an illustrative application we present the stochastic repressilator, an artificial cellular clock, which oscillates readily without any cooperative effects. } } @article{Borgstroem-Gordon-Phillips-ENTCS08 ,author = {Johannes Borgstroem and Andrew Gordon and Andrew Phillips} ,title = {A Chart Semantics for the Pi-calculus} ,journal = {Electronic Notes in Theoretical Computer Science} ,volume = {194} ,number = {2} ,year = {2008} ,month = {January} ,issn = {1571-0661} ,pages = {3--29} ,doi = {http://dx.doi.org/10.1016/j.entcs.2007.11.002} ,publisher = {Elsevier} ,abstract = { We present a graphical semantics for the pi-calculus, that is easier to visualize and better suited to expressing causality and temporal properties than conventional relational semantics. A pi-chart is a finite directed acyclic graph recording a computation in the pi-calculus. Each node represents a process, and each edge either represents a computation step, or a message-passing interaction. Pi-charts enjoy a natural pictorial representation, akin to message sequence charts, in which vertical edges represent control flow and horizontal edges represent data flow based on message passing. A pi-chart represents a single computation starting from its top (the nodes with no ancestors) to its bottom (the nodes with no descendants). Unlike conventional reductions or transitions, the edges in a pi-chart induce ancestry and other causal relations on processes. We give both compositional and operational definitions of pi-charts, and illustrate the additional expressivity afforded by the chart semantics via a series of examples. } } @inproceedings{Phillips-Cardelli-CMSB07 ,author = {Andrew Phillips and Luca Cardelli} ,title = {Efficient, Correct Simulation of Biological Processes in the Stochastic Pi-calculus} ,booktitle = {Computational Methods in Systems Biology} ,year = {2007} ,month = {September} ,publisher = {Springer} ,series = {LNCS} ,volume = {4695} ,pages = {184--199} ,doi = {http://dx.doi.org/10.1007/978-3-540-75140-3_13} ,abstract = { This paper presents a simulation algorithm for the stochastic pi-calculus, designed for the efficient simulation of biological systems with large numbers of molecules. The cost of a simulation depends on the number of species, rather than the number of molecules, resulting in a significant gain in efficiency. The algorithm is proved correct with respect to the calculus, and then used as a basis for implementing the latest version of the SPiM stochastic simulator. The algorithm is also suitable for generating graphical animations of simulations, in order to visualise system dynamics. } } @article{Phillips-Cardelli-Castagna-TCSB06 ,author = {Andrew Phillips and Luca Cardelli and Giuseppe Castagna} ,title = {A Graphical Representation for Biological Processes in the Stochastic Pi-calculus} ,journal = {Transactions in Computational Systems Biology} ,year = {2006} ,month = {November} ,publisher = {Springer} ,series = {LNCS} ,volume = {4230} ,pages = {123--152} ,doi = {http://dx.doi.org/10.1007/11905455_7} ,abstract = { This paper presents a graphical representation for the stochastic pi-calculus, which builds on previous formal and informal notations. The graphical representation is used to model a couple of example biological systems, namely a bistable gene network and a mapk signalling cascade. One of the main benefits of the representation is its ability to highlight the existence of cycles, which are a key feature of many biological systems. Another benefit is its ability to animate interactions between system components, in order to clarify the overall system function. The graphical representation can also be used as a front end to a simulator for the stochastic pi-calculus. This complements the existing textual interface to the simulator, with a view to making modelling and simulation of biological systems more accessible to non computer scientists. } } @article{Blossey-Cardelli-Phillips-TCSB06 ,author = {Ralf Blossey and Luca Cardelli and Andrew Phillips} ,title = {A Compositional Approach to the Stochastic Dynamics of Gene Networks} ,journal = {Transactions in Computational Systems Biology} ,year = {2006} ,month = {January} ,publisher = {Springer} ,series = {LNCS} ,volume = {3939} ,pages = {99--122} ,doi = {http://dx.doi.org/10.1007/11539452_3} ,abstract = { We propose a compositional approach to the dynamics of gene regulatory networks based on the stochastic pi-calculus, and develop a representation of gene network elements which can be used to build complex circuits in a transparent and efficient way. To demonstrate the power of the approach we apply it to several artificial networks, such as the repressilator and combinatorial gene circuits first studied in Combinatorial Synthesis of Genetic Networks [1]. For two examples of the latter systems, we point out how the topology of the circuits and the interplay of the stochastic gate interactions influence the circuit behavior. Our approach may be useful for the testing of biological mechanisms proposed to explain the experimentally observed circuit dynamics. } } @book{2020-Science ,title = {Towards 2020 Science} ,editor = {Stephen Emmott and Ehud Shapiro and Stuart Rison and Andrew Phillips and Andrew Herbert} ,publisher = {Microsoft Research} ,isbn = {0955476100} ,month = {March} ,year = {2006} ,abstract = { This report contains the initial findings and conclusions of a group of internationally distinguished scientists who met over an intense three days in July 2005 to debate and consider the role and future of science over the next 14 years towards 2020, and in particular the importance and impact of computing and computer science on science towards 2020. } } @inproceedings{Phillips-Cardelli-Bioconcur05 ,author = {Andrew Phillips and Luca Cardelli} ,title = {A Graphical Representation for the Stochastic Pi-calculus} ,booktitle = {Concurrent Models in Molecular Biology} ,year = {2005} ,month = {August} ,place = {San Francisco} ,abstract = { This paper presents a graphical representation for the stochastic pi-calculus, which builds on previous formal and informal notations. The graphical representation is used to model a Mapk signalling cascade and an evolved gene network. One of the main benefits of the representation is its ability to clearly highlight the existence of cycles, which are a key aspect of many biological systems. Another advantage is its ability to animate interactions between biological system components, in order to clarify the overall system function. The paper also shows how the graphical representation can be used as a front end to a stochastic simulator for the pi-calculus, in order to allow the direct simulation of graphical models. This complements the existing textual interface of the simulator, with a view to making modelling and simulation of biological systems more accessible to non computer scientists. } } @inproceedings{Phillips-Cardelli-Bioconcur04 ,author = {Andrew Phillips and Luca Cardelli} ,title = {A Correct Abstract Machine for the Stochastic Pi-calculus} ,booktitle = {Concurrent Models in Molecular Biology} ,year = {2004} ,month = {August} ,place = {London} ,abstract = { In this paper, an abstract machine is presented for a variant of the stochastic pi-calculus, in order to correctly model the stochastic simulation of biological processes. The machine is first proved sound and complete with respect to the calculus, and then used as the basis for implementing a stochastic simulator. The correctness of the stochastic machine helps ensure that the simulator is correctly implemented, giving greater confidence in the simulation results. A graphical representation for the pi-calculus is also introduced. } } @inproceedings{Phillips-Yoshida-Eisenbach-Esop04 ,author = {Andrew Phillips and Nobuko Yoshida and Susan Eisenbach} ,title = {A Distributed Abstract Machine for Boxed Ambient Calculi} ,booktitle = {European Symposium on Programming} ,year = {2004} ,month = {April} ,place = {Barcelona} ,series = {LNCS} ,volume = {2986} ,pages = {155--170} ,publisher = {Springer} ,doi = {http://dx.doi.org/10.1007/b96702} ,abstract = { Boxed ambient calculi have been used to model and reason about a wide variety of problems in mobile computing. Recently, several new variants of Boxed Ambients have been proposed, which seek to improve on the original calculus. In spite of these theoretical advances, there has been little research on how such calculi can be correctly implemented in a distributed environment. This paper bridges a gap between theory and implementation by defining a distributed abstract machine for a variant of Boxed Ambients with channels. The abstract machine uses a list semantics, which is close to an implementation language, and a blocking semantics, which leads to an efficient implementation. The machine is proved sound and complete with respect to the underlying calculus. A prototype implementation is also described, together with an application for tracking the location of migrating ambients. The correctness of the machine ensures that the work done in specifying and analysing mobile applications is not lost during their implementation. } } @inproceedings{Phillips-Eisenbach-Lister-FTfJP02 ,author = {Andrew Phillips and Susan Eisenbach and Daniel Lister} ,title = {From Process Algebra to Java Code} ,booktitle = {FTfJP'02} ,year = {2002} ,month = {June} ,place = {M�laga} ,publisher = {http://www.cs.kun.nl/~erikpoll/ftfjp/2002.html} ,abstract = { The delta-pi-calculus, a calculus based on the pi-calculus, is a model for mobile distributed computation. The delta-pi-calculus can be used to specify applications, in order to reason about their security and correctness properties. The delta-pi primitives have been implemented as a Java API. The implementation in Java provides a means of bridging the gap between application specification and implementation. } } @phdthesis{Phillips-Thesis06 ,author = {Andrew Phillips} ,title = {Specifying and Implementing Secure Mobile Applications in the Channel Ambient System} ,school = {Imperial College London} ,year = {2006} ,month = {April} ,abstract = { The Internet has grown substantially in recent years, and an increasing number of applications are now being developed to exploit this distributed infrastructure. Mobility is an important paradigm for such applications, where mobile code is supplied on demand and mobile components interact freely within a given network. However, mobile applications are difficult to develop: not only do they involve complex parallel interactions between multiple components, but they must also satisfy strict security requirements. One could argue that the development of such applications requires a rigorous means of describing and reasoning about mobile computation, through the use of an appropriate model. Foundational research by Cardelli and Gordon on the Ambient Calculus has shown that process calculi are a promising approach to modelling mobile computation. This thesis builds on more recent research in the field of process calculi, and presents a new model of computation known as the Channel Ambient calculus, which can be used both to specify mobile applications and to reason about their security properties. The primitives of the model were developed with real-world applications in mind, and are designed to be at a level of abstraction suitable for an application programmer. The thesis also bridges a gap between theory and implementation by defining a distributed abstract machine for the Channel Ambient calculus. The abstract machine uses a list semantics, which is close to an implementation language, and a blocking semantics, which leads to an efficient implementation. The machine is proved sound and complete with respect to the underlying calculus. A prototype implementation is also described, together with an application for tracking the location of migrating ambients. The correctness of the machine ensures that the work done in specifying and analysing mobile applications is not lost during their implementation.} }