2022 Annual Meeting

(481c) Verifying Properties of Chemical Reactors Using an Automated Theorem Prover

Authors

Tyler R. Josephson, University of Maryland, Baltimore County
Differential dynamic logic (dL) can be used to validate properties of systems governed by systems of ordinary differential equations (ODEs) through a mathematical correctness proof. KeYmaera X is an automated theorem prover that implements dL, and has been used to verify safety of cyber-physical systems[1].

To explore the application of dL in chemically reacting systems, we first verified the properties of the elementary reaction (A→B), as well as parallel (A→B, A→C) and sequential first-order reactions (A→ B →C). These set us up to verify the properties of Michaelis-Menten kinetics, a kind of enzyme kinetics that functions as a simple catalytic process (E + S ⇌ ES → E + P), in which an enzyme, E, binds with a substrate, S, to produce a complex, ES, which in turn forms product, P, and regenerates the enzyme, E.

Notably, this system of ODEs has no closed-form solution unless certain appropriations are made. Nonetheless, by using dL, we can prove that some states are unreachable by this system of ODEs.

In this case study, we demonstrate how the tactics defined in KeYmaera X can be used to build a step-by-step proof that establishes limits on concentrations in reacting systems. In the case of Michaelis-Menten kinetics, we prove that for all time t > 0, ES <= E0 + S0; ES never exceeds the total initial concentrations of E and S, a conclusion which logically holds at all times and for any combination of reaction rate parameters and initial concentrations. We found that the mole balance E + ES = E0 + ES0 was useful additional information for building the proof; as a differential invariant, it served as an intermediate statement used by the solver to find a solution.

  1. A Platzer. Logical Foundation of Cyber-Physical Systems, Springer, 2018