TY - GEN
T1 - ARCH-COMP21 Category Report
T2 - 8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21)
AU - Johnson, Taylor T.
AU - Lopez, Diego Manzanas
AU - Benet, Luis
AU - Forets, Marcelo
AU - Guadalupe, Sebastián
AU - Schilling, Christian
AU - Ivanov, Radoslav
AU - Carpenter, Taylor J.
AU - Weimer, James
AU - Lee, Insup
PY - 2021
Y1 - 2021
N2 - This report presents the results of a friendly competition for formal verification of continuous and hybrid systems with artificial intelligence (AI) components. Specifically, machine learning (ML) components in cyber-physical systems (CPS), such as feedforward neural networks used as feedback controllers in closed-loop systems are considered, which is a class of systems classically known as intelligent control systems, or in more modern and specific terms, neural network control systems (NNCS). We more broadly refer to this category as AI and NNCS (AINNCS). The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2021. In the third edition of this AINNCS category at ARCH-COMP, three tools have been applied to solve seven different benchmark problems, (in alphabetical order): JuliaReach, NNV, and Verisig. JuliaReach is a new participant in this category, Verisig participated previously in 2019 and NNV has participated in all previous competitions. This report is a snapshot of the current landscape of tools and the types of benchmarks for which these tools are suited. Due to the diversity of problems, lack of a shared hardware platform, and the early stage of the competition, we are not ranking tools in terms of performance, yet the presented results combined with 2020 results probably provide the most complete assessment of current tools for safety verification of NNCS.
AB - This report presents the results of a friendly competition for formal verification of continuous and hybrid systems with artificial intelligence (AI) components. Specifically, machine learning (ML) components in cyber-physical systems (CPS), such as feedforward neural networks used as feedback controllers in closed-loop systems are considered, which is a class of systems classically known as intelligent control systems, or in more modern and specific terms, neural network control systems (NNCS). We more broadly refer to this category as AI and NNCS (AINNCS). The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2021. In the third edition of this AINNCS category at ARCH-COMP, three tools have been applied to solve seven different benchmark problems, (in alphabetical order): JuliaReach, NNV, and Verisig. JuliaReach is a new participant in this category, Verisig participated previously in 2019 and NNV has participated in all previous competitions. This report is a snapshot of the current landscape of tools and the types of benchmarks for which these tools are suited. Due to the diversity of problems, lack of a shared hardware platform, and the early stage of the competition, we are not ranking tools in terms of performance, yet the presented results combined with 2020 results probably provide the most complete assessment of current tools for safety verification of NNCS.
U2 - 10.29007/kfk9
DO - 10.29007/kfk9
M3 - Article in proceeding
T3 - EPiC Series in Computing
SP - 90
EP - 119
BT - 8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21)
A2 - Frehse, G.
A2 - Althoff, M.
PB - EasyChair
Y2 - 9 July 2021 through 9 July 2021
ER -