Nano-devices are molecular machines synthesized from molecular subcomponents whose functions are combined in order to perform the func- tion of the machine. It frequently results of relative motions of subcomponents triggered by chemical events such as excitement induced by light, acidity or tem- perature changes. Thus the function consists in the transformation of a chemical event into a mechanical event. An important and characteristic feature of these devices is their intrinsic compositional nature. Therefore process-algebra for- malisms are natural candidates for their modeling. To this aim we introduce a dialect of the -calculus, the nano calculus. It is a rule-based language, the basic agents are molecules, with explicit representa- tion of molecular complexations and internal states. Its stochastic semantics is governed by rules which correspond to chemical reactions. The stochastic rate of the rule, possibly in nite, corresponds to the kinetic rate of the reaction. We illustrated its relevance for the modeling and simulation of nano-devices with an example stemming from the collaboration with the chemistry department of bologna: the [2]RaH rotaxane. We modeled it in nano and simulated its behaviour under various conditions of concentration: rst we validate our model by checking its correspondance with the experimental data and then we investi- gate extreme conditions not observable in practice. We were able to show that some classical assumption about kinetic rates were not correct any longer in this setting. The calculus has many advantages for the modelling of biochemical sys- tems. It is in particular compact, easily reusable and modi able and maybe more importantly much biological-like and thus easier to learn for biochemists. On the other hand the -calculus, also often used to model biochemical sys- tems, has a much more developed theory and more available tools. We present an encoding from the nano calculus to the stochastic -calculus. It satis es a very strong correctness property: S ! T , [[S]] ! [[T]], where S and T are nano terms, is the rate of the reaction and [[:]] is the encoding. Thus it permits to use nano as a front-end formalism and still get the bene ts of the theory and tools of the -calculus. We carry on with a study of the chemical master equation. It probabilisti- cally describes the possible behaviours of the system over time as a di erential equation on the probability to be in a given state at a given instant. It is a key notion in chemistry. There have been many e orts to solve it, and methods such as the Gillespie's algorithm has been developed to simulate its solution. We introduce and motivate a notion of equivalence based on the chemical master equation. It equates state with similar stochastic behavior. Then we prove that this equivalence corresponds exactly to the notion backward stochastic bisimu- lation. This bisimulation di ers from the usual ones because it considers ingoing transitions instead of outgoing transitions. This results is worth in itself since it establishes a bridge between a chemical semantics and a computer semantics, but it is also the rst step towards a metrics for biochemistry. Finally we present an unexpected consequence of our study of the nano calculus. We study the relative expressiveness of the synchronous and asyn- chronous -calculus. In the classical setting the latter is known to be strictly less expressive than the former. We prove that the separation also holds in the stochastic setting. We then extend the result to the -calculi with in nite rates. We also show that under a small restriction the asynchronous -calculus with in nite rates can encode the synchronous -calculus without in nite rates. In- terestingly the separation results are proved using the encodability of the nano calculus. We also propose and motivate a stochastic -calculus with rates of di erent orders of magnitude: the multi-scale -calculus to which we generalize our results. Finally we prove that in the probabilistic settings the asynchronous -calculus can be encoded into the asynchronous one.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00780567 |
| Date | 25 September 2009 |
| Creators | Pradalier, Sylvain |
| Publisher | Ecole Polytechnique X |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | English |
| Type | PhD thesis |
Page generated in 0.0019 seconds