<!DOCTYPE article PUBLIC "-//NLM//DTD JATS (Z39.96) Journal Archiving and Interchange DTD v1.0 20120330//EN" "JATS-archivearticle1.dtd">
<article xmlns:xlink="http://www.w3.org/1999/xlink">
  <front>
    <journal-meta />
    <article-meta>
      <title-group>
        <article-title>Combinatorial Strand Algebra in Insertion Modeling System</article-title>
      </title-group>
      <contrib-group>
        <contrib contrib-type="author">
          <string-name>Dmitriy M. Klionov</string-name>
          <xref ref-type="aff" rid="aff0">0</xref>
        </contrib>
        <contrib contrib-type="editor">
          <string-name>Key Terms: Computation, Model, InsertionModeling, Algebra.</string-name>
        </contrib>
        <aff id="aff0">
          <label>0</label>
          <institution>Kherson State University</institution>
          ,
          <addr-line>40 rokiv Zhovtnya st. 27, Kherson</addr-line>
          ,
          <country country="UA">Ukraine</country>
        </aff>
      </contrib-group>
      <fpage>102</fpage>
      <lpage>111</lpage>
      <abstract>
        <p>This article is focused on the Insertion Modeling System developed by A.A. Letichevsky of the department 100/105 of the Glushkov Institute of Cybernetics, National Academy of Science of Ukraine, Kyiv, Ukraine Insertion Modeling System (IMS)[1] is buit on the Algebraic Programming System (APS) that also was developed by A.A. Letichevsky in 1987. and on the way of implementation of strand algebras - a process algebra for DNA computing devised by Luca Cardelli in order to compile other formal systems into the algebra, and compilation of this algebra into DNA structures. We focus on the basic strand algebra - combinatorial strand algebra, which is equivalent to the place-transition Petri nets, and on the version of the model driver of the Insertion Modeling System, based on the Petri nets.</p>
      </abstract>
      <kwd-group>
        <kwd>insertion modeling</kwd>
        <kwd>system biology</kwd>
        <kwd>strand algebras</kwd>
      </kwd-group>
    </article-meta>
  </front>
  <body>
    <sec id="sec-1">
      <title>-</title>
      <p>DNA technology is reaching the point where one can envision automatically
compiling high-level formalisms to DNA computational structures [11]. There are
three compilation processes for concurrent languages, described by Cardelli in
paper[10]. First, is the compilation of a low-level combinatorial algebra to a certain
class of composable DNA structures [12]: this is intended to be a direct (but not quite
trivial) mapping, which provides an algebraic notation for writing concurrent
molecular programs. Second, is the compilation of a higher-level expression-based
algebra to the lower-level combinatorial algebra, as a paradigm for compiling
expressions of arbitrary complexity to `assembly language' DNA combinators. Third
is translating concurrent interacting automata [13] to molecular structures. There is no
clear way to implement such system, because one must decompose concurrent
communication patterns into a form suitable for molecular interactions (a quadratic
process that is described in [13]), and then one must find some suitable `general
programmable matter' as a physical substrate. Some solution of this problem, based
on the combinatorial DNA algebra, was given by Cardelli in paper[10].</p>
      <p>Process algebras are formal languages designed to describe and analyze the
concurrent activities of multiple processes. The standard technical presentation of
process algebras was initially inspired by a chemical metaphor [14], and it is therefore
natural, as a tutorial, to see how the chemistry of diluted well-mixed solutions can
itself be presented as a process algebra. Having chemistry in this form also facilitates
relating it to other process algebras.</p>
      <p>Take a set C of chemical solutions denoted by P,Q,R. Two binary relations are
defined on this set. The first relation, mixing, P  Q is an equivalence relation: its
purpose is to describe reversible events that amount to `chemical mixing'; that is, to
bringing components close to each other (syntactically) so that they can conveniently
react by the second relation. Its basic algebraic laws are the commutative monoid
laws of + and 0, where + is the chemical combination symbol and 0 represents the
empty solution. The second relation, reaction, P  Q , describes how a (sub-) solution
P becomes a different solution Q. A reaction P  Q operates under a dilution
assumption; namely, that adding some R to P does not make it then impossible for P
to become Q (although R may enable additional reactions that overall quantitatively
repress by interfering with P). The two relations of mixing and reaction are connected
by a rule that says that the solution is well mixed: for any reaction to happen it is
sufficient to mix the solution so that the reagents can interact. In first instance, the
reaction relation does not have chemical rates. However, from the initial solution,
from the rates of the base reactions, and from the relation  describing
wholesystem transitions, one can generate a continuous time Markov chain representing the
kinetics of the system. In terms of system evolution, it is also useful to consider the
symmetric and transitive closure,  , representing sequences of reactions.</p>
      <p>As process algebra, chemistry therefore obeys the following general laws, shown
lower:</p>
    </sec>
    <sec id="sec-2">
      <title>Equivalence</title>
    </sec>
    <sec id="sec-3">
      <title>Congruence</title>
    </sec>
    <sec id="sec-4">
      <title>Diffusion</title>
    </sec>
    <sec id="sec-5">
      <title>Dilusion well mixing</title>
      <p>P  P; P  Q  Q  P; P  Q,Q  R  P  R</p>
      <p>P  Q  P  R  Q  R
P  Q  Q  P; P  (Q  R)  (P  Q)  R; P  0  P</p>
      <p>
        P  Q  P  R  Q  R
P  P', P' Q',Q'  Q  P  Q
(
        <xref ref-type="bibr" rid="ref1">1</xref>
        )
(
        <xref ref-type="bibr" rid="ref2">2</xref>
        )
(
        <xref ref-type="bibr" rid="ref3">3</xref>
        )
(
        <xref ref-type="bibr" rid="ref4">4</xref>
        )
(
        <xref ref-type="bibr" rid="ref5">5</xref>
        )
      </p>
      <p>Algebra is about equations, but in process algebra equations are usually a derived
concept. Instead of axiomatizing a set of equations, we can use the reaction relation to
study the equations that hold in a given algebra, meaning that P  Q holds if P and Q
produce the same reactions [15]. The complexity of these derived equational theories
varies with the algebra. A simple instance here is the equation P + 0 = P, whose
validity requires verifying that in definition of  there is no reaction for 0, nor for 0
combined with something else.</p>
      <p>This way, chemistry can be presented as process algebra. But the algebra of
chemical `+' is one among many: there are other process algebras that can suit
biochemistry more directly [16,17] or, that can suit DNA computing. In the same way
the strand algebra represent DNA strands, DNA gates and operations among them
allowing the higher-level formalisms to be compiled to the DNA structures. I this
paper we will show the way to represent the simplest strand algebra – combinatorial
strand algebra as insertion model for the Insertion Modeling System[1], using the fact
that combinatorial strand algebra is equivalent to place transition Petri nets. There is a
representation of Petri nets, given by A.A. Letichevsky in form of insertion machines.
We use this representation in order to build a specified analytical model driver for the
combinatorial strand algebra.</p>
      <sec id="sec-5-1">
        <title>2 Insertion Modeling System</title>
        <p>2.1</p>
        <sec id="sec-5-1-1">
          <title>The Architecture of Insertion Modeling System</title>
          <p>Insertion Modeling System(IMS) [1] developed by A.A. Letichevsky of the Glushkov
Institute of Cybernetics, National Academy of Science of Ukraine, Kyiv, Ukraine.
Insertion modeling is the technology of system design founded on the theory of
interaction of agents and environments. It is based on process algebra and is intended
for the unification of different models of interaction and computation (such as CCS,
CSP, π- calculus, mobile ambients etc.).</p>
          <p>Insertion model of a system represent this system as a composition of environment
and agents inserted into it. The insertion function is usually denoted as E[u] were E is
the state of environment and u is the state of an agent. E[u] is a new environment state
after insertion an agent u. All agents and environments are labeled or attributed
transition systems (labeled systems with states labeled by attribute labels [9]). The
states of transition systems are considered up to bisimilarity. The main invariant of
bisimilarity is the behavior beh[E] of transition system in the state E (an oriented tree
with edges labeled by actions and nodes labeled by attribute labels). Behaviors
themselves can be considered as states of transition systems.</p>
          <p>The general architecture of insertion machine is represented on the fig. 1.</p>
          <p>The main component of insertion machine is model driver, the component which
controls the machine movement along the behavior tree of a model. The state of a
model is represented as a text in the input language of insertion machine and is
considered as an algebraic expression. The input language include the recursive
definitions of agent behaviors, the notation for insertion function, and possibly some
compositions for environment states. The state of a system must be reduced to the
form E[u1,u2,...] . This functionality is performed by the module called agent behavior
unfolder.</p>
          <p>Two kinds of insertion machines are considered: real type or interactive and
analytical insertion machines. The first ones exist in the real or virtual environment,
interacting with it in the real or virtual time. Analytical machines intended for model
analyses, investigation of its properties, solving problems etc. The drivers for two
kinds of machines correspondingly are also divided on interactive and analytical
drivers.</p>
          <p>Insertion machine with interactive driver operates as an agent inserted into external
environment with insertion function defining the laws of functioning of this
environment.</p>
          <p>Interactive driver can be organized in a rather complex way. If it has criteria of
successful functioning in external environment intellectual driver can accumulate the
information about its past, develop the models of external environment, improve the
algorithms of selecting actions to increase the level of successful functioning.</p>
          <p>Analytical insertion machine as opposed to interactive one can consider different
variants of making decision about performed actions, returning to choice points (as in
logic programming) and consider different paths in the behavior tree of a model. The
model of a system can include the model of external environment of this system, and
the driver performance depends on the goals of insertion machine. In the general case
analytical machine solves the problems by search of states, having the corresponding
properties(goal states) or states in which given safety properties are violated.</p>
        </sec>
        <sec id="sec-5-1-2">
          <title>2.2 The Decomposition of Petri Nets into the Composition of Agents and</title>
        </sec>
        <sec id="sec-5-1-3">
          <title>Environments</title>
          <p>Petri net (place/transition net) is one of several mathematical modeling languages for
the description of distributed systems. A Petri net is a directed bipartite graph, in
which the nodes represent transitions (i.e. events that may occur, signified by bars),
and places (i.e. conditions, signified by circles). The directed arcs describe which
places are pre/and/or postconditions for which transitions (signified by arrows). Like
the industry standards such as UML activity diagrams, BPMN and EPCs, Petri nets
offer graphical notation for stepwise processes that include choice, iteration, and
concurrent execution. Unlike these standards, Petri nets have an exact mathematical
definition of their execution semantics, with a well-developed theory for process
analysis.</p>
          <p>A Petri net consists of places, transitions, and arcs. Arcs run from a place to
transition or vice versa, newer between places or between transitions. The places from
which an arc runs to a transition are called the input places of the transition; the places
to which arcs run from a transition are called the output places of the transition.
Places in a Petri net may contain a discrete number of marks called tokens. Any
distribution of tokens over the places will represent a configuration of the net called a
marking. In abstract sense relating to Petri nets diagram, a transition of a Petri net
may fire whenever there are sufficient tokens at the start of all input arcs; when it
fires, it consumes this tokens, and places them at the end of all output arcs. A firing is
atomic, i.e., a single non-interruptible step.</p>
          <p>Execution of Petri nets s nondeterministic: when multiple transitions are enabled at
the same time, any of them may fire, so multiple tokens may be represented anywhere
in the net (even in the same place). Petri nets are well suited for modeling the
concurrent behavior of distributed systems.</p>
          <p>Petri nets are formally defined as a state-transition systems that extend a class of
nets called elementary nets. Formal definition is represented lower.</p>
          <p>1. P is a set of states, called places.
2. T is a set of transitions
3. F where F  (P  T )  (T  P) is a set of relations called arcs
4. N  (P,T , F ) is a net
5. C is such that C  P is a configuration
6. M so that M : P  Z is a place multiset, where Z is a countable set.
7. W so that W : F  Z is an arc multiset
8. PN  (N , M ,W ) is a Petri net</p>
          <p>Fig 2. Formal definition of Petri net.</p>
          <p>Petri net is bipartite graph, where P is one partition and T is the other. Moreover,
for every t in T there exist p and q in P so that (p, t) and (t, q) are in F, and for every p
and q in P, if (p, t) and (t, q) are in F then p≠q.</p>
          <p>The set are the new elements. The set of places define the local states of a net,
however, the global state of a net can be defined by place subsets.</p>
          <p>In order to represent Petri nets as a composition of agents and environments, we
represent transitions T as actions, tokens as agents, and places as states. The behavior
of tokens located in the enabled place s is written as:
u(s) </p>
          <p>
             t.
W (s,t)0
(
            <xref ref-type="bibr" rid="ref6">6</xref>
            )
          </p>
          <p>The states of Petri environment are equal to the marks (configurations) of the net.</p>
          <p>M : S  Nat  E(M ) || {u(s) |M (s)| s  S}
The insertion function is defined as:</p>
        </sec>
      </sec>
    </sec>
    <sec id="sec-6">
      <title>The environment transitions are defined as:</title>
      <p>
        E(M )[u]  E(M ) || u
u tu'
E[u] t E[u']
(
        <xref ref-type="bibr" rid="ref7">7</xref>
        )
(
        <xref ref-type="bibr" rid="ref8">8</xref>
        )
(
        <xref ref-type="bibr" rid="ref9">9</xref>
        )
3
      </p>
      <sec id="sec-6-1">
        <title>Combinatorial Strand Algebra</title>
        <p>Strand algebra is a process algebra [18] where the main components represent DNA
strands, DNA gates, and their interactions. The basic algebra is non-deterministic
algebra, and the further extension is a stochastic variant [10]. Strand algebras may
look very similar to either chemical reactions, or Petri nets, or multiset-rewriting
systems. The difference here is that the equivalent of, respectively, reactions,
transitions, and rewrites, do not live outside the system, but rather are part of the
system itself and are consumed by their own activity, reflecting their DNA
implementation. A process algebra formulation is particularly appropriate for such an
internal representation of active elements.</p>
        <p>The Combinatorial Strand Algebra, P – basic strand algebra has some atomic
elements (signals and gates), and only two combinators: parallel (concurrent)
composition P | Q , and populations P . An inexhaustible population P has the
property that P  P | P* ; that is, there is always one more P that can be taken from the
population. The set P is formally the set of finite trees P generated by the syntax
shown below; we freely use parentheses when representing these trees linearly as
strings. Up to the algebraic equations described below, each P is a multiset, i.e., a
solution. The signals x,y,... are taken from a countable set.</p>
        <p>
          P :: x;[x1,..., xn ].[ y1,..., ym ];0; P1 | P2; Pn  1, m  0
(
          <xref ref-type="bibr" rid="ref10">10</xref>
          )
        </p>
        <p>A gate is an operator from signals to signals: [x1,..., xn ].[ y1,..., ym ] is a gate that
binds signals x1,..., xn , produces signals y1,..., ym , and is consumed in the process. We
say that this gate joins n signals and then forks m signals; some special cases are
shown on the fig 4. An inert component is indicated by 0. Signals and gates can be
combined into a `soup' by parallel composition P1 | P2 (a commutative and associative
operator, similar to chemical `+'), and can also be assembled into inexhaustible
populations, P . Square brackets are omitted for single inputs or outputs.
Explanation of the Syntax and Abbreviations:</p>
      </sec>
    </sec>
    <sec id="sec-7">
      <title>Signal</title>
    </sec>
    <sec id="sec-8">
      <title>Inert</title>
      <p>transduser gate</p>
    </sec>
    <sec id="sec-9">
      <title>Composition fork gate</title>
    </sec>
    <sec id="sec-10">
      <title>Population x 0</title>
      <p>P1 | P2</p>
      <p>P</p>
      <p>
        P  P
x1.x2 ≜
[x1].[x2]
x.[x1,..., xm ] ≜ [x].[x1,..., xm ]
[x1,..., xm ].x ≜ [x1,..., xm ].[x]
(
        <xref ref-type="bibr" rid="ref11">11</xref>
        )
(
        <xref ref-type="bibr" rid="ref12">12</xref>
        )
(
        <xref ref-type="bibr" rid="ref13">13</xref>
        )
(14)
(
        <xref ref-type="bibr" rid="ref14">15</xref>
        )
(
        <xref ref-type="bibr" rid="ref15">16</xref>
        )
(
        <xref ref-type="bibr" rid="ref16">17</xref>
        )
(
        <xref ref-type="bibr" rid="ref17">18</xref>
        )
population
      </p>
    </sec>
    <sec id="sec-11">
      <title>Diffusion</title>
      <p>P  Q  P  Q
P  Q,Q  R  P  R</p>
      <p>P  P | P
P | 0  P
0*  0</p>
      <p>P | Q  Q | P
(P | Q)*  P | Q*
P | (Q | R)  (P | Q) | R</p>
      <p>P  P
The relation</p>
      <p> P  P , called reaction, is the smallest relation satisfying the
following properties. In addition,  , reaction sequence, is the symmetric and
transitive closure of  . Reaction is shown lower:</p>
      <p>x1 | .. | xn | [x1,..., xn ].[ y1,..., ym ]  y1 | .. | ym gate n  1, m  0</p>
    </sec>
    <sec id="sec-12">
      <title>Dilution</title>
      <p>P  Q  P | R  Q | R</p>
      <p>P  P', P' Q',Q'  Q  P  Q
well mixing</p>
      <p>The first reaction (gate) forms the core of the semantics: the other rules allow
reactions to happen in context. Note that the special case of the gate rule for m = 0 is
x1 | .. | xn | [x1,..., xn ].[]  0 . And, in particular, x.[] annihilates an x signal. We can
choose any association of operators in the formal gate rule: because of the
associativity of parallel composition under the exact choice is not important. Since
is a relation, reactions are in general nondeterministic.
(20)
(21)
(22)
(23)
(24)
(25)
(26)
(27)
(28)
(29)
(30)
(31)</p>
      <p>Note that signals can interact with gates but signals cannot interact with signals,
nor gates with gates. As we shall see, in the DNA implementation the input part of a
gate is the Watson-Crick dual of the corresponding signal strand, so that the inputs are
always `negative' and the outputs are always `positive'. This Watson-Crick duality
need not be exposed in the syntax: it is implicit in the separation between signals and
gates, so we use the same x1 both for the `positive' signal strand and for the
complementary `negative' gate input in a reaction like x1 | x1.x2  x2 .</p>
      <sec id="sec-12-1">
        <title>4 Insertion Machine for Combinatorial Strand Algebra</title>
        <p>The representation of Petri nets as a composition of agents and environments was
discussed in section 2.2. This will allow us to build a model driver based on the Petri
nets. Consider a place-transition Petri Net with places xi; then, a transition with
incoming arcs from places x1..xn ,and outgoing arcs to places y1..ym is represented in
the combinatorial strand algebra as ([x1..xn ].[ y1..ym ]) , where an unbounded
population of gates ensures that the transition can fire repeatedly. The initial token
marking x1,..., xk (a multiset of places) is represented as x1 | .. | xk . Conversely, a
signal in strand algebra can be represented as a marked place in a Petri net, and a gate
[x1,...xn ].[ y1..ym ] as a transition with an additional marked `one-shot' place on the
input that makes it fire only once; then, P can be represented by connecting the
transitions of P to refresh the one-shot places (this was suggested by Cosimo Laneve).
Therefore, the combinatorial strand algebra is equivalent to place-transition Petri nets,
and can be easily implemented into the Insertion Modeling System, by using the
model driver based on the Petri nets.</p>
      </sec>
      <sec id="sec-12-2">
        <title>Conclusions</title>
        <p>Strand algebras in general would allow the compilation of a high-level formalism into
the DNA structures, using the methods advised by Cardelli in [10]. We have shown
the way of implementation of the basic strand algebra – combinatorial strand algebra,
in the Insertion Modeling System, by constructing the model driver for the system,
based on the Petri nets. Combinatorial strand algebra deals with countable sets of
signals/gates and so on(as well as Petri nets), we can extend it in future, to make it
able to handle infinite sets, using the possibilities of insertion modeling, that works
with infinite models. Implementation of combinatorial strand algebra to the insertion
modeling system can be considered as the first step for building the insertion models
of biological systems. However the further extensions of combinatorial strand
algebra: Nested strand algebra [6], and Stochastic strand algebra, require a
constructing of a probabilistic model driver, in order to implement them in the
Insertion Modeling System. The stochastic semantics can be taken for example from
the Stochastic Petri nets, which are just nets with rates on transitions and with an
induced Continuous Time Markov Chain semantics.</p>
      </sec>
    </sec>
  </body>
  <back>
    <ref-list>
      <ref id="ref1">
        <mixed-citation>
          1.
          <string-name>
            <given-names>Alexander</given-names>
            <surname>Letichevsky</surname>
          </string-name>
          , Olexander Letichevskyi, Vladimir Peschanenko,
          <article-title>Igor Blinov and Dmitriy Klionov: (en) Insertion Modeling System And Constraint Programming</article-title>
          . In: Ermolayev,
          <string-name>
            <surname>V.</surname>
          </string-name>
          et al.
          <source>(eds.) Proc. 7-th Int. Conf. ICTERI</source>
          <year>2011</year>
          , Kherson, Ukraine, May 4-
          <issue>7</issue>
          ,
          <year>2011</year>
          , CEUR-WS.org/Vol-
          <volume>716</volume>
          , ISSN 1613-
          <issue>0073</issue>
          , pp.
          <fpage>51</fpage>
          -
          <lpage>64</lpage>
          (
          <year>2011</year>
          ), http://ceur-ws.
          <source>org/Vol716</source>
        </mixed-citation>
      </ref>
      <ref id="ref2">
        <mixed-citation>
          2.
          <string-name>
            <surname>Gilbert</surname>
            <given-names>D.R.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Letichevsky</surname>
            <given-names>A.A.</given-names>
          </string-name>
          :
          <article-title>A universal interpreter for nondeterministic concurrent programming languages</article-title>
          .In M. Gabbrielli (eds.),
          <article-title>Fifth Compulog network area meeting on language design and semantic analysis methods (</article-title>
          <year>1996</year>
          ).
        </mixed-citation>
      </ref>
      <ref id="ref3">
        <mixed-citation>
          3.
          <string-name>
            <surname>Letichevsky</surname>
            <given-names>A.A.</given-names>
          </string-name>
          ,
          <string-name>
            <given-names>D.R.</given-names>
            <surname>Gilbert</surname>
          </string-name>
          :
          <article-title>A general theory of action languages</article-title>
          .
          <source>Cybernetics and System Analyses</source>
          , vol.
          <volume>1</volume>
          , pp.
          <fpage>16</fpage>
          --
          <lpage>36</lpage>
          (
          <year>1998</year>
          ).
        </mixed-citation>
      </ref>
      <ref id="ref4">
        <mixed-citation>
          4.
          <string-name>
            <surname>Letichevsky</surname>
            <given-names>A.A.</given-names>
          </string-name>
          and
          <string-name>
            <surname>Gilbert D.R.:</surname>
          </string-name>
          <article-title>A Model for Interaction of Agents and Environments</article-title>
          . In D. Bert,
          <string-name>
            <given-names>C.</given-names>
            <surname>Choppy</surname>
          </string-name>
          , P. Moses, (eds.).
          <source>Recent Trends in Algebraic Development Techniques. LNCS</source>
          , vol.
          <year>1827</year>
          , pp.
          <fpage>11</fpage>
          --
          <lpage>58</lpage>
          . Springer (
          <year>1999</year>
          ).
        </mixed-citation>
      </ref>
      <ref id="ref5">
        <mixed-citation>
          5.
          <string-name>
            <surname>Letichevsky</surname>
            <given-names>A.A.</given-names>
          </string-name>
          :
          <article-title>Algebra of behavior transformations and its applications</article-title>
          . In V.B.
          <string-name>
            <surname>Kudryavtsev</surname>
            and
            <given-names>I.G</given-names>
          </string-name>
          .Rosenberg (eds).
          <source>Structural theory of Automata</source>
          , Semigroups, and
          <source>Universal Algebra, NATO Science Series II. Mathematics, Physics and Chemistry</source>
          , vol.
          <volume>207</volume>
          , pp.
          <fpage>241</fpage>
          --
          <lpage>272</lpage>
          . Springer (
          <year>2005</year>
          ).
        </mixed-citation>
      </ref>
      <ref id="ref6">
        <mixed-citation>
          6.
          <string-name>
            <surname>Baranov</surname>
            <given-names>S.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Jervis</surname>
            <given-names>C.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Kotlyarov</surname>
            <given-names>V.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Letichevsky</surname>
            <given-names>A.</given-names>
          </string-name>
          , and
          <string-name>
            <surname>Weigert</surname>
            <given-names>T.</given-names>
          </string-name>
          :
          <article-title>Leveraging UML to Deliver Correct Telecom Applications</article-title>
          . In L. Lavagno, G. Martin,
          <string-name>
            <surname>B.</surname>
          </string-name>
          Selic (eds.).
          <article-title>UML for Real: Design of Embedded Real-Time Systems</article-title>
          . Kluwer Academic Publishers. Amsterdam (
          <year>2003</year>
          ).
        </mixed-citation>
      </ref>
      <ref id="ref7">
        <mixed-citation>
          7.
          <string-name>
            <surname>Letichevsky</surname>
            <given-names>A.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Kapitonova</surname>
            <given-names>J.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Letichevsky</surname>
            <given-names>A.</given-names>
          </string-name>
          <string-name>
            <surname>Jr.</surname>
          </string-name>
          ,
          <string-name>
            <surname>Volkov</surname>
            <given-names>V.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Baranov</surname>
            <given-names>S.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Kotlyarov</surname>
            <given-names>V.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Weigert</surname>
            <given-names>T.</given-names>
          </string-name>
          :
          <article-title>Basic Protocols, Message Sequence Charts, and the Verification of Requirements Specifications</article-title>
          .
          <source>Computer Networks</source>
          , vol.
          <volume>47</volume>
          ,
          <fpage>662</fpage>
          -
          <lpage>675</lpage>
          (
          <year>2005</year>
          ).
        </mixed-citation>
      </ref>
      <ref id="ref8">
        <mixed-citation>
          8.
          <string-name>
            <surname>Kapitonova</surname>
            <given-names>J.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Letichevsky</surname>
            <given-names>A.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Volkov</surname>
            <given-names>V.</given-names>
          </string-name>
          , and
          <string-name>
            <surname>Weigert</surname>
            <given-names>T.</given-names>
          </string-name>
          :
          <article-title>Validation of Embedded Systems</article-title>
          . In R. Zurawski, (eds.).
          <source>The Embedded Systems Handbook</source>
          , CRC Press, Miami (
          <year>2005</year>
          ).
        </mixed-citation>
      </ref>
      <ref id="ref9">
        <mixed-citation>
          9.
          <string-name>
            <surname>Letichevsky</surname>
            <given-names>A.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Kapitonova</surname>
            <given-names>J.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Volkov</surname>
            <given-names>V.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Letichevsky</surname>
            <given-names>A.</given-names>
          </string-name>
          , jr.,
          <string-name>
            <surname>Baranov</surname>
            <given-names>S.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Kotlyarov</surname>
            <given-names>V.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Weigert</surname>
            <given-names>T.</given-names>
          </string-name>
          :
          <article-title>System Specification with Basic Protocols</article-title>
          .
          <source>Cybernetics and System Analyses</source>
          , vol.
          <volume>4</volume>
          , pp.
          <fpage>479</fpage>
          --
          <lpage>493</lpage>
          (
          <year>2005</year>
          ).
        </mixed-citation>
      </ref>
      <ref id="ref10">
        <mixed-citation>
          10.Cardelli L.:
          <article-title>Strand Algebras for DNA Computing (Preliminary version)</article-title>
          .
          <source>DNA Computing and Molecular Programming</source>
          ,
          <source>15th International Conference, DNA 15. LNCS</source>
          <volume>5877</volume>
          :
          <fpage>12</fpage>
          -
          <lpage>24</lpage>
          , Springer (
          <year>2009</year>
          ).
        </mixed-citation>
      </ref>
      <ref id="ref11">
        <mixed-citation>
          11.
          <string-name>
            <given-names>P.</given-names>
            <surname>Yin</surname>
          </string-name>
          ,
          <string-name>
            <given-names>H. M.T.</given-names>
            <surname>Choi</surname>
          </string-name>
          ,
          <string-name>
            <surname>Calvert</surname>
            <given-names>C.R.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Pierce</surname>
            <given-names>N.A.</given-names>
          </string-name>
          :
          <article-title>Programming Biomolecular Selfassembly Pathways</article-title>
          .
          <source>Nature</source>
          ,
          <volume>451</volume>
          :
          <fpage>318</fpage>
          -
          <lpage>322</lpage>
          (
          <year>2008</year>
          ).
        </mixed-citation>
      </ref>
      <ref id="ref12">
        <mixed-citation>
          12.
          <string-name>
            <surname>Soloveichik</surname>
            <given-names>D.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Seelig</surname>
            <given-names>G.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Winfree</surname>
            <given-names>E.</given-names>
          </string-name>
          :
          <article-title>DNA as a Universal Substrate for Chemical Kinetics</article-title>
          .
          <source>PNAS, March</source>
          <volume>4</volume>
          ,
          <year>2010</year>
          , doi: 10.1073/pnas.0909380107.
        </mixed-citation>
      </ref>
      <ref id="ref13">
        <mixed-citation>
          13.Cardelli L.:
          <article-title>On Process Rate Semantics</article-title>
          .
          <source>Theoretical Computer Science</source>
          <volume>391</volume>
          (
          <issue>3</issue>
          )
          <fpage>190</fpage>
          -
          <lpage>215</lpage>
          ,
          <fpage>14</fpage>
          .
          <string-name>
            <surname>Marathe</surname>
            <given-names>A.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Condon</surname>
            <given-names>A.E.</given-names>
          </string-name>
          ,
          <string-name>
            <given-names>R.M.</given-names>
            :
            <surname>Corn</surname>
          </string-name>
          .
          <article-title>On Combinatorial DNA Word Design</article-title>
          .
          <source>J. Comp. Biology</source>
          <volume>8</volume>
          (
          <issue>3</issue>
          ), vol. pp.
          <fpage>201</fpage>
          --
          <lpage>219</lpage>
          , (
          <year>2001</year>
          ).
        </mixed-citation>
      </ref>
      <ref id="ref14">
        <mixed-citation>
          15.
          <string-name>
            <surname>Milner</surname>
            <given-names>R.</given-names>
          </string-name>
          :
          <source>Communicating and Mobile Systems: The π-Calculus</source>
          . Cambridge University Press (
          <year>1999</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref15">
        <mixed-citation>
          16.
          <string-name>
            <surname>Danos</surname>
            <given-names>V.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Laneve</surname>
            <given-names>C.</given-names>
          </string-name>
          :
          <article-title>Formal molecular biology</article-title>
          .
          <source>Theoretical Computer Science</source>
          <volume>325</volume>
          (
          <issue>1</issue>
          ) pp.
          <fpage>69</fpage>
          -
          <lpage>110</lpage>
          (
          <year>2004</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref16">
        <mixed-citation>
          17.
          <string-name>
            <surname>Regev</surname>
            <given-names>A.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Panina</surname>
            <given-names>E.M.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Silverman</surname>
            <given-names>W.</given-names>
          </string-name>
          , Cardelli L.,
          <string-name>
            <surname>Shapiro</surname>
            <given-names>E.:</given-names>
          </string-name>
          <article-title>BioAmbients: An Abstraction for Biological Compartments</article-title>
          .
          <source>Theoretical Computer Science</source>
          , vol.
          <volume>325</volume>
          (
          <issue>1</issue>
          ), pp.
          <fpage>141</fpage>
          --
          <lpage>167</lpage>
          (
          <year>2004</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref17">
        <mixed-citation>
          18. Cardelli L.:
          <article-title>Artificial Biochemistry</article-title>
          . In: A.
          <string-name>
            <surname>Condon</surname>
            ,
            <given-names>D.</given-names>
          </string-name>
          <string-name>
            <surname>Harel</surname>
            ,
            <given-names>J.N.</given-names>
          </string-name>
          <string-name>
            <surname>Kok</surname>
            ,
            <given-names>A.</given-names>
          </string-name>
          <string-name>
            <surname>Salomaa</surname>
          </string-name>
          , E.Winfree (eds.).
          <source>Algorithmic Bioprocesses</source>
          . Springer (
          <year>2009</year>
          )
        </mixed-citation>
      </ref>
    </ref-list>
  </back>
</article>