Using Automated Reasoning Systems on Molecular Computing

Using Automated Reasoning Systems on Molecular Computing Carmen Graciani D´ıaz and Mario J. P´erez-Jim´enez Research Group on Natural Computing, Dpto. Ciencias de la Computaci´on e Inteligencia Artificial, Universidad de Sevilla (Spain) {cgdiaz, marper}@us.es Abstract. This paper is focused on the interplay between automated reasoning systems (as theoretical and formal devices to study the correctness of a program) and DNA computing (as practical devices to handle DNA strands to solve classical hard problems with laboratory techniques). To illustrate this work we have proven in the PVS proof checker, the correctness of a program, in a sticker based model for DNA computation, solving the pairwise disjoint families problem. Also we introduce the formalization of the Floyd–Hoare logic for imperative programs. 1 Introduction One of the most active areas of research in Computer Science is the study and use of formal methods (applications of primarily discrete mathematics to software engineering problems). Its widely development and the complexity of interesting problems have given rise to automated reasoning. In this area, one of the main problems is the correctness [2]: developing specifications and proofs that ensures a program meets its specification. There is a previous work of formalization: expressing all definitions, theorems and proofs in a formal language without semantic ambiguity. This approximation has especial relevance in new computing paradigms such as the DNA based molecular computing. In many molecular models the data are tubes over an alphabet whose content encodes a collection of DNA strands. The operations considered are abstraction of different laboratory techniques to manipulate DNA strands. This paper is organized as follows. It begins with a short presentation of the Prototype Verification System (PVS) and the sticker model. Then, how this model can be formalized in PVS, is briefly described. Section 4 introduces imperative programs and gives an overview of how we deal with them in PVS. Finally, as an example, a molecular solution of the pairwise disjoint families problem and a description of its formal verification obtained with PVS, is presented. The set of developed theories in PVS for this paper are available on the web at http://www.cs.us.es/∼cgdiaz/investigacion. 2 The Prototype Verification System The Prototype Verification System (PVS) is a proof checker based on higher– order logic where types have semantics according to Zermelo–Fraenkel set theory with the axiom of choice [8]. In such a logic we can quantify over functions which take functions as arguments and return them as values. Specifications are organized into theories. They can be parameterized with semantic constructs (constant or types). Also they can import other theories. Aprelude for certain standard theories is preloaded into the system. As an example we include in figure 1 the PVS theory suc finitas def which provides an alternative definition (to the type finseq given in the prelude) for sequences of a given length nfor elements of a given type V. suc_finitas_def[V: TYPE, n: nat]: THEORY BEGIN % Finite sequence: S = {sk}k<n+1 SUC_FINITAS: TYPE = [below[n] -> V] SF: TYPE = SUC_FINITAS END suc_finitas_def Fig. 1. A PVS Theory Before a theory may be used, it must be typechecked. The PVS typechecker analyzes the theory for semantic consistency and adds semantic information to the internal representation built by the parser. Since this is an undecidable process, the checks which cannot be resolved automatically are presented to the user as assertions called type–correctness conditions. The PVS prover is goal–oriented. Goals are sequents consisting of antecedents and consequents, e.g. A1,...,A nB1,...,B m. The conjunction of the antecedents should imply the disjunction of consequents, i.e. A1∧ ··· ∧ An→ B1∨···∨Bm. The proof starts with a goal of the form B, where Bis the theorem to be proved. The user may type proof commands which either prove the current goal, or result in one or more new goals to prove. In this manner a proof tree is constructed. The original goal is proved when all leaves of the proof tree are recognized as true propositions. Basic proof commands can also be combined into strategies. 3 The Sticker Model: A Description Through PVS The sticker model used in this paper was introduced by S. Roweis et al. [9] (this model is completely different from the sticker systems introduced by L. Kari et al in [6]). It is an abstract model of DNA based molecular computing with random access memory in the following sense: some operations could modify the structure of the DNA molecules and so the information codified by them changes during the execution. In this model, a memory strand (a single stranded DNA molecule) Nbases in length subdivided into knon–overlapping regions each Mbases long is considered to represent a string of kbits. Each region is identified with exactly one bit position. Also, kdifferent sticker strands (single stranded DNA molecule) each of them Mbases long and complementary with one and only one of the k memory regions are considered. If a sticker is annealed to its matching region then the corresponding bit is on. Otherwise, it is off. A memory strand together with its associated stickers, if any, is called a memory complex and represent one bit string. In this sense we consider memory complexes as finite sequence of bits in PVS: BITS: TYPE = {on, off} MEMORY_COMPLEX: TYPE = finseq[BITS] Associated with this definition we consider the application σfrom Ninto {on, off}defined as follows (where σiis the i-th element of the bit sequent σ): σ(i)=σiif i<k off otherwise appl(sigma: MEMORY_COMPLEX, i: nat): BITS = IF i < sigma‘length THEN sigma‘seq(i) ELSE off ENDIF Within sticker model a tube is a collection of memory complexes representing a multiset of bit strings. All memory strands (underlying each complex) in a tube are identical and each one has stickers annealed only at the required bit positions. In PVS we consider a general concept: a multiset of memory complexes: GEN_TUBE: TYPE = MULTISETS[MEMORY_COMPLEX] Then we restrict this definition to consider tubes containing only memory complexes of a given length, namely k. MTUBE: TYPE = {T: GEN_TUBE | FORALL (sigma: MEMORY_COMPLEX): ms_in(sigma, T) IMPLIES sigma‘length = k} The following are the molecular operations on tubes used in the sticker model and the corresponding implementation in PVS. –To combine two tubes producing a new one containing all the memory complexes from both tubes. combine(T1, T2: GEN_TUBE): GEN_TUBE = LAMBDA (sigma: MEMORY_COMPLEX): T1(sigma) + T2(sigma) –To separate the content of a tube into two new tubes, one containing all the memory complexes with a particular sticker annealed (a particular bit on) and the other all those with that region free (that bit off ). separate(T: GEN_TUBE, oi: nat): [GEN_TUBE, GEN_TUBE] = (LAMBDA (sigma: MEMORY_COMPLEX): IF appl(sigma, oi) = on THEN T(sigma) ELSE 0 ENDIF, LAMBDA (sigma: MEMORY_COMPLEX): IF appl(sigma, oi) = off THEN T(sigma) ELSE 0 ENDIF) –To turn on (set) a particular region annealing the appropriate sticker on every complex in a tube (turning the corresponding bit to on). –To turn off (clear) a particular region removing the appropriate sticker, if any, on every complex in a tube (turning the corresponding bit to off ). Previously to the implementation of these operations we define the concept of modifying in a memory complex, σ, a particular bit, i,tob∈{on, off}. σb i={σ0,...,σ i−1,b,σ i+1,...,σ k−1}if i<k σotherwise turn(sigma: MEMORY_COMPLEX, i: nat, b: BITS): MEMORY_COMPLEX = IF i < sigma‘length THEN sigma WITH [(seq) := sigma‘seq WITH [(i) := b]] ELSE sigma ENDIF From this we consider a general operation that changes, in all memory complexes present in a tube, T, a particular bit, i,tob∈{on, off}. Change(T, i,b)={{ σb i|σ∈T}} change(T: GEN_TUBE, i: nat, b: BITS): GEN_TUBE = LAMBDA (sigma: MEMORY_COMPLEX): IF i < sigma‘length AND sigma‘seq(i) = b THEN T(turn(sigma, i, off)) + T(turn(sigma, i, on)) ELSIF i >= sigma‘length THEN T(sigma) ELSE 0 ENDIF The implementation of the turn operations (set and clear) are as follows: Set(T, i) = {{ σon i|σ∈T}} Clear(T, i) = {{ σoff i|σ∈T}} set(T: GEN_TUBE, i: nat): GEN_TUBE = change(T, i, on) clear(T: GEN_TUBE, i: nat): GEN_TUBE = change(T, i, off) Also a read operation is considered. This operation determines if a tube is empty and otherwise selects a complex from the tube and produce the associated string of bits. To implement it we consider the special memory complex of length 0as the answer when there is no elements in the tube. read(T: GEN_TUBE): MEMORY_COMPLEX = IF EXISTS (gamma: MEMORY_COMPLEX): ms_in(gamma, T) THEN choose({sigma: MEMORY_COMPLEX | ms_in(sigma, T)}) ELSE empty_seq ENDIF Usually we express the use of those operations as assignments. For example, T←− Combine(T1,T 2) The interpretation of a program in the sticker model as a sequence of such operations has taken us to consider them as imperative programs. 4 Imperative Programs Following [3] we consider an imperative program as a sequence, I1@@ I2@@ ...@@ Ik, of states transformers1. When such a program is executed on an initial state the first transformer is applied to it, the second is applied to the state obtained by the previous one and so on. A general work that shows how to deal in PVS with nontermination and nondeterministic state transformers can be found in [11]. Astate is considered as a finite sequence of data in a given domain (we introduced the possibility of take a tuple of sequences over different domains to deal with elements of different nature). To access to the information stored in a state we have variables. Each variable is associated with a natural number in a one–to–one manner. The n–variable over a given state takes the value of the n–th element. In general, a term is any function, t, that given a state, s∈S, produces an element over a given domain, D. Operations between elements of given domains are lifted to operations between terms using the function lwe describe with an example. Suppose we have a binary operation op: D1×D2→R. With lwe obtain a binary operation l(op), that given two terms t1:S→D1and t2:S →D2produces the term l(op)(t1,t 2): S →Rwhere l(op)(t1,t 2)(s) = op(t1(s), t2(s)) This function lis generalized to consider constants. Given c∈D, we obtain the term l(c): S →Dsuch that l(c)(s) = c. In [5], Hoare introduced the {ϕ}P{ψ}notation to describe the behaviour of a program P. Those expressions are called specifications of partial correctness and have the following meaning: If ϕand ψare some conditions over states the specification is true if whenever the program Pis executed over a state verifying ϕand it halts, then it produces a state verifying ψ. As the considered notion of program only consider total functions those expressions are, in fact, specifications of total correctness. 1In order to save space, we do not include in this section the corresponding PVS implementations, see [3] and [4] for more details. To construct a formal proof of a specification of partial correctness we use the Floyd–Hoare logic, a set of axioms and inference rules. Next we introduce the ones used to construct the correctness proof in the following section. –The consequence rule: ϕ→ϕ,{ϕ’}S{ψ’},ψ →ψ {ϕ}S{ψ} –The assignment instruction,X←− t(we denote ←− by << in PVS) is a program that over a state sproduces the state s[t(s)/X], resulting from s after the substitution of the associated value for the variable Xby t(s). The assignment axiom is {ϕ[t/X]}X←− t{ϕ} where ϕ[t/X](s) = ϕ(s[t(s)/X]). –The compose rule: {ϕ}S1{ψ},{ψ}S2{φ} {ϕ}S1@@ S2{φ} –Given a program P, the following form for X from 0 to t-1 do P end for (we write it loop(X, t, P) for short) has the following meaning X←− 0 @@ P @@ ...@@ X ←− t-1 @@ P Theloopruleis {ϕ∧X<t}P{ϕ[X+1/X]} {ϕ[0/X]}loop(X, t, P) {ϕ[t/X]} no assignment to Xor variables occurring in tis used in P 4.1 First Order Logic To express conditions over states we consider a first order logic whose set of terms, TERM, is the inductive closure of the union of the set of variables mentioned above and the set of lifted constants under the constructors l(op) for every function op. The set of atomic formulas is the inductive closure of the pair of sets TERM and {l(p)| p boolean constant}, under the constructors l(op) for every predicate op. Previous to the definition of the set of formulas we need the concept of the state, s[d/X], resulting from a given one, s, after the substitution of the associated value for a variable Xby d.Thatis,s[d/X] is a state such that for any other variable different from Xit has the same associated value than sand for Xit has das the associated value. The set of formulas is the inductive closure of the set of atomic formulas under the constructors l(∧), l(∨), l(¬), foreach and exists, where foreach(X, ϕ):S→bool such that foreach(X, ϕ)(s) ≡∀ d(ϕ(s[d/X])) exists(X, ϕ):S→bool such that exists(X, ϕ)(s) ≡∃ d(ϕ(s[d/X])) 5 The Pairwise Disjoint Families Problem Let us consider the following problem: Let A={0, ..., p-1}.LetF={B0, ..., Bq−1}a finite family of subsets of A. To determine all the ordered pairs (F’, F’),whereF’is a subfamily of Fand its elements are pairwise disjoint. To solve this problem in the sticker model we consider as initial tube T0,a (p+q, q)–library (a tube containing, at least, a copy of any memory complex with p+q regions and the plast regions deactivated). The first qbits represent a subfamily of F. Given a memory complex with p+q regions, σ, we consider that it codifies an ordered pair (Fσ,A σ), where Fσis the subfamily {Bj|σ(j)= on}of Fand Aσis the subset {j| σ(j+q)=on}of A. Fσ p Aσ q Fig. 2. Memory complex with (p+q) regions The following is a program in the sticker model that solves the pairwise disjoint families problem (where bi jis the j-th element of Bi,thei-th subset of F,andriis its size; that is, Bi={bi 0,...,bi ri−1}∈F). Note: Each instruction is labeled in order to make references. Procedure Disjoint INPUT: A family Fof A subsets I1for I ←− 0to q-1 do L1(T*, T-) ←− Separate(T, I) @@ L2for J ←− 0to rI-1 do l1(T+, T’-) ←− Separate(T*, bI J+q) @@ l2T* ←− Set(T’-, bI J+q) end for @@ L3T←− Combine(T*, T-) end for The following PVS expression implements the program: disjoint(F: (FAMILY(p, q))): program = LET eB = l(elemF(p,q,F)) IN loop(VI, q, assig2((VTast, VTn), l(separate)(VT, VI)) @@ loop(VJ, l(tam(p,q,F))(VI), assig2((VTm, VTnn), l(separate)(VTast, eB(VI, VJ) + l(q))) @@ (VTast << l(set)(VTnn, eB(VI, VJ) + l(q)))) @@ (VT << l(combine)(VTast, VTn))) assig2(PT: [V1, V1], Pt: [term1, term1]): program = (PT‘1 << Pt‘1) @@ (PT‘2 << Pt‘2) In order to stablish the correctness of this program we consider the formula: ΘF(T) ≡∀τ(τ∈T→∀ i1<i 2<q(τ(i1)=τ(i2)=on→Bi1∩Bi2=∅)) expressing that the memory complexes of a given tube codifies a subfamily of F whose elements are pairwise disjoint. correc_disjoint(F: (FAMILY(p, q)))(T: MTUBE[p + q]): bool = FORALL (tau: MEMORY_COMPLEX): (ms_in(tau, T) IMPLIES (FORALL (i1, i2: below[q]): (appl(tau, i1) = on AND appl(tau, i2) = on AND i1 < i2 IMPLIES disj(F‘seq(i1), F‘seq(i2))))) The following specification stablish the correctness of the program (where library?[p+q](q) is a predicate over tubes characterizing a (p+q, q)–library): {library?[p+q](q)(T)}disjoint(F){ΘF(T)} To prove this specification we will use two formulas θand δ, that will be invariants of the main loop (I1) and inner loop (L2), respectively. For these formulas we prove the following results: 1. library?[p+q](q)(T) →θ[0/I] 2. θ[q/I] →ΘF(T) 3. θ∧I<q→δ[0/J][+(T,I)/T*][-(T,I)/T-] 4. δ[rI/J] →θ[I+1/I][T* ∪T-/T] 5. δ∧J<r I→ δ[J+1/J][Set(T’-, bI J+q)/T*][-(T*, bI J+q)/T’-][+(T*, bI J+q)/T+] From those results and using the appropriate axioms and inference rules from Floyd–Hoare logic we prove the following specifications: –{δ*}l1@@ l2{δ[J+1/J]}where δ*is the formula δ[J+1/J][Set(T’-, bI J+q)/T*][-(T*, bI J+q)/T’-][+(T*, bI J+q)/T+] (using the assignment axiom and the compose rule). –{δ∧J<r I}l1@@ l2{δ[J+1/J]}(using 5 and the consequence rule). –{δ[0/J]}L2{δ[rI/J]}(using the loop for rule). –{δ[0/J]}L2{θ[I+1/I][T* ∪T-/T]}(using 4 and the consequence rule). –{δ[0/j][+(T,I)/T*][-(T,I)/T-]}L1@@ L2@@ L3{θ[I+1/I]}(with the assignment axiom and the compose rule). –{θ∧I<q}L1@@ L2@@ L3{θ[I+1/I]}(with 3 and the consequence rule). –{θ[0/I]}I1{θ[q/I]}} (using the loop for rule). –{library?[p+q](q)(T)}disjoint(F){ΘF(T)}(using 1, 2 and the consequence rule). The used formulas, θand δ, are the following: θ≡θD(T,I) ∧θR(T,I) ∧(I=0 →library?[p+q](q)(T)]) δ≡δD(T*,I,J) ∧θD(T-,I) ∧carac(T-,I) ∧δR(T*,I,J) ∧θR(T-,I) where –θD(T,I) is the formula: I≤q→∀τ(τ∈T→∀i1<i2<I(τ(i1)=τ(i2)=on→Bi1∩Bi2=∅)) expressing that for each memory complex τof a tube T, the elements of the subfamily FI τ={Bi|i<I∧τ(i)=on}are pairwise disjoint. –θR(T, I) is the formula: I≤q→∀τ(τ∈T→ ∀k<I (τ(k)=on→Bk+q ⊆τ)∧ ∀s<p(τ(s+q) = on →∃k<I(τ(k)=on∧s∈Bk))) that is, for each memory complex, τ,ofatubeT,wehaveFI τ=A τ. –δD(T,I,J) is the formula: I<q∧J≤rI→ ∀τ(τ∈T→(τ(I)=on→∀i1<I (τ(i1)=on→Bi1∩BJ I=∅)) ∧ ∀i1<i2<I(τ(i1)=τ(i2)=on→Bi1∩Bi2=∅)) expressing that for each memory complex, τ,inatubeT,ifBI∈F I+1 τ, then the set BJ I(compose by the first Jelements of BI) is disjoint with the elements of the subfamily FI τ; and that the elements of the subfamily FI τare pairwise disjoint. –δR(T,I,J) is the formula I<q∧j≤rI→ ∀τ(τ∈T→(τ(I)=on∧∀k<I (τ(k)=on→Bk+q ⊆τ)∧BJ I+q ⊆τ∧ ∀s<p(τ(s+q)=on→∃k<I((τ(k)=on∧s∈Bk)∨s∈BJ I)))) expressing that for each memory complex, τ,inatubeT,wehave (FI τ)∪BJ I=A τ –carac(T, I) ≡∀τ(τ∈T→τ(I) = off). This formula characterizes the contents of the second tube obtained after the use of the Separate operation.