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-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 Subtree matching by pushdown automata

2010 ◽  
Vol 7 (2) ◽  
pp. 331-357 ◽  
Author(s):  
Tomás Flouri ◽  
Jan Janousek ◽  
Bořivoj Melichar
Keyword(s):  
Programming Languages ◽  
Theorem Proving ◽  
Systematic Approach ◽  
Finite Automata ◽  
Term Rewriting ◽  
Mechanical Theorem Proving ◽  
Pushdown Automaton ◽  
String Pattern ◽  
Pushdown Automata ◽  
Mechanical Theorem

Subtree matching is an important problem in Computer Science on which a number of tasks, such as mechanical theorem proving, term-rewriting, symbolic computation and nonprocedural programming languages are based on. A systematic approach to the construction of subtree pattern matchers by deterministic pushdown automata, which read subject trees in prefix and postfix notation, is presented. The method is analogous to the construction of string pattern matchers: for a given pattern, a nondeterministic pushdown automaton is created and is then determinised. In addition, it is shown that the size of the resulting deterministic pushdown automata directly corresponds to the size of the existing string pattern matchers based on finite automata.

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 Structured Proofs for Adversarial Cyber-Physical Systems

2021 ◽  
Vol 20 (5s) ◽  
pp. 1-26
Author(s):  
Brandon Bohrer ◽  
André Platzer
Keyword(s):  
Hybrid Systems ◽  
Differential Game ◽  
Programming Language ◽  
First Language ◽  
Cyber Physical Systems ◽  
Proof Checking ◽  
Game Logic ◽  
Physical Systems ◽  
Safety Critical ◽  
High Level

Many cyber-physical systems (CPS) are safety-critical, so it is important to formally verify them, e.g. in formal logics that show a model’s correctness specification always holds. Constructive Differential Game Logic ( CdGL ) is such a logic for (constructive) hybrid games, including hybrid systems. To overcome undecidability, the user first writes a proof, for which we present a proof-checking tool. We introduce Kaisar , the first language and tool for CdGL proofs, which until now could only be written by hand with a low-level proof calculus. Kaisar’s structured proofs simplify challenging CPS proof tasks, especially by using programming language principles and high-level stateful reasoning. Kaisar exploits CdGL ’s constructivity and refinement relations to build proofs around models of game strategies. The evaluation reproduces and extends existing case studies on 1D and 2D driving. Proof metrics are compared and reported experiences are discussed for the original studies and their reproductions.

scholarly journals Chlamydia Pneumoniae and Chronic Diseases with a Great Impact on Public Health

2008 ◽  
Vol 21 (4) ◽  
pp. 1041-1043 ◽  
Author(s):  
R. Sessa ◽  
P. Cipriani ◽  
M. Di Pietro ◽  
G. Schiavoni ◽  
I. Santino ◽  
...  
Keyword(s):  
Public Health ◽  
Immune Response ◽  
T Cells ◽  
Chronic Diseases ◽  
Chlamydia Pneumoniae ◽  
T Cell Apoptosis ◽  
Tnf Α ◽  
Characteristic Features ◽  
Experimental Findings ◽  
Tract Infections

Chlamydia pneumoniae is recognised as a common cause of respiratory tract infections and has recently been implicated in several extrapulmonary chronic diseases, with great impact on public health, such as atherosclerosis, multiple sclerosis and Alzheimer's disease. The involvement of C. pneumoniae in such diseases may be correlated to characteristic features of this pathogen, including intracellular growth and ability to induce persistent forms. C. pneumoniae persistent forms are inherently more suited to evade the host immune response and are more difficult to eradicate by antibiotics. Our preliminary experimental findings show that interaction of C. pneumoniae with macrophages and/or T cells characterized by interference with TNF-α production, and redox state, culminates in the induction of T cell apoptosis and survival of infected macrophages. Based on our evidence, the poor cooperation between T cells and macrophages could lead to an inappropriate immune response against C. pneumoniae that may therefore promote the development of extrapulmonary chronic diseases.

Sign in / Sign up

Export Citation Format

Share Document