Formal Verification of Programs in Molecular Models with Random Access Memory

Formal Verification of Programs in Molecular Models with Random Access Memory MARIO J. PÉREZ-JIMÉNEZ FERNANDO SANCHO-CAPARRINI Dpto. Ciencias de la Computación e Inteligencia Artificial Universidad de Sevilla, E.T.S. Ingeniería Informática Avda. Reina Mercedes, s/n – 41012 Sevilla, Spain E-mail: {Mario.Perez,Fernando.Sancho}@cs.us.es Abstract Formal verification of molecular programs is a first step towards their automatic processing by means of reasoning systems (ACL2, PVS, etc). In this paper a systematic method to establish verifications of these programs within molecular models with memory, that is, molecular computing models where some operations modifying the inner structure of molecules exist, is proposed. The method presented in this work is applied to relevant problems for the design of molecular programs solving some well-known numerical NP-complete problems: the Generating Cover Families problem, the Set Covering problem and the Minimal Set Cover Selection Problem. M. J. Pérez-Jiménez et al. (Eds.): Recent Results in Natural Computing, pp. 205–229 c The Authors c Fénix Editora 206 Formal Verification of Programs in Molecular Models... 1 Introduction Since the first result in molecular computing at the end of 1994 [1], some solutions to several NP-complete problems in this framework have been offered. In 1995 the first molecular models appeared. They are universal models, that is, with the same computational power as Turing Machines. Since then, it appears the possibility of designing molecular programs having as input the instance of the problem to solve (until then, molecular computing was limited to solve particular instances, with no description of molecular operations in general cases). However, this brings about the necessity of a greater flexibility in the design of the programs and the necessity of a formal verification of the fact that those programs effectively solve the problem for which they were designed. Usually, the first step to solve a concrete problem in computing models is to encode the input of the problem into the type of data that the model deals with (in this case, encoding will be made by means of tubes containing DNA molecules); next step consists in applying a finite sequence of basic operations of the model to the input data to get an output encoding the solution of the problem. The goal of this paper is the presentation of a methodology to establish a formal verification of programs in molecular models with memory. The method is applied to molecular programs solving several wellknown numerical NP-complete problems: the Generating Cover Families problem, the Set Covering problem, and the Minimal Set Cover problem. The problems we solve in this work are associated with a finite family, F, of subsets of a finite set. And they are the following ones: (1) generate every ordered pair (F0, B)such that F0is a subfamily of F and B=∪F0; (2) generate all pairwise disjoint subfamilies of F. The paper is organized as follows: in section 2 a methodology to establish a formal verification of programs in molecular models with memory is given. Section 3 summarizes the main characteristics of the molecular model we use in this work: the Sticker Model. Sections 4 and 5 apply this methodology to two numerical problems. The main reason why we have chosen the above problems is because there exists a qualitative difference in the way their formal verification have been established. On one hand, all the molecules of the input tube are kept M. J. PÉREZ-JIMÉNEZ, F. SANCHO-CAPARRINI 207 (possibly modified) along the execution of the program; on the other hand, a filtering process is made, hence some molecules are thrown away because they do not encode any of the valid solutions to the problem. 2 A Methodology for Verification of Programs within Models with Memory Let Pbe a program within a molecular model designed to solve a problem X. Let us suppose that the program Phas a main loop FOR or WHILE (we will say that Pis a FOR or WHILE program). To verify (X, P)we will search formulas, in the variables of the program, that are invariant of the main loop and such that, at the end of the execution, can help us to deduce the soundness and completeness of Pfor the problem X. The execution of the program Pcan be interpreted as the evolution over time of a certain population. At the beginning of the execution the population consists of a multiset of molecules forming the input tube of P. Every molecule represents an element, thus, in the original population cloned members can exist. Every step of the main loop takes one unit of time. Hence, throughout the execution an element of the population can die (that is, it can be thrown away) or it can survive. If the molecular computing model has random access memory (that is, if the inner structure of the molecules can be modified) then the molecules surviving all the steps can be of two kinds: those whose inner structure has been altered and those that remain with no modifications. The study of invariant formulas of the main loop needs a detailed study of every molecule in the input tube. First we proceed to a relabelling of the tubes used in the program in order to individualize them and to distinguish and characterize the relevant tubes along the execution. Second, a function showing the evolution of every molecule, σ, in every step, i, of the main loop is defined. This function can be undefined for some values (σ, i). This will be interpreted as the fact that the molecule σdoes not survive after the execution of i-th step of the loop. The methodology we propose to verify (X, P)consists of the following stages: 208 Formal Verification of Programs in Molecular Models... 1. Re-labelling of the tubes of the program P, to individualize them along the execution. 2. A detailed follow-up of the evolution of every molecule along the process, using a function that we will name STEP . 3. Searching invariant formulas of the main loop based on the STEP function properties. 4. Deducing the Soundness (every molecule in the output tube encodes a valid solution of the problem) and the Completeness (every molecule in the input tube encoding a valid solution of the problem must be in the output tube) of the program based on invariant formulas after the execution of the program. 3 The Sticker Model The sticker model was introduced by S. Roweis, E. Winfree et al [6] as an abstract model of molecular computing based on DNA, with random access memory. In this model the information is represented in a different way from that used in the Adleman-Lipton paradigm. An (n, k, m)-memory strand, with n≥k·m, consists of a strand of nbases subdivided into knon-overlapping substrands each of which is mbases long. A sticker associated with an (n, k, m)-memory strand is mbases long and complementary to exactly one of the ksubstrands of the memory strand. If a sticker is annealed to its matching substrand on a memory strand, then the particular substrand is said to be on, if not it is said to be off. An (n, k, m)-memory complex is an (n, k, m)-memory strand along with its annealed stickers (if any). The (n, k, m)-memory complexes represent bit strings of {0,1}k, for this reason, it is usual to identify them either as binary functions (σ:{1, ..., k} −→ {0,1}, such that σ(i) = 1 if and only if the i-th substrand is on), or as subsets of {1, ..., k}by means of their characteristic functions. Within the sticker model, a tube is a finite multiset (a collection where elements can be repeated) of memory complexes. In this paper we use the following operations of the sticker model over tubes: M. J. PÉREZ-JIMÉNEZ, F. SANCHO-CAPARRINI 209 •Combine(T1, T2): given two test tubes T1and T2this operation produces a new tube, denoted by T1∪T2, the multiset union of T1 and T2. •Separate(T, i): given a test tube Tand a natural number i, with 1≤i≤k, this operation produces two new tubes, +(T, i) = {{σ∈T:σ(i) = 1}} and −(T, i) = {{σ∈T:σ(i) = 0}}. We usually write (T1, T2)←separate(T, i)to indicate that T1= +(T, i)and T2=−(T, i). •Set(T, i): given a test tube Tand a natural number i, with 1≤ i≤k, this operation produces a new tube, Set(T, i), where the ith substrand of each memory complex in Tis turned on. •Read(T): given a test tube Tthis operation reads the content of tube T. To achieve that, one memory complex has to be isolated from Tand its annealed stickers determined, or else it has to be reported that the tube Tcontains no memory complexes. Note that, in this model, the operations Separate and Set are the only ones implementing a massive parallelism. Also, only operation Set can modify inner structure of the molecules of a tube. A(k, l)-library, with 1≤l≤k, consists of all memory complexes with ksubstrands, where the first lsubstrands are either on or off, in all possible ways, whereas the last k−lsubstrands are off. In the sticker model a program, P, is a finite sequence of molecular operations that can be written in a simple way by means of robotic operations (such as loops, conditionals, etc.). 4 The Generating Cover Families Problem The Generating Cover Families problem is the following: Let A={1, . . . , p}. Let F={B1, . . . , Bq}be a finite family of subsets of A. Determine all ordered pairs (F0, B), where F0is a subfamily of Fand B=SF0. 210 Formal Verification of Programs in Molecular Models... 4.1 Design of a Program in the Sticker Model To solve this problem we consider as the input tube, T0, a (p+q, q)- library encoding all possible subfamilies of F. If ρis a memory complex with p+qsubstrands (from now on, we will say that ρis a molecule), we will note: ρq= (ρ(1), . . . , ρ(q)) ρp= (ρ(q+ 1), . . . , ρ(q+p)) We can interpret that molecule ρencodes an ordered pair, (Fρ, Aρ), where Fρis a subfamily of Fand Aρis a subset of A, according to the following: Fρ={Bk∈ F : 1 ≤k≤q∧ρ(k) = 1} Aρ={s∈A: 1 ≤s≤p∧ρ(q+s) = 1} Definition 1. Let ρbe a molecule and let tbe such that 1≤t≤q+p. We will say that t∈ρ(resp. t /∈ρ) if and only if ρ(t) = 1 (resp. ρ(t) = 0). If ρis a molecule, then we have: [Fρ={xj k: 1 ≤k≤q∧1≤j≤rk∧k∈ρ} Definition 2. A molecule ρis consistent if and only if Aρ=SFρ. A molecular program solving the Generating Cover Families problem is the following: Procedure Cover Input: T0(where T0is a (p+q, q)-library) for i= 1 to qdo (T+ i, T− i)←separate(T0, i) for j= 1 to rido set(T+ i, q +xj i) end for T0←combine(T+ i, T− i) end for Where, for each i(1 ≤i≤q)we denote by rithe cardinality of the set Bi, and Bi={x1 i, . . . , xri i}. The number of molecular operations in this program is of the order of O(q·p). M. J. PÉREZ-JIMÉNEZ, F. SANCHO-CAPARRINI 211 4.2 Formal Verification In order to establish a formal verification of this molecular program we proceed to a re-labelling of the used tubes: Procedure Cover Input: T0(where T0isa(p+q, q)-library) for i= 1 to qdo (T+ i, T− i)←separate(Ti−1, i) T∗ i,0←T+ i for j= 1 to rido T∗ i,j ←set(T∗ i,j−1, q +xj i) end for Ti←combine(T∗ i,ri, T− i) end for Obviously, this program is equivalent to the above one in the following sense: both have the same input tubes, T0, and produce output tubes (T0and Tq, respectively) with the same content. We want to note that the semantic of this program is very close to the semantic of the problem it solves. Hence, the problems that appear when trying to establish its formal verification are mainly due to the use of molecular operations that modify the inner structure of the molecules (i.e. set operation), making it harder the analysis of their track along the execution. Next, we define a function, namely STEP, that captures the evolution of each molecule after the execution of a step of the main loop. Definition 3. Let ibe such that 1≤i≤q. Let ρ∈Ti−1. We define STEP(ρ, i)as follows: STEP(ρ, i) = ρ , if i /∈ρ ρ∪(q+Bi),if i∈ρ Where q+Bi={q+xj i: 1 ≤j≤ri}. Note that if τ=STEP (ρ, i)then ρq=τqand ρ⊆τ. Moreover, the function STEP is a total function; that is, it is defined over all possible input data. 212 Formal Verification of Programs in Molecular Models... Lemma 1. ∀i(1 ≤i≤q→ ∀ ρ∈Ti−1(ST EP(ρ, i)∈Ti)) Proof. Let ibe such that 1≤i≤q, and let ρ∈Ti−1. •If i /∈ρ, then ρ∈ −(Ti−1, i) = T− i⊆Ti, and since STEP(ρ, i) = ρ, we deduce that STEP(ρ, i)∈Ti. •If i∈ρ, we define recursively ρ(j), for each 0≤j≤rias follows: –ρ(0) =ρ. –ρ(j+1) =ρ(j)∪ {q+xj+1 i}. Let us see that ∀j(0 ≤j≤ri→ρ(j)∈T∗ i,j). By induction on j. –The case j= 0 is trivial because ρ(0) =ρ∈+(Ti−1, i) = T+ i=T∗ i,0. –Let j < risuch that ρ(j)∈T∗ i,j. From definition of ρ(j+1) we deduce that ρ(j+1) ∈set(T∗ i,j, q +xj+1 i) = T∗ i,j+1. Since ρ(ri)=STEP(ρ, i), we obtain that STEP(ρ, i)∈T∗ i,ri⊆Ti. Definition 4. Let σ∈T0. We define recursively σi, with 0≤i≤q, as follows: σi=σ , if i= 0 STEP(σi−1, i),if 1≤i≤q From Lemma 1 it follows that σi∈Ti, for each 0≤i≤q. Lemma 2. For each i,jsuch that 1≤i≤qand 1≤j≤riwe have ∀τ∈T∗ i,j ∃ρ∈T+ i(τ=ρ∪(q+Bj i)), where Bj i={x1 i, . . . , xj i}. Proof. For a given i, the proof can be deduced by induction on jfollowing the semantic structure of the program. Corollary 1. Let ibe such that 1≤i≤q. Then for every molecule τ∈T∗ i,ri there exists a molecule ρ∈Ti−1verifying i∈ρand STEP (ρ, i) = τ. Proof. Let ibe such that 1≤i≤q. Let τ∈T∗ i,ri. From Lemma 2 (with j=ri) we deduce that there exists ρ∈T+ i= +(Ti−1, i)such that τ=ρ∪(q+Bj i). Then, ρ∈Ti−1and i∈ρ. Hence, STEP(ρ, i) = τ. M. J. PÉREZ-JIMÉNEZ, F. SANCHO-CAPARRINI 213 4.3 Soundness of the Program We have to prove that every molecule in the output tube, Tq, encodes a valid solution of the problem. That is, if τ∈Tq, then τqencodes a subfamily, Fτ, of Fand τpencodes a subset, Aτ, of A, such that Aτ= SFτ. In other words, we have to prove that every molecule, τ, in the output tube, Tq, is consistent. To prove the soundness of the program we consider the following formula θ(i) ∀τ∈Ti[∀k(1 ≤k≤i∧k∈τ→(q+Bk)⊆τ)∧ ∧ ∀ s(1 ≤s≤p∧(q+s)∈τ→ ∃ k∈τ(1 ≤k≤i∧s∈Bk))] That is, the formula θ(i)(with i > 0) means that after the execution of the i-th step of main loop, all molecules, τ, verifying Aτ=S{Br∈ Fτ: 1≤r≤i}are in the tube Ti. For the case i= 0 we suppose that B0=∅. Theorem 1. The formula θ(i)is an invariant of the main loop. That is, ∀i(0 ≤i≤q→θ(i)) Proof. By induction on i. The case i= 0 is trivial. Let i < q be such that the formula θ(i)is true. Let τ∈Ti+1 =T∗ i+1,ri+1 ∪T− i+1. •If τ∈T− i+1, then τ∈Ti∧i+ 1 /∈τ. In this case we have τ∈Ti and i+ 1 /∈τ. As τ∈Ti, from the induction hypothesis we obtain that (a) ∀k(1 ≤k≤i∧k∈τ→(q+Bk)⊆τ) (b) ∀s(1 ≤s≤p∧(q+s)∈τ→ ∃ k∈τ(1 ≤k≤i∧s∈Bk))] Having in mind that i+ 1 /∈τwe have (a’) ∀k(1 ≤k≤i+ 1 ∧k∈τ→(q+Bk)⊆τ) From (b)we directly obtain (b’) ∀s(1 ≤s≤p∧(q+s)∈τ→ ∃ k∈τ(1 ≤k≤i+ 1 ∧s∈ Bk))] So, the formula θ(i+ 1) is true. •If τ∈T∗ i+1,ri+1 , from Corollary 1 we deduce that there exists ρ∈Ti such that ρ∈Tiverifying i+ 1 ∈ρand STEP(ρ, i + 1) = τ. Then τ=ρ∪(q+Bi+1). 220 Formal Verification of Programs in Molecular Models... Input: T0 T−1,0←T0;T−1,1← ∅;T0,1←T0;T∗ 0,1← ∅ For i←0to q−1do Ti,i+2 ← ∅ For j←ito 0do T+ i,j ←+(Ti−1,j, i + 1) Ti,j+1 ←combine(T+ i,j, T∗ i,j+1) T∗ i,j ← −(Ti−1,j, i + 1) Ti,0←T∗ i,0 if Tq−1,1is nonempty Read Tq−1,1 else Read Tq−1,2 else Read Tq−1,3 . . . else Read Tq−1,q Obviously, this program is equivalent to the above one in the following sense: both have the same input tubes, T0, and produce output tubes (T0, . . . , Tq, and Tq−1,0, . . . , Tq−1,q respectively) such that the contents of the tubes Tiand Tq−1,i (for i= 0, . . . , q) are the same. This program produces i+ 1 tubes (Ti,i+1, . . . , Ti,0)after the execution of the i-th step of the main loop, as Figure 1 illustrates. T T T T T T T T TT T T T T T 0 0,0 0,1 1,0 1,1 1,2 2,0 2,1 2,2 2,3 3,0 3,1 3,2 3,3 3,4 Combine Combine Combine Combine Combine Combine - ++ + + + -+ + + + + - - - - - -- - i=1 i=3 i=2 i=0 Separate Separate Separate Separate 1 2 3 4 Figure 1. Labelled merge-binary tree. That is, the execution of this program can be described as a rooted directed graph with depth qthat we will call as labelled merge-binary tree with depth q, and that can be defined as follows: M. J. PÉREZ-JIMÉNEZ, F. SANCHO-CAPARRINI 221 Definition 5. A grid with depth h,Gh= (Vh, Eh), is the following directed graph: Vh={(i, j) : 0 ≤i≤h∧0≤j≤i} Eh={((i, j),(i+ 1, j)),((i, j),(i+ 1, j + 1)) : 0 ≤i < h ∧0≤j≤i} Definition 6. A labelled merge-binary tree with depth his a tuple (Gh, L, {Fi: 0 ≤i≤h−1}, B, T0, l) where: •Ghis a grid with depth h. •Lis a nonempty set (its elements will be called labels). •For each i(with 0≤i≤h−1) Fiis a function from Lto L×L (we will note Fi= (F− i, F+ i)). •Bis a binary function from L×Lto L. •T0belongs to L(that is, T0is a label). •lis a function from Vhto L, called the labelling function, defined by recursion (using T0, Fiand B), as follows:            l(0,0) = T0 l(i+ 1,0) = F− i(l(i, 0)) l(i+ 1, i + 1) = F+ i(l(i, i)) l(i+ 1, j) = B(F− i(l(i, j −1)), F+ i(l(i, j))) with 0≤i < h and 1≤j≤i. In the execution of the designed molecular program a labelled merge-binary tree with depth qis obtained, where: (a) The labels are the tubes. (b) For each i(with 0≤i≤q−1) we have Fi(T) = separate(T, i+1). So, F− i(T) = −(T, i + 1) and F+ i(T) = +(T, i + 1) 222 Formal Verification of Programs in Molecular Models... (c) The binary function, B, is the combine molecular operation (called merge too). (d) T0is the input test–tube of the subroutine. This combinatorics structure allows us to design a subroutine solving a more general sorting problem, where the semantic of the subroutine is very close to the semantic of the problem ([3]). To establish the formal verification of the subroutine, in connection with the Minimal Set Cover Selection problem, we have to prove specifically that: •Every molecule, σ, in the output tube, Tq−1,r (with 1≤r≤q), verifies |σ|=r(Soundness). •Every molecule, σ, in the input tube, T0, such that |σ|=r(with 1≤r≤q), is in the output tube Tq−1,r (Completeness). The execution of the subroutine can be seen as an evolution of a population of elements. Initially, the population is determined by the multiset of molecules in the input tube, T0. Every molecule is an individual, and repeated ones can exist at the same time (so cloned members can be alive simultaneously in this population). Every step of the main loop can be interpreted as a time unit. After a lapse, the population is transformed into another one, but, in this case, there is no death or mutation in elements, since this subroutine is, basically, a filtering procedure. We consider the following formulas: ψ(i, 0) ≡ ∀σ(σ∈Ti,0↔σ∈T0∧ ∀k(1 ≤k≤i+ 1 →k /∈σ)) ψ(i, j + 1) ≡ ∀σ(σ∈Ti,j+1 ↔(σ∈Ti−1,j ∧i+ 1 ∈σ)∨ ∨(σ∈Ti−1,j+1 ∧i+ 1 /∈σ)) θ(i)≡ ∀j(0 ≤j≤i+ 1 →ψ(i, j)) Theorem 5. The formula θ(i)is an invariant of the main loop. That is, ∀i(0 ≤i≤q−1→θ(i)). Proof. By induction on i. •The result is true for i= 0. The formula ψ(0,0) is true because M. J. PÉREZ-JIMÉNEZ, F. SANCHO-CAPARRINI 223 σ∈T0,0⇐⇒ σ∈T∗ 0,0=−(T−1,0,1) = −(T0,1) ⇐⇒ σ∈T0∧1/∈σ⇐⇒ σ∈T0∧ ∀ k(1 ≤k≤0+1→k /∈σ). The formula ψ(0,1) is true because σ∈T0,1⇐⇒ σ∈T+ 0,0∪T∗ 0,1=T+ 0,0= +(T−1,0,1) ⇐⇒ σ∈ T−1,0∧1∈σ⇐⇒ (σ∈T−1,0∧1∈σ)∨(σ∈T−1,1∧1/∈σ). •Let i < q −1such that the formula θ(i)is true. Let us see that the formula θ(i+ 1) is true; that is, ∀j(0 ≤j≤i+ 2 →ψ(i+ 1, j). –For j= 0 we have the following: σ∈Ti+1,0⇐⇒ σ∈T∗ i+1,0⇐⇒ σ∈ −(Ti,0, i + 2) ⇐⇒ σ∈ Ti,0∧i+ 2 /∈σ⇐⇒ σ∈T0∧ ∀ k(1 ≤k≤i+ 1 →k /∈ σ)∧i+ 2 /∈σ⇐⇒ σ∈T0∧ ∀ k(1 ≤k≤i+ 2 →k /∈σ). –Let j≤i+ 2 such that j > 0and let us see that ψ(i+ 1, j)is true. Indeed: σ∈Ti+1,j ⇐⇒ σ∈T+ i+1,j−1∪T∗ i+1,j ⇐⇒ σ∈+(Ti,j−1)∪ −(Ti,j, i+2) ⇐⇒ (σ∈Ti,j−1∧i+2 ∈σ)∨(σ∈Ti,j ∧i+2 /∈σ). Next, we describe the trace of every molecule in the input tube along the execution of the subroutine. For this, if σ∈T0is given, we will write σ= (i1, . . . , ir)to note that 1≤i1<· · · < ir≤qand ∀j(1 ≤j≤r→σ(ij) = 1) ∧ ∀ t∀j(1 ≤t≤q∧ij6=t→σ(t) = 0) That is, the molecule σ= (i1, . . . , ir)∈T0encodes in a natural way the subfamily F0={Bi1, . . . , Bir}of F. Proposition 1. Let σ= (i1, . . . , ir)∈T0, where 1≤i1< i2<· · · < ir≤ q. Then (1) ∀j(1 ≤j≤r→σ∈Tij−1,j). (2) ∀t(1 ≤t≤q−ir→σ∈Tir+t−1,r). (3) σ∈Tq−1,r. 224 Formal Verification of Programs in Molecular Models... Proof. 1. By induction on j. •First, we consider the case j= 1. –If i1= 1 then Ti1−1,1=T0,1=T0. So, σ∈Ti1−1,1. –If i1>1then we prove that ∀s(1 ≤s<i1→σ∈ Ts−1,0). Indeed: ∗Let sbe such that 1≤s < i1. Then, σ∈T0∧ ∀ k(1 ≤ k≤s−1 + 1 →k /∈σ). As s−1≥0the formula ψ(s−1,0) is true, so we deduce that σ∈Ts−1,0. From 1≤i1−1< i1we obtain that σ∈T(i1−1)−1,0. As i1∈σwe have σ∈+(Ti1−2,0, i1). Then σ∈Ti1−2,0,i1∈ σ, and the formula ψ(i1−1,1) is true. Hence, σ∈Ti1−1,1. •Let jbe such that 1≤j < r. Let us suppose that σ∈Tij−1,j. We have to prove that σ∈Tij+1−1,j+1. –If ij+1 −1 = ij(that is, ij+1 =ij+ 1), from induction hypothesis we have σ∈Tij−1,j and ij+1 ∈σ. That is, σ∈Tij−1,j and ij+1 ∈σ. As formula ψ(ij+1 −1, j+1) ≡ ψ(ij, j + 1) is true, we deduce that σ∈Tij+1−1,j+1. –If ij+1 −1> ijwe prove that ∀t(1 ≤t≤ij+1 −ij−1→ σ∈Tij+t−1,j), by induction on t. ∗We have σ∈Tij−1,j and ij+ 1 /∈σ. As formula ψ(ij, j)is true (and j > 0) we obtain that σ∈Tij,j. That is, σ∈Tij+1−1,j. So, the result is true for t= 1. ∗Let tbe such that t < ij+1 −ij−1and let us suppose the result holds for t. Then, σ∈Tij+t−1,j. As ij< ij+t+ 1 < ij+1, we have ij+t+ 1 /∈σ. Having in mind that the formula ψ(ij+t, j)is true, we conclude that σ∈Tij+t,j. That is, σ∈Tij+(t+1)−1,j. Now, let us see that σ∈Tij+1−1,j+1. Applying the above relation for t=ij+1 −ij−1,σ∈Tij+(ij+1−ij−1)−1,j = Tij+1−2,j. As ij+1 ∈σand the formula ψ(ij+1 −1, j + 1) is true we deduce that σ∈Tij+1−1,j+1. 2. By induction on t. M. J. PÉREZ-JIMÉNEZ, F. SANCHO-CAPARRINI 225 •For t= 1 we have that 1≤q−ir, that is, ir+ 1 ≤q. From (1) we obtain that σ∈Tir−1,r. But ir+1 /∈σ. As formula ψ(ir, r) is true we conclude that σ∈Tir,r. That is, σ∈Tir+1−1,r. •Let tbe such that 1≤t<q−ir, and let us suppose that σ∈Tir+t−1,r. As ir< ir+t+ 1 ≤qwe have ir+t+ 1 /∈ σ. Taking into account that the formula ψ(ir+t, r)is true (because ir+t≤q−1), we conclude that σ∈Tir+t,r. That is, σ∈Tir+(t+1)−1,r. 3. Applying the result obtained in (2), considering t=q−ir, we deduce that σ∈Tir+(q−ir)−1,r =Tq−1,r. Next we will prove that the generated tubes after i-th step of the main loop, {Ti,0, Ti,1, . . . , Ti,i+1}, form a partition of the initial test tube, T0. This confirms that the subroutine runs a filtering procedure where no strand dies along the execution. Proposition 2. ∀i(0 ≤i≤q−1→T0=S0≤j≤i+1 Ti,j). Proof. Let us first prove that ∀i(0 ≤i≤q−1→T0⊆S0≤j≤i+1 Ti,j). By induction on i. •Let σ∈T0. Then (σ∈T0∧1∈σ)∨(σ∈T0∧1/∈σ). So, (σ∈T0∧1∈σ) =⇒(σ∈T−1,0∧1∈σ) =⇒σ∈T0,1 (σ∈T0∧1/∈σ) =⇒σ∈T0,0 Hence σ∈T0,1∪T0,0⊆S0≤j≤1T0,j. •Let i < q −1be such that T0⊆S0≤j≤i+1 Ti,j. Let σ∈T0. From induction hypothesis, there exists jsuch that 0≤j≤i+ 1 and σ∈Ti,j. Then (σ∈Ti,j ∧i+ 2 ∈σ)∨(σ∈Ti,j ∧i+ 2 /∈σ). –Let us suppose that σ∈Ti,j and i+ 2 ∈σ. As formula ψ(i+1, j +1) is true we deduce that σ∈Ti+1,j+1 ⊆S0≤s≤i+2 Ti+1,s. –Let us suppose that σ∈Ti,j and i+ 2 /∈σ 226 Formal Verification of Programs in Molecular Models... ∗If j= 0 then σ∈Ti,0and i+ 2 /∈σ. But σ∈Ti,0=⇒σ∈ T0∧ ∀ k(1 ≤k≤i+ 1 →k /∈σ). So, σ∈T0∧ ∀ k(1 ≤ k≤i+ 2 →k /∈σ). As formula ψ(i+ 1,0) is true, we deduce that σ∈Ti+1,0⊆S0≤s≤i+2 Ti+1,s. ∗If j > 0, taking into account that σ∈Ti,j ∧i+ 2 /∈σ and the formula ψ(i+ 1, j)is true, we conclude that σ∈ Ti+1,j. That is, σ∈S0≤s≤i+2 Ti+1,s. Now, let us see that ∀i(0 ≤i≤q−1→S0≤j≤i+1 Ti,j ⊆T0). For that, it is enough to prove that ∀i∀j(0 ≤i≤q−1∧0≤j≤i+1 →Ti,j ⊆T0). By induction on i. •The result holds for i= 0. Indeed: T0,0=T∗ 0,0=−(T−1,0,1) = −(T0,1) ⊆T0 T0,1=T+ 0,0∪T∗ 0,1=T+ 0,0= +(T−1,0,1) = +(T0,1) ⊆T0 •Let i < q −1be such that ∀j(0 ≤j≤i+ 1 →Ti,j ⊆T0). Let us see that ∀j(0 ≤j≤i+ 2 →Ti+1,j ⊆T0). –If j= 0 then Ti+1,0=T∗ i+1,0=−(Ti,0, i+2) = −(Ti,0, i+2) h.i. ⊆ T0. –If j > 0(and j≤i+ 2) then we have: Ti+1,j =T∗ i+1,j−1∪ T∗ i+1,j = +(Ti,j−1, i + 2) ∪ −(Ti,j, i + 2) ⊆Ti,j−1∪Ti,j. Taking into account that j≤i+ 1 =⇒Ti,j−1∪Ti,j ⊆T0 j=i+ 2 =⇒Ti,j−1∪Ti,j =Ti,i+1 ∪Ti,i+2 =Ti,i+1 ⊆T0 we conclude that Ti+1,j ⊆T0. Proposition 3. ∀i(0 ≤i≤q−1→ ∀r∀s(0 ≤r < s ≤i+ 1 → Ti,r ∩Ti,s =∅)). Proof. By induction on i. •The result holds for i= 0 because T0,0∩T0,1=T∗ 0,0∩T0,1=−(T−1,0,1) ∩+(T−1,0,1) = ∅. M. J. PÉREZ-JIMÉNEZ, F. SANCHO-CAPARRINI 227 •Let i < q −1be such that ∀r∀s(0 ≤r < s ≤i+ 1 →Ti,r ∩ Ti,s =∅). Let r, s be such that 0≤r < s ≤i+ 2. Let us see that Ti+1,r ∩Ti+1,s =∅. –Let us suppose that s=i+ 2. If there exists τ∈Ti+1,r ∩Ti+1,i+2 then τ∈Ti+1,i+2 =⇒(τ∈Ti,i+1 ∧i+ 2 ∈τ)∨ (τ∈Ti,i+2 ∧i+ 2 /∈τ) =⇒(τ∈Ti,i+1 ∧i+ 2 ∈τ) But τ∈Ti+1,0=⇒τ∈T0∧ ∀ k(1 ≤k≤i+ 2 →k /∈τ), and i+ 2 ∈τ. So, r > 0. Then, τ∈Ti+1,r =⇒τ∈Ti,r−1. Hence, Ti,i+1 ∩Ti,r−16=∅. This contradicts our assumption. –Let us suppose that r= 0 and 1≤s≤i+ 1. If there exists τ∈Ti+1,0∩Ti+1,s then τ∈Ti+1,0=⇒τ∈T0∧ ∀ k(1 ≤k≤i+ 2 →k /∈τ) =⇒τ∈Ti,0∧ ∀ k(1 ≤k≤i+ 2 →k /∈τ) τ∈Ti+1,s =⇒(τ∈Ti,s−1∧ ≤ i+ 2 ∈τ)∨ (τ∈Ti,s ∧i+ 2 /∈τ) So, τ∈Ti,0∩Ti,s. This contradicts the induction hypotesis (because 0< s ≤i+ 1). –Let us suppose that r > 0and 1≤s≤i+ 1. If there exists τ∈Ti+1,r ∩Ti+1,s then τ∈Ti+1,r =⇒(τ∈Ti,r−1∧i+ 2 ∈τ)∨ (τ∈Ti,r ∧i+ 2 /∈τ) τ∈Ti+1,s =⇒(τ∈Ti,s−1∧i+ 2 ∈τ)∨ (τ∈Ti,s ∧i+ 2 /∈τ) If i+ 2 ∈τthen Ti,r−1∩Ti,s−16=∅, which contradicts the induction hypothesis. If i+2 /∈τthen Ti,r∩Ti,s 6=∅, which contradicts the induction hypothesis. 228 Formal Verification of Programs in Molecular Models... Corollary 6. Tq−1,0=∅. Proof. Let us suppose that Tq−1,06=∅. Then there exists σ= (i1, . . . , ir) ∈Tq−1,0, with r > 0. From Proposition 1.(3) we have σ∈Tq−1,r. So, Tq−1,0∩Tq−1,r 6=∅, which contradicts Proposition 3. Finally, we establish the soundness and the completeness of the designed subroutine that solves the Minimal Set Cover Selection problem. Theorem 6. (Soundness) Every strand, σ, in the final test–tube, Tq−1,r (with 1≤r≤q), verifies that its length is r. That is, ∀r(1 ≤r≤q→ ∀σ∈ Tq−1,r(|σ|=r)). Proof. Let rbe such that 1≤r≤q. Let σ∈Tq−1,r. From Proposition 2 we obtain that σ∈T0. From Proposition 1.(3), we have σ∈Tq−1,|σ|. From Proposition 3 we conclude that |σ|=r. Theorem 7. (Completeness) Every strand, σ, in the initial test–tube, T0, with length ris in the output tube, Tq−1,r. That is, ∀σ∈T0(|σ|=r→ σ∈Tq−1,r). Moreover, ∀σ∈T0∃!r(1 ≤r≤q∧σ∈Tq−1,r). Proof. Let σ∈T0such that |σ|=r. From Proposition 1.(3) we can deduce that σ∈Tq−1,r. In the other hand, from Proposition 3 (with i=q−1) there exists jsuch that 0≤j≤i+ 1 and σ∈Tq−1,j. From Corollary 1 we obtain j > 0, and from Proposition 3 we conclude that j is unique. 7 Conclusions A methodology to establish the formal verification of FOR or W HILE programs within molecular computing models with random access memory has been presented. The search of invariant formulas of the main loop needs a detailed study of the evolution of every molecule along the execution of the program. A function called ST EP has been introduced to capture the evolution of the molecules after one step of the main loop. These solutions are applied to solve some numerical NP-complete problems: the Generating Cover Families problem, the Set Covering problem and the Minimal Set Cover Selection Problem. The problems we M. J. PÉREZ-JIMÉNEZ, F. SANCHO-CAPARRINI 229 have chosen in this paper present some interesting and different characteristics with respect to the STEP function. We think that the study of the formal verification of molecular programs is a necessary step for their automatic processing by means of reasoning systems (we are currently working on ACL2 and PVS). Acknowledgement The support for this research through the project TIC2002-04220-C0301 of the Ministerio de Ciencia y Tecnología of Spain, cofinanced by FEDER funds, is gratefully acknowledged. References [1] Adleman, L. Molecular Computation of Solutions to Combinatorial Problems, Science,268 (1994), 1021–1024. [2] Garey, M. R.; Johnson, D. S. Computers and intractability, W. H. Freeman and Company, New York, 1979. [3] Pérez-Jiménez, M. J.; Sancho-Caparrini, F. Solving Knapsack Problems in a Sticker Based Model, in Jonoska, N.; Seeman, N. (eds.), DNA Computing, LNCS 2340 (2002), 161–171. [4] Hoare, C. A. R. An axiomatic basis for computer programming, Communications of the ACM,12 (1969), 576–583. [5] Pérez-Jiménez, M. J.; Sancho-Caparrini, F. Minimal Set Cover Problem: On a DNA solution of selection stage, in Martín-Vide, C.; P˘aun, Gh. (eds.), Pre-Proceedings of Workshop on Membrane Computing, RGML Report 17/01 (2001), 251–258. [6] Roweis, S.; Winfree, E.; Burgoyne, R.; Chelyapov, N.; Goodman, M.; Rothemund, P.; Adleman, L. A Sticker–Based Model for DNA Computation, Journal of Computational Biology,5, 4 (1998), 615–629.