Abstract
The aim of this paper is to develop an executable prototype of an unconventional model of computation. Using the PVS verifica- tion system (an interactive environment for writing formal specifications and checking formal proofs), we formalize the restricted model, based on DNA, due to L. Adleman. Also, we design a formal molecular program in this model that solves SAT following Lipton’s ideas. We prove using PVS the soundness and completeness of this molecular program. This work is intended to give an approach to the opportunities offered by mecha nized analysis of unconventional model of computation in general. This approach opens up new possibilities of verifying molecular experiments before implementing them in a laboratory.
This work has been supported by DGES/MEC: Projects TIC2000-1368-C03-02 and PB96-1345
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Leonard M. Adleman. Molecular computation of solutions to combinatorial problems. Science, 266:1021–1024, November 11, 1994.
Leonard M. Adleman. On constructing a molecular computer. DIMACS: Series in Discrete Mathematics and Theoretical Computer Science. American Mathematical Society, 1996. DNA Based Computers.
Judy Crow, Sam Owre, John Rushby, Natarajan Shankar, and Mandayam Srivas. A tutorial introduction to PVS. Presented at WIFT’ 95: Workshop on Industrial-Strength Formal Specification Techniques, Boca Raton, Florida, April 1995. Available, with specification files, at http://www.csl.sri.com/papers/wift-tutorial/.
M.J. Pérez Jiménez, F. Sancho Caparrini, M.C. Graciani Díaz, and A. Romero Jiménez. Soluciones moleculares del problema SAT de la Lógica Proposicional. In Lógica, Lenguaje e Información, JOLL’2000, pages 243–252. Ed. Kronos, 2000.
Richard J. Lipton. Using DNA to solve NP-complete problems. Science, 268:542–545, April 1995.
F.J. Martín-Mateos, J.A. Alonso, M.J. Pérez-Jiménez, and F. Sancho-Caparrini. Molecular computation models in ACL2: a simulation of Lipton’s experiment solving SAT. In Third International Workshop on the ACL2 Theorem Prover and Its Applications, Grenoble, 2002.
Sam Owre and Natarajan Shankar. The formal semantics of PVS. Technical Report SRI-CSL-97-2, Computer Science Laboratory, SRI International, Menlo Park,CA, August 1997.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Díaz, C.G., Mateos, F.J.M., Pérez Jiménez, M.J. (2002). Specification of Adleman’s Restricted Model Using an Automated Reasoning System: Verification of Lipton’s Experiment. In: Unconventional Models of Computation. UMC 2002. Lecture Notes in Computer Science, vol 2509. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45833-6_11
Download citation
DOI: https://doi.org/10.1007/3-540-45833-6_11
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44311-7
Online ISBN: 978-3-540-45833-3
eBook Packages: Springer Book Archive