Compositionality results for cardiac cell dynamics

By appealing to the small-gain theorem of one of the authors (Girard), we show that the 13-variable sodium-channel component of the 67-variable IMW cardiac-cell model (Iyer Mazhari-Winslow) can be replaced by an approximately bisimilar, 2-variable HH-type (Hodgkin-Huxley) abstraction. We show that this substitution of (approximately) equals for equals is safe in the sense that the approximation error between sodium-channel models is not amplified by the feed- back-loop context in which it is placed. To prove this feed-back- compositionality result, we exhibit quadratic-polynomial, exponentially decaying bisimulation functions between the IMW and HH-type sodium channels, and also for the IMW-based context in which these sodium-channel models are placed. These functions allow us to quantify the over-all error introduced by the sodium-channel abstraction and subsequent substitution in the IMW model. To automate computation of the bisimulation functions, we employ the SOSTOOLS optimization toolbox. Our experimental results validate our analytical findings. To the best of our knowledge, this is the first application of δ-bisimilar, feedback-assisting, compositional reasoning in biological systems. Copyright is held by the owner/author(s).