A formal language for nano-devices

A formal language for nano-devices

In this Chapter we investigate the formal description of nano-devices. As detailed in the Chapter 1, the κ-calculus[26] constitutes a good candidate be- cause it has a stochastic semantics, it is rule-based and it permits us to represent explicitly sites and internal states. Moreover it has an efficient simulator and some causality and reachability analysis techniques. However the description of nano-devices does not require the full power of the κ-calculus. So we focus on the study the nanoκ calculus. It is simple and adequate for the description of nano-devices and it retains the good properties of the κ-calculus. Moreover it can also be encoded in the stochastic π-calculus, which permits us to reuse its tools and theory, as we will see in the next Chapter. The Chapter is organized as follows. In Section 3.1, we introduce the syntax and semantics of the nanoκ calculus. In Section 3.2, we present a modeling of the rotaxane in the nanoκ calculus and present several simulations. The Chapter is closed by a conclusion in Section 3.3 and a discussion on related works in Section 3.4. Definition 3.1.1 (nanoκ solutions, nanoκ pre-solutions) The nanoκ calcu- lus uses several sets of names: species ranged over by A, B , C , . . . , fields names ranged over by r, s, t, . . . , sites ranged over by a, b, c, . . . , and bonds names that are totally ordered and countable and ranged over by x, y, z, . . . In order to reflect their biochemical meaning, species, fields and sites are often addressed using strings of characters.

Intuitively, a molecule A[u](σ) is determined by the species A to which it belongs, and its valuation u and its interface σ. The values of the fields in u represent the internal state of the molecule, for instance its electronic charges, or some missing or additional protons. The sites in the interface σ represent the binding capabilities of the molecule. A site a mapped to a bond name x means that a bond, called x, is established between a and a site of some other molecule. A site mapped to the special value ε is free, it is not involved in any bond. For example, if the species A has two fields r and phos and three sites nh, bipy, and 3 the following term is a molecule: A[r 7→ 0; phos 7→ 1](nh 7→ ε; bipy 7→ x; ). The fields r and phos have values 0 and 1, respectively; the site nh is free, the site bipy is bond and the bond is x and this interface does not define the state of the site 3, which may be bond or not. ) (the value ε is always omitted). Let ∅ be the empty map. We write A(σ) instead of A[∅](σ), A[u] instead of A[u](∅), and simply A instead of A[∅](∅). We denote by ran(σ) the range of an interface σ omitting ε and by bonds(S) the set of bonds appearing in the solution S.

We require the set of bond names to be totally ordered in order to ease the building of a finitely branching basic transition relation (see 3.1.5). The countability of the set of bond names is used only for the encoding into the nanoπ-calculus (see the next Chapter and in particular the definition 4.3.1).  or they are in their standard states A and B. We model these possible states using one field e with values −1, 0 and 1 that denote respectively an additional electron, no missing or additional electron and a missing electron. Moreover we model the possible complexation using a site called bond. Formally we can use A[eCreations produce new bonds between two unbound sites and/or synthesize new molecules. Destructions behave in the other way around. Exchanges either leave the interfaces unchanged or move one bond from a reactant to the other, which we call bond-flipping exchange. It is worthwhile to remark that reactions do not address every field and site of the reactants (both hand sides of a rule are pre-solutions). The intended meaning is that two molecules react if they are instances of the left-hand side of a reaction. We will formalize this notion later on in the basic transition relation (see definition 3.1.5 ). Stochastic semantics of the nanoκ calculus. We can now present the stochastic semantics of nanoκ. As we anticipated in the Chapter 2, it is achieved in several steps: first we build the basic transition relation, then the collective transition relation is derived from the basic one and finally the resulting IMC is downgraded into a CTMC, assuming that our system meets the strictly Marko- vian property.