2014/04/22 by Elisabetta De Maria, De Maria, Elisabetta, Joëlle Despeyroux +4 · 1 citation
Biochemistry, Genetics and Molecular Biology · Computer Science · #FOS: Biological sciences #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Other Quantitative Biology (q-bio.OT) #Semantic Web and Ontologies #cs.LO #q-bio.OT
paper · pdf · doi:10.48550/arxiv.1404.5439
(2014)
arxiv created 2014/04/22 · openalex publication_date 2014/04/22 · arxiv updated 2014/05/03 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We propose a novel approach for the formal verification of biological systems based on the use of a modal linear logic. We show how such a logic can be used, with worlds as instants of time, as an unified framework to encode both biological systems and temporal properties of their dynamic behaviour. To illustrate our methodology, we consider a model of the P53/Mdm2 DNA-damage repair mechanism. We prove several properties that are important for such a model to satisfy and serve to illustrate the promise of our approach. We formalize the proofs of these properties in the Coq Proof Assistant, with the help of a Lambda Prolog prover for partial automation of the proofs.