A genetically modified Hoare logic

DOI10.1016/J.TCS.2018.02.003zbMATH Open1423.68163arXiv1506.05887OpenAlexW2963446106MaRDI QIDQ2422014FDOQ2422014

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)

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.

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

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

zbMATH Keywords

parameter identificationgene regulatory networksHoare logicsoundness and completenessThomas networks

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (2)

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

Uses Software

• Ginsim
• GNA
• Leviathan

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)