TY - GEN
T1 - Invariant verification of nonlinear hybrid automata networks of cardiac cells
AU - Huang, Zhenqi
AU - Fan, Chuchu
AU - Mereacre, Alexandru
AU - Mitra, Sayan
AU - Kwiatkowska, Marta
N1 - The authors are supported by NSA SoS grant (W911NSF-13-0086), AFOSR YIP grant (FA9550-12-1-0336), NSF CAREER grant (CNS 10-54247), the ERC AdG VERIWARE, ERC PoC VERIPACE, and the Institute for the Future of Computing, Oxford Martin School.
PY - 2014
Y1 - 2014
N2 - 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.
AB - 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.
KW - Biological networks
KW - hybrid systems
KW - invariants
KW - verification
UR - https://www.scopus.com/pages/publications/84904815101
UR - https://www.scopus.com/pages/publications/84904815101#tab=citedBy
U2 - 10.1007/978-3-319-08867-9_25
DO - 10.1007/978-3-319-08867-9_25
M3 - Conference contribution
AN - SCOPUS:84904815101
SN - 9783319088662
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 373
EP - 390
BT - Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings
PB - Springer
T2 - 26th International Conference on Computer Aided Verification, CAV 2014 - Held as Part of the Vienna Summer of Logic, VSL 2014
Y2 - 18 July 2014 through 22 July 2014
ER -