Invariant verification of nonlinear hybrid automata networks of cardiac cells

Zhenqi Huang, Chuchu Fan, Alexandru Mereacre, Sayan Mitra, Marta Kwiatkowska

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Verification algorithms for networks of nonlinear hybrid automata (HA) can aid us understand and control biological processes such as cardiac arrhythmia, formation of memory, and genetic regulation. We present an algorithm for over-approximating reach sets of networks of nonlinear HA which can be used for sound and relatively complete invariant checking. First, it uses automatically computed input-to-state discrepancy functions for the individual automata modules in the network A for constructing a low-dimensional model M. Simulations of both A and M are then used to compute the reach tubes for A. These techniques enable us to handle a challenging verification problem involving a network of cardiac cells, where each cell has four continuous variables and 29 locations. Our prototype tool can check bounded-time invariants for networks with 5 cells (20 continuous variables, 295 locations) typically in less than 15 minutes for up to reasonable time horizons. From the computed reach tubes we can infer biologically relevant properties of the network from a set of initial states.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings
PublisherSpringer-Verlag
Pages373-390
Number of pages18
ISBN (Print)9783319088662
DOIs
StatePublished - Jan 1 2014
Event26th International Conference on Computer Aided Verification, CAV 2014 - Held as Part of the Vienna Summer of Logic, VSL 2014 - Vienna, Austria
Duration: Jul 18 2014Jul 22 2014

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8559 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other26th International Conference on Computer Aided Verification, CAV 2014 - Held as Part of the Vienna Summer of Logic, VSL 2014
CountryAustria
CityVienna
Period7/18/147/22/14

    Fingerprint

Keywords

  • Biological networks
  • hybrid systems
  • invariants
  • verification

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Huang, Z., Fan, C., Mereacre, A., Mitra, S., & Kwiatkowska, M. (2014). Invariant verification of nonlinear hybrid automata networks of cardiac cells. In Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings (pp. 373-390). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8559 LNCS). Springer-Verlag. https://doi.org/10.1007/978-3-319-08867-9_25