Verifying chemical reaction network implementations: a pathway decomposition approach
From MaRDI portal
Publication:2422010
Abstract: Here we focus on the challenge of verifying the correctness of molecular implementations of abstract chemical reaction networks, where operation in a well-mixed "soup" of molecules is stochastic, asynchronous, concurrent, and often involves multiple intermediate steps in the implementation, parallel pathways, and side reactions. This problem relates to the verification of Petri nets, but existing approaches are not sufficient for providing a single guarantee covering an infinite set of possible initial states (molecule counts) and an infinite state space potentially explored by the system given any initial state. We address these issues by formulating a new theory of pathway decomposition that provides an elegant formal basis for comparing chemical reaction network implementations, and we present an algorithm that computes this basis. Our theory naturally handles certain situations that commonly arise in molecular implementations, such as what we call "delayed choice," that are not easily accommodated by other approaches. We further show how pathway decomposition can be combined with weak bisimulation to handle a wider class that includes most currently known enzyme-free DNA implementation techniques. We anticipate that our notion of logical equivalence between chemical reaction network implementations will be valuable for other molecular implementations such as biochemical enzyme systems, and perhaps even more broadly in concurrency theory.
Recommendations
- Verifying chemical reaction network implementations: a bisimulation approach
- Verifying chemical reaction network implementations: a bisimulation approach
- Verifying polymer reaction networks using bisimulation
- Modular verification of chemical reaction network encodings via serializability analysis
- On design and analysis of chemical reaction network algorithms
Cites work
- A general-purpose CRN-to-DSD compiler with formal verification, optimization, and simulation capabilities
- Bisimulation relations for weighted automata
- CONCUR 2005 – Concurrency Theory
- Efficient Turing-universal computation with DNA polymers
- scientific article; zbMATH DE number 1696467 (Why is no real title available?)
- scientific article; zbMATH DE number 42752 (Why is no real title available?)
- scientific article; zbMATH DE number 559221 (Why is no real title available?)
- Less haste, less waste: on recycling and its limits in strand displacement systems
- Modular verification of chemical reaction network encodings via serializability analysis
- Persistence of vector replacement systems is decidable
- Petri nets and regular processes
- Reduction techniques for network validation in systems biology
- Rule-Based Modelling of Cellular Signalling
- Space and energy efficient computation with DNA strand displacement systems
- Stochastic mechanics of graph rewriting
- Stochastic simulation of the kinetics of multiple interacting nucleic acid strands
- Strand algebras for DNA computing
- Symbolic transfer function-based approaches to certified compilation
- Two-domain DNA strand displacement
- Verifying chemical reaction network implementations: a bisimulation approach
Cited in
(10)- On design and analysis of chemical reaction network algorithms
- Verifying polymer reaction networks using bisimulation
- Verifying chemical reaction network implementations: a bisimulation approach
- Comparing chemical reaction networks: a categorical and algorithmic perspective
- Verifying chemical reaction network implementations: a bisimulation approach
- Modular verification of chemical reaction network encodings via serializability analysis
- Population-induced phase transitions and the verification of chemical reaction networks
- Computing with chemical reaction networks: a tutorial
- Polynomial equivalence of extended chemical reaction models
- Testing binomiality of chemical reaction networks using comprehensive Gröbner systems
This page was built for publication: Verifying chemical reaction network implementations: a pathway decomposition approach
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2422010)
