Using Au oma ed Reasoning Sys ems on
Molecula Compu ing
Ca men G aciani D´ıaz and Ma io J. P´e ez-Jim´enez
Resea ch G oup on Na u al Compu ing,
Dp o. Ciencias de la Compu aci´on e In eligencia A i icial,
Uni e sidad de Se illa (Spain)
{cgdiaz, ma pe }@us.es
Abs ac . This pape is ocused on he in e play be ween au oma ed
easoning sys ems (as heo e ical and o mal de ices o s udy he co -
ec ness o a p og am) and DNA compu ing (as p ac ical de ices o
handle DNA s ands o sol e classical ha d p oblems wi h labo a o y
echniques). To illus a e his wo k we ha e p o en in he PVS p oo
checke , he co ec ness o a p og am, in a s icke based model o DNA
compu a ion, sol ing he pai wise disjoin amilies p oblem. Also we in-
oduce he o maliza ion o he Floyd–Hoa e logic o impe a i e p o-
g ams.
1 In oduc ion
One o he mos ac i e a eas o esea ch in Compu e Science is he s udy and use
o o mal me hods (applica ions o p ima ily disc e e ma hema ics o so wa e
enginee ing p oblems). I s widely de elopmen and he complexi y o in e es ing
p oblems ha e gi en ise o au oma ed easoning. In his a ea, one o he main
p oblems is he co ec ness [2]: de eloping specifica ions and p oo s ha ensu es
a p og am mee s i s specifica ion. The e is a p e ious wo k o o maliza ion:
exp essing all defini ions, heo ems and p oo s in a o mal language wi hou
seman ic ambigui y. This app oxima ion has especial ele ance in new compu ing
pa adigms such as he DNA based molecula compu ing. In many molecula
models he da a a e ubes o e an alphabe whose con en encodes a collec ion o
DNA s ands. The ope a ions conside ed a e abs ac ion o diffe en labo a o y
echniques o manipula e DNA s ands.
This pape is o ganized as ollows. I begins wi h a sho p esen a ion o
he P o o ype Ve ifica ion Sys em (PVS) and he s icke model. Then, how his
model can be o malized in PVS, is b iefly desc ibed. Sec ion 4 in oduces impe -
a i e p og ams and gi es an o e iew o how we deal wi h hem in PVS. Finally,
as an example, a molecula solu ion o he pai wise disjoin amilies p oblem
and a desc ip ion o i s o mal e ifica ion ob ained wi h PVS, is p esen ed.
The se o de eloped heo ies in PVS o his pape a e a ailable on he web a
h p://www.cs.us.es/∼cgdiaz/in es igacion.
2 The P o o ype Ve i ica ion Sys em
The P o o ype Ve ifica ion Sys em (PVS) is a p oo checke based on highe –
o de logic whe e ypes ha e seman ics acco ding o Ze melo–F aenkel se heo y
wi h he axiom o choice [8]. In such a logic we can quan i y o e unc ions which
ake unc ions as a gumen s and e u n hem as alues.
Specifica ions a e o ganized in o heo ies. They can be pa ame e ized wi h
seman ic cons uc s (cons an o ypes). Also hey can impo o he heo ies.
Ap elude o ce ain s anda d heo ies is p eloaded in o he sys em. As an
example we include in figu e 1 he PVS heo y suc ini as de which p o ides
an al e na i e defini ion ( o he ype inseq gi en in he p elude) o sequences
o a gi en leng h n o elemen s o a gi en ype V.
suc_ ini as_de [V: TYPE, n: na ]: THEORY
BEGIN
% Fini e sequence: S = {sk}k<n+1
SUC_FINITAS: TYPE = [below[n] -> V]
SF: TYPE = SUC_FINITAS
END suc_ ini as_de
Fig. 1. A PVS Theo y
Be o e a heo y may be used, i mus be ypechecked. The PVS ypechecke
analyzes he heo y o seman ic consis ency and adds seman ic in o ma ion
o he in e nal ep esen a ion buil by he pa se . Since his is an undecidable
p ocess, he checks which canno be esol ed au oma ically a e p esen ed o he
use as asse ions called ype–co ec ness condi ions.
The PVS p o e is goal–o ien ed. Goals a e sequen s consis ing o an eceden s
and consequen s, e.g. A1,...,A
nB1,...,B
m. The conjunc ion o he an-
eceden s should imply he disjunc ion o consequen s, i.e. A1∧ ··· ∧ An→
B1∨···∨Bm. The p oo s a s wi h a goal o he o m B, whe e Bis he
heo em o be p o ed. The use may ype p oo commands which ei he p o e
he cu en goal, o esul in one o mo e new goals o p o e. In his manne
a p oo ee is cons uc ed. The o iginal goal is p o ed when all lea es o he
p oo ee a e ecognized as ue p oposi ions. Basic p oo commands can also
be combined in o s a egies.
3 The S icke Model: A Desc ip ion Th ough PVS
The s icke model used in his pape was in oduced by S. Roweis e al. [9] ( his
model is comple ely diffe en om he s icke sys ems in oduced by L. Ka i
e al in [6]). I is an abs ac model o DNA based molecula compu ing wi h
andom access memo y in he ollowing sense: some ope a ions could modi y he
s uc u e o he DNA molecules and so he in o ma ion codified by hem changes
du ing he execu ion.
In his model, a memo y s and (a single s anded DNA molecule) Nbases
in leng h subdi ided in o knon–o e lapping egions each Mbases long is con-
side ed o ep esen a s ing o kbi s. Each egion is iden ified wi h exac ly one
bi posi ion. Also, kdiffe en s icke s ands (single s anded DNA molecule)
each o hem Mbases long and complemen a y wi h one and only one o he k
memo y egions a e conside ed. I a s icke is annealed o i s ma ching egion
hen he co esponding bi is on. O he wise, i is off. A memo y s and oge he
wi h i s associa ed s icke s, i any, is called a memo y complex and ep esen one
bi s ing. In his sense we conside memo y complexes as fini e sequence o bi s
in PVS:
BITS: TYPE = {on, o }
MEMORY_COMPLEX: TYPE = inseq[BITS]
Associa ed wi h his defini ion we conside he applica ion σ om Nin o
{on, o }defined as ollows (whe e σiis he i- h elemen o he bi sequen σ):
σ(i)=σii i<k
o o he wise
appl(sigma: MEMORY_COMPLEX, i: na ): BITS =
IF i < sigma‘leng h THEN sigma‘seq(i) ELSE o ENDIF
Wi hin s icke model a ube is a collec ion o memo y complexes ep esen ing
a mul ise o bi s ings. All memo y s ands (unde lying each complex) in a
ube a e iden ical and each one has s icke s annealed only a he equi ed bi
posi ions.
In PVS we conside a gene al concep : a mul ise o memo y complexes:
GEN_TUBE: TYPE = MULTISETS[MEMORY_COMPLEX]
Then we es ic his defini ion o conside ubes con aining only memo y
complexes o a gi en leng h, namely k.
MTUBE: TYPE =
{T: GEN_TUBE | FORALL (sigma: MEMORY_COMPLEX):
ms_in(sigma, T) IMPLIES sigma‘leng h = k}
The ollowing a e he molecula ope a ions on ubes used in he s icke model
and he co esponding implemen a ion in PVS.
–To combine wo ubes p oducing a new one con aining all he memo y com-
plexes om bo h ubes.
combine(T1, T2: GEN_TUBE): GEN_TUBE =
LAMBDA (sigma: MEMORY_COMPLEX): T1(sigma) + T2(sigma)
–To sepa a e he con en o a ube in o wo new ubes, one con aining all he
memo y complexes wi h a pa icula s icke annealed (a pa icula bi on)
and he o he all hose wi h ha egion ee ( ha bi off ).
sepa a e(T: GEN_TUBE, oi: na ): [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) = o THEN T(sigma) ELSE 0 ENDIF)
–To u n on (se ) a pa icula egion annealing he app op ia e s icke on
e e y complex in a ube ( u ning he co esponding bi o on).
–To u n off (clea ) a pa icula egion emo ing he app op ia e s icke , i
any, on e e y complex in a ube ( u ning he co esponding bi o off ).
P e iously o he implemen a ion o hese ope a ions we define he concep
o modi ying in a memo y complex, σ, a pa icula bi , i, ob∈{on, o }.
σb
i={σ0,...,σ
i−1,b,σ
i+1,...,σ
k−1}i i<k
σo he wise
u n(sigma: MEMORY_COMPLEX, i: na , b: BITS): MEMORY_COMPLEX =
IF i < sigma‘leng h
THEN sigma WITH [(seq) := sigma‘seq WITH [(i) := b]]
ELSE sigma ENDIF
F om his we conside a gene al ope a ion ha changes, in all memo y com-
plexes p esen in a ube, T, a pa icula bi , i, ob∈{on, o }.
Change(T, i,b)={{ σb
i|σ∈T}}
change(T: GEN_TUBE, i: na , b: BITS): GEN_TUBE =
LAMBDA (sigma: MEMORY_COMPLEX):
IF i < sigma‘leng h AND sigma‘seq(i) = b
THEN T( u n(sigma, i, o )) + T( u n(sigma, i, on))
ELSIF i >= sigma‘leng h THEN T(sigma) ELSE 0 ENDIF
The implemen a ion o he u n ope a ions (se and clea ) a e as ollows:
Se (T, i) = {{ σon
i|σ∈T}} Clea (T, i) = {{ σo
i|σ∈T}}
se (T: GEN_TUBE, i: na ): GEN_TUBE = change(T, i, on)
clea (T: GEN_TUBE, i: na ): GEN_TUBE = change(T, i, o )
Also a ead ope a ion is conside ed. This ope a ion de e mines i a ube is
emp y and o he wise selec s a complex om he ube and p oduce he associa ed
s ing o bi s. To implemen i we conside he special memo y complex o leng h
0as he answe when he e is no elemen s in he ube.
ead(T: GEN_TUBE): MEMORY_COMPLEX =
IF EXISTS (gamma: MEMORY_COMPLEX): ms_in(gamma, T)
THEN choose({sigma: MEMORY_COMPLEX | ms_in(sigma, T)})
ELSE emp y_seq ENDIF
Usually we exp ess he use o hose ope a ions as assignmen s. Fo example,
T←− Combine(T1,T
2)
The in e p e a ion o a p og am in he s icke model as a sequence o such
ope a ions has aken us o conside hem as impe a i e p og ams.
4 Impe a i e P og ams
Following [3] we conside an impe a i e p og am as a sequence, I1@@ I2@@
...@@ Ik, o s a es ans o me s1. When such a p og am is execu ed on an
ini ial s a e he fi s ans o me is applied o i , he second is applied o he
s a e ob ained by he p e ious one and so on. A gene al wo k ha shows how o
deal in PVS wi h non e mina ion and nonde e minis ic s a e ans o me s can
be ound in [11].
As a e is conside ed as a fini e sequence o da a in a gi en domain (we
in oduced he possibili y o ake a uple o sequences o e diffe en domains o
deal wi h elemen s o diffe en na u e). To access o he in o ma ion s o ed in
a s a e we ha e a iables. Each a iable is associa ed wi h a na u al numbe in
a one– o–one manne . The n– a iable o e a gi en s a e akes he alue o he
n– h elemen .
In gene al, a e m is any unc ion, , ha gi en a s a e, s∈S, p oduces an
elemen o e a gi en domain, D. Ope a ions be ween elemen s o gi en domains
a e li ed o ope a ions be ween e ms using he unc ion lwe desc ibe wi h
an example. Suppose we ha e a bina y ope a ion op: D1×D2→R. Wi h lwe
ob ain a bina y ope a ion l(op), ha gi en wo e ms 1:S→D1and 2:S
→D2p oduces he e m l(op)( 1,
2): S →Rwhe e
l(op)( 1,
2)(s) = op( 1(s), 2(s))
This unc ion lis gene alized o conside cons an s. Gi en c∈D, we ob ain
he e m l(c): S →Dsuch ha l(c)(s) = c.
In [5], Hoa e in oduced he {ϕ}P{ψ}no a ion o desc ibe he beha iou
o a p og am P. Those exp essions a e called specifica ions o pa ial co ec ness
and ha e he ollowing meaning: I ϕand ψa e some condi ions o e s a es he
specifica ion is ue i whene e he p og am Pis execu ed o e a s a e e i ying
ϕand i hal s, hen i p oduces a s a e e i ying ψ. As he conside ed no ion o
p og am only conside o al unc ions hose exp essions a e, in ac , specifica ions
o o al co ec ness.
1In o de o sa e space, we do no include in his sec ion he co esponding PVS
implemen a ions, see [3] and [4] o mo e de ails.

To cons uc a o mal p oo o a specifica ion o pa ial co ec ness we use
he Floyd–Hoa e logic, a se o axioms and in e ence ules. Nex we in oduce
he ones used o cons uc he co ec ness p oo in he ollowing sec ion.
–The consequence ule:
ϕ→ϕ,{ϕ’}S{ψ’},ψ
→ψ
{ϕ}S{ψ}
–The assignmen ins uc ion,X←− (we deno e ←− by << in PVS) is a
p og am ha o e a s a e sp oduces he s a e s[ (s)/X], esul ing om s
a e he subs i u ion o he associa ed alue o he a iable Xby (s).
The assignmen axiom is
{ϕ[ /X]}X←− {ϕ}
whe e ϕ[ /X](s) = ϕ(s[ (s)/X]).
–The compose ule:
{ϕ}S1{ψ},{ψ}S2{φ}
{ϕ}S1@@ S2{φ}
–Gi en a p og am P, he ollowing o m
o X om 0 o -1 do
P
end o
(we w i e i loop(X, , P) o sho ) has he ollowing meaning
X←− 0 @@ P @@ ...@@ X ←− -1 @@ P
Theloop uleis
{ϕ∧X< }P{ϕ[X+1/X]}
{ϕ[0/X]}loop(X, , P) {ϕ[ /X]}
no assignmen o Xo a iables occu ing in is used in P
4.1 Fi s O de Logic
To exp ess condi ions o e s a es we conside a fi s o de logic whose se o
e ms, TERM, is he induc i e closu e o he union o he se o a iables men ioned
abo e and he se o li ed cons an s unde he cons uc o s l(op) o e e y
unc ion op. The se o a omic o mulas is he induc i e closu e o he pai o
se s TERM and {l(p)| p boolean cons an }, unde he cons uc o s l(op) o
e e y p edica e op.
P e ious o he defini ion o he se o o mulas we need he concep o
he s a e, s[d/X], esul ing om a gi en one, s, a e he subs i u ion o he
associa ed alue o a a iable Xby d.Tha is,s[d/X] is a s a e such ha o
any o he a iable diffe en om Xi has he same associa ed alue han sand
o Xi has das he associa ed alue.
The se o o mulas is he induc i e closu e o he se o a omic o mulas
unde he cons uc o s l(∧), l(∨), l(¬), o each and exis s, whe e
o each(X, ϕ):S→bool such ha o each(X, ϕ)(s) ≡∀ d(ϕ(s[d/X]))
exis s(X, ϕ):S→bool such ha exis s(X, ϕ)(s) ≡∃ d(ϕ(s[d/X]))
5 The Pai wise Disjoin Families P oblem
Le us conside he ollowing p oblem:
Le A={0, ..., p-1}.Le F={B0, ..., Bq−1}a fini e amily o subse s
o A. To de e mine all he o de ed pai s (F’, F’),whe eF’is a sub amily
o Fand i s elemen s a e pai wise disjoin .
To sol e his p oblem in he s icke model we conside as ini ial ube T0,a
(p+q, q)–lib a y (a ube con aining, a leas , a copy o any memo y complex
wi h p+q egions and he plas egions deac i a ed). The fi s qbi s ep esen a
sub amily o F. Gi en a memo y complex wi h p+q egions, σ, we conside ha
i codifies an o de ed pai (Fσ,A
σ), whe e Fσis he sub amily {Bj|σ(j)=
on}o Fand Aσis he subse {j| σ(j+q)=on}o A.
Fσ
p
Aσ
q
Fig. 2. Memo y complex wi h (p+q) egions
The ollowing is a p og am in he s icke model ha sol es he pai wise
disjoin amilies p oblem (whe e bi
jis he j- h elemen o Bi, hei- h subse o
F,and iis i s size; ha is, Bi={bi
0,...,bi
i−1}∈F).
No e: Each ins uc ion is labeled in o de o make e e ences.
P ocedu e Disjoin
INPUT: A amily Fo A subse s
I1 o I ←− 0 o q-1 do
L1(T*, T-) ←− Sepa a e(T, I) @@
L2 o J ←− 0 o I-1 do
l1(T+, T’-) ←− Sepa a e(T*, bI
J+q) @@
l2T* ←− Se (T’-, bI
J+q)
end o @@
L3T←− Combine(T*, T-)
end o
The ollowing PVS exp ession implemen s he p og am:
disjoin (F: (FAMILY(p, q))): p og am =
LET eB = l(elemF(p,q,F)) IN
loop(VI, q,
assig2((VTas , VTn), l(sepa a e)(VT, VI)) @@
loop(VJ, l( am(p,q,F))(VI),
assig2((VTm, VTnn), l(sepa a e)(VTas , eB(VI, VJ) + l(q))) @@
(VTas << l(se )(VTnn, eB(VI, VJ) + l(q)))) @@
(VT << l(combine)(VTas , VTn)))
assig2(PT: [V1, V1], P : [ e m1, e m1]): p og am =
(PT‘1 << P ‘1) @@ (PT‘2 << P ‘2)
In o de o s ablish he co ec ness o his p og am we conside he o mula:
ΘF(T) ≡∀τ(τ∈T→∀ i1<i
2<q(τ(i1)=τ(i2)=on→Bi1∩Bi2=∅))
exp essing ha he memo y complexes o a gi en ube codifies a sub amily o F
whose elemen s a e pai wise disjoin .
co ec_disjoin (F: (FAMILY(p, q)))(T: MTUBE[p + q]): bool =
FORALL ( au: MEMORY_COMPLEX): (ms_in( au, T) IMPLIES
(FORALL (i1, i2: below[q]):
(appl( au, i1) = on AND appl( au, i2) = on AND i1 < i2 IMPLIES
disj(F‘seq(i1), F‘seq(i2)))))
The ollowing specifica ion s ablish he co ec ness o he p og am (whe e
lib a y?[p+q](q) is a p edica e o e ubes cha ac e izing a (p+q, q)–lib a y):
{lib a y?[p+q](q)(T)}disjoin (F){ΘF(T)}
To p o e his specifica ion we will use wo o mulas θand δ, ha will be
in a ian s o he main loop (I1) and inne loop (L2), espec i ely. Fo hese
o mulas we p o e he ollowing esul s:
1. lib a y?[p+q](q)(T) →θ[0/I]
2. θ[q/I] →ΘF(T)
3. θ∧I<q→δ[0/J][+(T,I)/T*][-(T,I)/T-]
4. δ[ I/J] →θ[I+1/I][T* ∪T-/T]
5. δ∧J<
I→
δ[J+1/J][Se (T’-, bI
J+q)/T*][-(T*, bI
J+q)/T’-][+(T*, bI
J+q)/T+]
F om hose esul s and using he app op ia e axioms and in e ence ules om
Floyd–Hoa e logic we p o e he ollowing specifica ions:
–{δ*}l1@@ l2{δ[J+1/J]}whe e δ*is he o mula
δ[J+1/J][Se (T’-, bI
J+q)/T*][-(T*, bI
J+q)/T’-][+(T*, bI
J+q)/T+]
(using he assignmen axiom and he compose ule).
–{δ∧J<
I}l1@@ l2{δ[J+1/J]}(using 5 and he consequence ule).
–{δ[0/J]}L2{δ[ I/J]}(using he loop o ule).
–{δ[0/J]}L2{θ[I+1/I][T* ∪T-/T]}(using 4 and he consequence ule).
–{δ[0/j][+(T,I)/T*][-(T,I)/T-]}L1@@ L2@@ L3{θ[I+1/I]}(wi h he as-
signmen axiom and he compose ule).
–{θ∧I<q}L1@@ L2@@ L3{θ[I+1/I]}(wi h 3 and he consequence ule).
–{θ[0/I]}I1{θ[q/I]}} (using he loop o ule).
–{lib a y?[p+q](q)(T)}disjoin (F){ΘF(T)}(using 1, 2 and he con-
sequence ule).
The used o mulas, θand δ, a e he ollowing:
θ≡θD(T,I) ∧θR(T,I) ∧(I=0 →lib a y?[p+q](q)(T)])
δ≡δD(T*,I,J) ∧θD(T-,I) ∧ca ac(T-,I) ∧δR(T*,I,J) ∧θR(T-,I)
whe e
–θD(T,I) is he o mula:
I≤q→∀τ(τ∈T→∀i1<i2<I(τ(i1)=τ(i2)=on→Bi1∩Bi2=∅))
exp essing ha o each memo y complex τo a ube T, he elemen s o he
sub amily FI
τ={Bi|i<I∧τ(i)=on}a e pai wise disjoin .
–θR(T, I) is he o mula:
I≤q→∀τ(τ∈T→
∀k<I (τ(k)=on→Bk+q ⊆τ)∧
∀s<p(τ(s+q) = on →∃k<I(τ(k)=on∧s∈Bk)))
ha is, o each memo y complex, τ,o a ubeT,weha eFI
τ=A
τ.
–δD(T,I,J) is he o mula:
I<q∧J≤ I→
∀τ(τ∈T→(τ(I)=on→∀i1<I (τ(i1)=on→Bi1∩BJ
I=∅)) ∧
∀i1<i2<I(τ(i1)=τ(i2)=on→Bi1∩Bi2=∅))
exp essing ha o each memo y complex, τ,ina ubeT,i BI∈F
I+1
τ,
hen he se BJ
I(compose by he fi s Jelemen s o BI) is disjoin wi h he
elemen s o he sub amily FI
τ; and ha he elemen s o he sub amily FI
τa e
pai wise disjoin .
–δR(T,I,J) is he o mula
I<q∧j≤ I→
∀τ(τ∈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))))
exp essing ha o each memo y complex, τ,ina ubeT,weha e
(FI
τ)∪BJ
I=A
τ
–ca ac(T, I) ≡∀τ(τ∈T→τ(I) = o ).
This o mula cha ac e izes he con en s o he second ube ob ained a e
he use o he Sepa a e ope a ion.