A genetically modified Hoare logic

DOI10.1016/J.TCS.2018.02.003MaRDI QIDQ2422014zbMATH OpenOpenAlexFDO

Authors Gilles Bernot, Z. Khalis, Adrien Richard, Olivier Roux, Jean-Paul Comet

Publication date 18 June 2019

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1506.05887

zbMATH Keywords

parameter identificationgene regulatory networksHoare logicsoundness and completenessThomas networks

Mathematics Subject Classification ID

Systems biology, networks (92C42) Logic in computer science (03B70)

Abstract: An important problem when modeling gene networks lies in the identification of parameters, even if we consider a purely discrete framework as the one of Ren'e Thomas. Here we are interested in the exhaustive search of all parameter values that are consistent with observed behaviors of the gene network. We present in this article a new approach based on Hoare Logic and on a weakest precondition calculus to generate constraints on possible parameter values. Observed behaviors play the role of "programs" for the classical Hoare logic, and computed weakest preconditions represent the sets of all compatible parameterizations expressed as constraints on parameters. Finally we give a proof of correctness of our Hoare logic for gene networks as well as a proof of completeness based on the computation of the weakest precondition.

Recommendations

• Constraint identification using modified Hoare logic on hybrid models of gene networks
• Model Checking Genetic Regulatory Networks with Parameter Uncertainty
• Model Checking Gene Regulatory Networks
• On Timed Models of Gene Networks
• Model checking the evolution of gene regulatory networks

Cites work

• scientific article; zbMATH DE number 48630 (Why is no real title available?)
• scientific article; zbMATH DE number 50840 (Why is no real title available?)
• A Semantic Basis for Program Verification
• An axiomatic basis for computer programming
• Application of formal methods to biological regulatory networks: extending Thomas' asynchronous logical approach with temporal logic
• Computational Methods in Systems Biology
• Concurrent dynamic logic
• Guarded commands, nondeterminacy and formal derivation of programs
• Inadequacy of computable loop invariants
• Logical identification of all steady states: The concept of feedback loop characteristic states
• Logical modeling of biological systems
• Model Checking Gene Regulatory Networks
• Multistationarity, the basis of cell differentiation and memory. I: Structural conditions of multistationarity and other nontrivial behavior
• Multistationarity, the basis of cell differentiation and memory. II: Logical analysis of regulatory networks in terms of feedback circuits
• Necessary conditions for multistationarity in discrete dynamical systems
• Negative circuits and sustained oscillations in asynchronous automata networks
• On the completeness of propositional Hoare logic
• Programming Languages and Systems
• Soundness and Completeness of an Axiom System for Program Verification
• Temporal constraints in the logical analysis of regulatory networks

Cited in

(2)

• Constrained Kripke structure for identifying parameters of biological models
• Greening R. Thomas' framework with environment variables: a divide and conquer approach

Describes a project that uses

Uses Software

• Leviathan
• GNA
• Ginsim

This page was built for publication: A genetically modified Hoare logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2422014)