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

Affine systems reachability is the basis of many verification methods. Withfurther computation, methods exist to reason about richer models with inputs,nonlinear differential equations, and hybrid dynamics. As such, the scalabilityof affine systems verification is a prerequisite to scalable analysis for morecomplex systems. In this paper, we improve the scalability of affine systemsverification, in terms of the number of dimensions (variables) in the system.  The reachable states of affine systems can be written in terms of the matrixexponential, and safety checking can be performed at specific time steps withlinear programming. Unfortunately, for large systems with many state variables,this direct approach requires an intractable amount of memory while using anintractable amount of computation time. We overcome these challenges bycombining several methods that leverage common problem structure. Memory isreduced by exploiting initial states that are not full-dimensional and safetyproperties (outputs) over a few linear projections of the state variables.Computation time is saved by using numerical simulations to compute onlyprojections of the matrix exponential relevant for the verification problem.Since large systems often have sparse dynamics, we use Krylov-subspacesimulation approaches based on the Arnoldi or Lanczos iterations. Our methodproduces accurate counter-examples when properties are violated and, in theextreme case with sufficient problem structure, can analyze a system with onebillion real-valued state variables.

Numerical Verification of Affine Systems with up to a Billion Dimensions