Invariant verification of nonlinear hybrid automata networks of cardiac cells

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

doi:10.1007/978-3-319-08867-9_25

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 proceeding › Conference 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, 29⁵ 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 language	English (US)
Title of host publication	Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings
Publisher	Springer-Verlag Berlin Heidelberg
Pages	373-390
Number of pages	18
ISBN (Print)	9783319088662
DOIs	https://doi.org/10.1007/978-3-319-08867-9_25
State	Published - 2014
Event	26th International Conference on Computer Aided Verification, CAV 2014 - Held as Part of the Vienna Summer of Logic, VSL 2014 - Vienna, Austria Duration: Jul 18 2014 → Jul 22 2014

Publication series

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

Other

Other	26th International Conference on Computer Aided Verification, CAV 2014 - Held as Part of the Vienna Summer of Logic, VSL 2014
Country	Austria
City	Vienna
Period	7/18/14 → 7/22/14

Keywords

Biological networks
hybrid systems
invariants
verification

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/978-3-319-08867-9_25

Fingerprint Dive into the research topics of 'Invariant verification of nonlinear hybrid automata networks of cardiac cells'. Together they form a unique fingerprint.

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 Berlin Heidelberg. https://doi.org/10.1007/978-3-319-08867-9_25

Invariant verification of nonlinear hybrid automata networks of cardiac cells. / Huang, Zhenqi; Fan, Chuchu; Mereacre, Alexandru; Mitra, Sayan; Kwiatkowska, Marta.

Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings. Springer-Verlag Berlin Heidelberg, 2014. p. 373-390 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8559 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8559 LNCS, Springer-Verlag Berlin Heidelberg, pp. 373-390, 26th International Conference on Computer Aided Verification, CAV 2014 - Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, 7/18/14. https://doi.org/10.1007/978-3-319-08867-9_25

Huang Z, Fan C, Mereacre A, Mitra S, Kwiatkowska M. 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. Springer-Verlag Berlin Heidelberg. 2014. p. 373-390. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-319-08867-9_25

Huang, Zhenqi ; Fan, Chuchu ; Mereacre, Alexandru ; Mitra, Sayan ; Kwiatkowska, Marta. / Invariant verification of nonlinear hybrid automata networks of cardiac cells. Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings. Springer-Verlag Berlin Heidelberg, 2014. pp. 373-390 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{7184c07b2f7f4cf99f56c2e508f6c41f,

title = "Invariant verification of nonlinear hybrid automata networks of cardiac cells",

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.",

keywords = "Biological networks, hybrid systems, invariants, verification",

author = "Zhenqi Huang and Chuchu Fan and Alexandru Mereacre and Sayan Mitra and Marta Kwiatkowska",

note = "Copyright: Copyright 2014 Elsevier B.V., All rights reserved.; 26th International Conference on Computer Aided Verification, CAV 2014 - Held as Part of the Vienna Summer of Logic, VSL 2014 ; Conference date: 18-07-2014 Through 22-07-2014",

year = "2014",

doi = "10.1007/978-3-319-08867-9_25",

language = "English (US)",

isbn = "9783319088662",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer-Verlag Berlin Heidelberg",

pages = "373--390",

booktitle = "Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings",

}

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

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 - http://www.scopus.com/inward/record.url?scp=84904815101&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84904815101&partnerID=8YFLogxK

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-Verlag Berlin Heidelberg

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 -