scholarly journals ARCH-COMP20 Category Report:Hybrid Systems Theorem Proving

10.29007/bdq9 ◽  
2020 ◽  
Author(s):  
Stefan Mitsch ◽  
Jonathan Julián Huerta Y Munive ◽  
Xiangyu Jin ◽  
Bohua Zhan ◽  
Shuling Wang ◽  
...  
Keyword(s):  
Hybrid Systems ◽  
Theorem Proving ◽  
Proof Checking ◽  
Specific Advice ◽  
Additional Input ◽  
Logical Reason ◽  
Safety Specification ◽  
Characteristic Features ◽  
Experimental Findings ◽  
Friendly Competition

This paper reports on the Hybrid Systems Theorem Proving (HSTP) category in the ARCH-COMP Friendly Competition 2020. The characteristic features of the HSTP category remain as in the previous editions [MST+18, MST+19]: i) The flexibility of pro- gramming languages as structuring principles for hybrid systems, ii) The unambiguity and precision of program semantics, and iii) The mathematical rigor of logical reason- ing principles. The HSTP category especially features many nonlinear and parametric continuous and hybrid systems. Owing to the nature of theorem proving, HSTP again accommodates three modes: A) Automatic in which the entire verification is performed fully automatically without any additional input beyond the original hybrid system and its safety specification. H) Hints in which select proof hints are provided as part of the input problem specification, allowing users to communicate specific advice about the sys- tem such as loop invariants. S) Scripted in which a significant part of the verification is done with dedicated proof scripts or problem-specific proof tactics. This threefold split makes it possible to better identify the sources of scalability and efficiency bottlenecks in hybrid systems theorem proving. The existence of all three categories also makes it easier for new tools with a different focus to participate in the competition, wherever they focus on in the spectrum from fast proof checking all the way to full automation. The types of benchmarks considered and experimental findings with the participating theorem provers KeYmaera, KeYmaera X 4.6.3, KeYmaera X 4.8.0, Isabelle/HOL/Hybrid-Systems-VCs, and HHL Prover are described in this paper as well.

scholarly journals ARCH-COMP19 Category Report: Hybrid Systems Theorem Proving

10.29007/nrv8 ◽  
2019 ◽  
Author(s):  
Stefan Mitsch ◽  
Andrew Sogokon ◽  
Yong Kiam Tan ◽  
Xiangyu Jin ◽  
Bohua Zhan ◽  
...  
Keyword(s):  
Programming Languages ◽  
Hybrid Systems ◽  
Theorem Proving ◽  
Proof Checking ◽  
Specific Advice ◽  
Previous Edition ◽  
Additional Input ◽  
Safety Specification ◽  
Characteristic Features ◽  
Experimental Findings

This paper reports on the Hybrid Systems Theorem Proving (HSTP) category in the ARCH-COMP Friendly Competition 2019. The most important characteristic features of the HSTP category remain as in the previous edition [MST+18]: i) The flexibility of programming languages as structuring principles for hybrid systems, ii) The unambiguity and precision of program semantics, and iii) The mathematical rigor of logical reason- ing principles. The HSTP category especially features many nonlinear and parametric continuous and hybrid systems. Owing to the nature of theorem proving, HSTP again accommodates three modes: A) Automatic in which the entire verification is performed fully automatically without any additional input beyond the original hybrid system and its safety specification. H) Hints in which select proof hints are provided as part of the input problem specification, allowing users to communicate specific advice about the system such as loop invariants. S) Scripted in which a significant part of the verification is done with dedicated proof scripts or problem-specific proof tactics. This threefold split makes it possible to better identify the sources of scalability and efficiency bottlenecks in hybrid systems theorem proving. The existence of all three categories also makes it easier for new tools with a different focus to participate in the competition, wherever they focus on in the spectrum from fast proof checking all the way to full automation. The types of benchmarks considered and experimental findings are described in this paper as well.

scholarly journals ARCH-COMP18 Category Report: Hybrid Systems Theorem Proving

10.29007/vjh3 ◽  
2018 ◽  
Author(s):  
Stefan Mitsch ◽  
Andrew Sogokon ◽  
Yong Kiam Tan ◽  
André Platzer ◽  
Hengjun Zhao ◽  
...  
Keyword(s):  
Programming Languages ◽  
Hybrid Systems ◽  
Hybrid System ◽  
Theorem Proving ◽  
Proof Checking ◽  
Specific Advice ◽  
Additional Input ◽  
Safety Specification ◽  
Experimental Findings ◽  
Friendly Competition

This paper reports on establishing Hybrid Systems Theorem Proving (HSTP) as a new category in the ARCH-COMP Friendly Competition 2018. The most important char- acteristic features of the HSTP category are: i) The flexibility of programming languages as structuring principles for hybrid systems, ii) The unambiguity and precision of program semantics, and iii) The mathematical rigor of logical reasoning principles. The HSTP category especially features many nonlinear and parametric continuous and hybrid sys- tems. Owing to the nature of theorem proving, HSTP is able to accomodate three modes: A) Automatic in which the entire verification is performed fully automatically without any additional input beyond the original hybrid system and its safety specification. H) Hints in which select proof hints are provided as part of the input problem specification, allowing users to communicate specific advice about the system such as loop invariants. S) Scripted in which a significant part of the verification is done with dedicated proof scripts or problem-specific proof tactics. This threefold split makes it possible to better identify the sources of scalability and efficiency bottlenecks in hybrid systems theorem proving. The existence of all three categories also makes it easier for new tools with a different focus to participate in the competition, wherever they focus on in the spectrum from fast proof checking all the way to full automation. The types of benchmarks considered and experimental findings are described in this paper as well.

scholarly journals ARCH-COMP17 Repeatability Evaluation Report

10.29007/7hvk ◽  
2018 ◽  
Author(s):  
Taylor T. Johnson
Keyword(s):  
Formal Verification ◽  
Hybrid Systems ◽  
Benchmark Problems ◽  
Safety Verification ◽  
Evaluation Report ◽  
Standard Practice ◽  
Friendly Competition

This report presents the results of the repeatability evaluation for a friendly competition for formal verification of continuous and hybrid systems. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2017. In its first edition, thirteen tools have been applied to solve benchmark problems for the six competition categories, of which, ten tools were evaluated and passed the repeatability evaluation. The repeatability results represent a snapshot of the current landscape of tools and the types of benchmarks for which they are particularly suited and for which others may repeat their analyses. Due to the diversity of problems in verification of continuous and hybrid systems, as well as basing on standard practice in repeatability evaluations, we evaluate the tools with pass and/or failing being repeatable. These re- sults probably provide the most complete assessment of tools for the safety verification of continuous and hybrid systems up to this date.

INTERNAL ORGANIZATION OF CLASSIFIER NETWORKS TRAINED BY BACKPROPAGATION

1992 ◽  
Vol 06 (01) ◽  
pp. 63-92
Author(s):  
D. F. MICHAELS
Keyword(s):  
Internal Representation ◽  
Training Environment ◽  
Cell Responses ◽  
Training Class ◽  
Separable Problems ◽  
Linear Transform ◽  
Multilayer Neural Networks ◽  
External Training ◽  
Characteristic Features ◽  
Experimental Findings

Backpropagation is one of the most widely used methods for training multilayer neural networks, yet questions still exist regarding how the networks organize internally during (raining to represent the external training environment. This paper presents empirical measurements showing that feedforward networks, when trained on many separable and non-separable problems, learn a characteristic internal representation, herein called the Network Linear Transform (NLT), that is independent of: (a) the initial weights and cell biases, and (b) the number of hidden units. The internal decomposition (defined as the values of cell weights and biases) of the trained nets, however, is greatly dependent upon these quantities. For the case of orthogonal input patterns, the NLT captures a literal image of the training environment, while for linearly-independent and separable linearly-dependent training sets, the NLT: (a) captures characteristic features of the correct input patterns, (b) captures inverted versions of characteristic features of incorrect patterns, and (c) rejects features common to all pattern classes. For non-separable problems, the NLT captures statistical ensemble information about patterns in each training class. The hidden units act as difference detectors and thus convey information that distinguishes input patterns from one another. They separate the patterns into groups that are easily discriminated by the output cells. A linearized mathematical network model is developed that accurately reproduces weight matrices and cell responses for certain separable learning situations, and which supports the experimental findings given above.

Novel experimental findings in the B–Z system employing mixed substrates

1996 ◽  
Vol 74 (1) ◽  
pp. 64-69 ◽  
Author(s):  
V. Jayalakshmi ◽  
R. Ramaswamy
Keyword(s):  
Current Density ◽  
Exchange Current ◽  
Exchange Current Density ◽  
Oscillatory Behaviour ◽  
Mixed Substrates ◽  
Mixed Substrate ◽  
Common Substrate ◽  
The Common ◽  
Characteristic Features ◽  
Experimental Findings

Certain novel features of the Belousov–Zhabotinsky (B–Z) system employing different mixed substrates and Mn(II) as the catalyst are presented. Malic acid is the common substrate together with one of malonic, citric, cyanoacetic, maleic, acetic, oxalic, or tartaric acid as the second substrate. The correlation of the oscillatory behaviour with values of exchange current density establishes the oscillatory control by the redox couple, namely, Mn(III)/Mn(II) and (or) Br2/Br−. Each substrate when used alone gives rise to an oscillatory behaviour with characteristic features that can be compared with the system containing mixed substrate. The combination of substrates provides different modes of oscillatory behaviour such as entrainment, independent, partial inhibition, or complete inhibition. These observations are rationalized in terms of relevant steps involved in the mechanism of the reaction. Key words: mixed substrate, exchange current density, entrainment, independent, inhibition.

scholarly journals ARCH-COMP18 Category Report: Continuous and Hybrid Systems with Linear Continuous Dynamics

10.29007/73mb ◽  
2018 ◽  
Author(s):  
Matthias Althoff ◽  
Stanley Bak ◽  
Xin Chen ◽  
Chuchu Fan ◽  
Marcelo Forets ◽  
...  
Keyword(s):  
Formal Verification ◽  
Hybrid Systems ◽  
Benchmark Problems ◽  
Safety Verification ◽  
Alphabetical Order ◽  
Friendly Competition

This report presents the results of a friendly competition for formal verification of continuous and hybrid systems with linear continuous dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2018. In its second edition, 9 tools have been applied to solve six different benchmark problems in the category for linear continuous dynamics (in alphabetical order): CORA, CORA/SX, C2E2, Flow*, HyDRA, Hylaa, Hylaa-Continuous, JuliaReach, SpaceEx, and XSpeed. This report is a snapshot of the current landscape of tools and the types of benchmarks they are particularly suited for. Due to the diversity of problems, we are not ranking tools, yet the presented results probably provide the most complete assessment of tools for the safety verification of continuous and hybrid systems with linear continuous dynamics up to this date.

scholarly journals ARCH-COMP18 Category Report: Hybrid Systems with Piecewise Constant Dynamics

10.29007/p11g ◽  
2018 ◽  
Author(s):  
Goran Frehse ◽  
Alessandro Abate ◽  
Dieky Adzkiya ◽  
Lei Bu ◽  
Mirco Giacobbe ◽  
...  
Keyword(s):  
Formal Verification ◽  
Hybrid Systems ◽  
Benchmark Problems ◽  
Safety Verification ◽  
Railway Network ◽  
Piecewise Constant ◽  
Friendly Competition

This report presents results of a friendly competition for formal verification of continuous and hybrid systems with piecewise constant dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2018. In this second edition, five tools have been applied to solve five different benchmark problems in the category for piecewise constant dynamics: BACH, Lyse, PHAVer, PHAVer-lite, and VeriSiMPL. Compared to last year, a new tool has participated (PHAVer-lite) and a benchmark has been made more complex (Dutch Railway Network). The result is a snapshot of the current landscape of tools and the types of benchmarks they are particularly suited for. Due to the diversity of problems, we are not ranking tools, yet the presented results probably provide the most complete assessment of tools for the safety verification of continuous and hybrid systems with piecewise constant dynamics up to this date.

scholarly journals ARCH-COMP20 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics

10.29007/zkf6 ◽  
2020 ◽  
Author(s):  
Luca Geretti ◽  
Julien Alexandre Dit Sandretto ◽  
Matthias Althoff ◽  
Luis Benet ◽  
Alexandre Chapoutot ◽  
...  
Keyword(s):  
Nonlinear Dynamics ◽  
Formal Verification ◽  
Hybrid Systems ◽  
Reachability Analysis ◽  
Current Status ◽  
Benchmark Problems ◽  
Hybrid Dynamics ◽  
Friendly Competition

We present the results of a friendly competition for formal verification of continuous and hybrid systems with nonlinear continuous dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2020. This year, 6 tools Ariadne, CORA, DynIbex, Flow*, Isabelle/HOL, and JuliaReach (in alphabetic order) participated. These tools are applied to solve reachability analysis problems on six benchmark problems, two of them featuring hybrid dynamics. We do not rank the tools based on the results, but show the current status and discover the potential advantages of different tools.

Sign in / Sign up

Export Citation Format

Share Document