English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

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 <InlineEquation ID=\"IEq1\" <EquationSource Format=\"TEX\"$\\mathcal{A}$</EquationSource> </InlineEquation> for constructing a low-dimensional model <InlineEquation ID=\"IEq2\" <EquationSource Format=\"TEX\"$\\mathcal{M}$</EquationSource> </InlineEquation>. Simulations of both <InlineEquation ID=\"IEq3\" <EquationSource Format=\"TEX\"$\\mathcal{A}$</EquationSource> </InlineEquation> and <InlineEquation ID=\"IEq4\" <EquationSource Format=\"TEX\"$\\mathcal{M}$</EquationSource> </InlineEquation> are then used to compute the reach tubes for <InlineEquation ID=\"IEq5\" <EquationSource Format=\"TEX\"$\\mathcal{A}$</EquationSource> </InlineEquation>. 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.

Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac Cells