JuliaReach: a Toolbox for Set-Based Reachability

被引：67

作者：

Bogomolov, Sergiy ^{[1
]}

Forets, Marcelo ^{[2
]}

Frehse, Goran ^{[3
]}

Potomkin, Kostiantyn ^{[1
]}

Schilling, Christian ^{[4
]}

机构：

[1] Australian Natl Univ, Canberra, ACT, Australia

[2] UdelaR, CURE, Maldonado, Uruguay

[3] ENSTA ParisTech, U2IS, Palaiseau, France

[4] IST Austria, Klosterneuburg, Austria

来源：

PROCEEDINGS OF THE 2019 22ND ACM INTERNATIONAL CONFERENCE ON HYBRID SYSTEMS: COMPUTATION AND CONTROL (HSCC '19) | 2019年

基金：

奥地利科学基金会;

关键词：

reachability analysis; hybrid systems; lazy computation;

D O I：

10.1145/3302504.3311804

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

We present JULIAREACH, a toolbox for set-based reachability analysis of dynamical systems. JULIAREACH consists of two main packages: Reachability, containing implementations of reachability algorithms for continuous and hybrid systems, and LazySets, a standalone library that implements state-of-the-art algorithms for calculus with convex sets. The library offers both concrete and lazy set representations, where the latter stands for the ability to delay set computations until they are needed. The choice of the programming language Julia and the accompanying documentation of our toolbox allow researchers to easily translate set-based algorithms from mathematics to software in a platform-independent way, while achieving runtime performance that is comparable to statically compiled languages. Combining lazy operations in high dimensions and explicit computations in low dimensions, JULIAREACH can be applied to solve complex, large-scale problems.

引用

页码：39 / 44

页数：6

共 23 条

[1]

Althoff M., 2015, P WORKSH APPL VER CO, DOI DOI 10.29007/ZBKV

[2]

Althoff M., 2018, ARCH18, P23

[3] THE ALGORITHMIC ANALYSIS OF HYBRID SYSTEMS [J].

ALUR, R ;

COURCOUBETIS, C ;

HALBWACHS, N ;

HENZINGER, TA ;

HO, PH ;

NICOLLIN, X ;

OLIVERO, A ;

SIFAKIS, J ;

YOVINE, S .

THEORETICAL COMPUTER SCIENCE, 1995, 138 (01) :3-34

[4]

Alur R., 1993, LNCS, V736, P209, DOI [10.1007/3-540-57318-6_30, DOI 10.1007/3-540-57318-6_30, 10.1007/3-540-57318, DOI 10.1007/3-540-57318, DOI 10.1007/3-540-57318-6, 10.1007]

[5] Simulation-Equivalent Reachability of Large Linear Systems with Inputs [J].

Bak, Stanley ;

Duggirala, Parasara Sridhar .

COMPUTER AIDED VERIFICATION, CAV 2017, PT I, 2017, 10426 :401-420

[6] Julia: A Fresh Approach to Numerical Computing [J].

Bezanson, Jeff ;

Edelman, Alan ;

Karpinski, Stefan ;

Shah, Viral B. .

SIAM REVIEW, 2017, 59 (01) :65-98

[7] Assume-guarantee abstraction refinement meets hybrid systems [J].

Bogomolov, Sergiy ;

Frehse, Goran ;

Greitschus, Marius ;

Grosu, Radu ;

Pasareanu, Corina ;

Podelski, Andreas ;

Strump, Thomas .

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2014, 8855 :116-131

[8]

Bogomolov Sergiy, 2012, Computer Aided Verification. Proceedings 24th International Conference, CAV 2012, P479, DOI 10.1007/978-3-642-31424-7_35

[9] Reach Set Approximation through Decomposition with Low-dimensional Sets and High-dimensional Matrices [J].

Bogomolov, Sergiy ;

Forets, Marcelo ;

Frehse, Goran ;

Viry, Frederic ;

Podelski, Andreas ;

Schilling, Christian .

HSCC 2018: PROCEEDINGS OF THE 21ST INTERNATIONAL CONFERENCE ON HYBRID SYSTEMS: COMPUTATION AND CONTROL (PART OF CPS WEEK), 2018, :41-50

[10]

Bogomolov Sergiy, 2015, STTT

← 1 2 3 →