scholarly journals Pegasus: sound continuous invariant generation

2021 ◽  
Author(s):  
Andrew Sogokon ◽  
Stefan Mitsch ◽  
Yong Kiam Tan ◽  
Katherine Cordwell ◽  
André Platzer
Keyword(s):  
Hybrid Systems ◽  
Experimental Evaluation ◽  
Discrete Systems ◽  
Automatic Generation ◽  
Theorem Prover ◽  
Continuous Systems ◽  
Formal Proofs ◽  
Deductive Verification ◽  
Invariant Generation ◽  
Discrete Invariants

AbstractContinuous invariants are an important component in deductive verification of hybrid and continuous systems. Just like discrete invariants are used to reason about correctness in discrete systems without having to unroll their loops, continuous invariants are used to reason about differential equations without having to solve them. Automatic generation of continuous invariants remains one of the biggest practical challenges to the automation of formal proofs of safety for hybrid systems. There are at present many disparate methods available for generating continuous invariants; however, this wealth of diverse techniques presents a number of challenges, with different methods having different strengths and weaknesses. To address some of these challenges, we develop Pegasus: an automatic continuous invariant generator which allows for combinations of various methods, and integrate it with the KeYmaera X theorem prover for hybrid systems. We describe some of the architectural aspects of this integration, comment on its methods and challenges, and present an experimental evaluation on a suite of benchmarks.

scholarly journals Hidden Attractors in Discrete Dynamical Systems

Entropy ◽  
2021 ◽  
Vol 23 (5) ◽  
pp. 616
Author(s):  
Marek Berezowski ◽  
Marcin Lawnik
Keyword(s):  
Dynamical Systems ◽  
Chaos Theory ◽  
Scientific Literature ◽  
Discrete Systems ◽  
Discrete Dynamical Systems ◽  
Continuous Systems ◽  
Hidden Attractors ◽  
Negative Effects ◽  
Chemical Reactors ◽  
Points Of View

Research using chaos theory allows for a better understanding of many phenomena modeled by means of dynamical systems. The appearance of chaos in a given process can lead to very negative effects, e.g., in the construction of bridges or in systems based on chemical reactors. This problem is important, especially when in a given dynamic process there are so-called hidden attractors. In the scientific literature, we can find many works that deal with this issue from both the theoretical and practical points of view. The vast majority of these works concern multidimensional continuous systems. Our work shows these attractors in discrete systems. They can occur in Newton’s recursion and in numerical integration.

scholarly journals Invariants and Robustness of BIP Models

10.29007/prxp ◽  
2018 ◽  
Author(s):  
Jan Olaf Blech ◽  
Thanh-Hung Nguyen ◽  
Michael Perin
Keyword(s):  
Embedded Systems ◽  
Higher Order ◽  
Theorem Prover ◽  
Important Goal ◽  
Invariant Generation ◽  
Execution Traces ◽  
Verification Tool ◽  
Verification Tools ◽  
Generation Mechanisms ◽  
Natural Way

In this paper we present on-going work addressing the problem of automatically generating realistic and guaranteed correct invariants. Since invariant generation mechanisms are error-prone, after the computation of invariants by a verification tool, we formally prove that the generated invariants are indeed invariants of the considered systems using a higher-order theorem prover and automated techniques. We regard invariants for BIP models. BIP (behavior, interaction, priority) is a language for specifying asynchronous component based systems. Proving that an invariant holds often requires an induction on possible system execution traces. For this reason, apart from generating invariants that precisely capture a system’s behavior, inductiveness of invariants is an important goal. We establish a notion of robust BIP models. These can be automatically constructed from our original non-robust BIP models and over-approximate their behavior. We motivate that invariants of robust BIP models capture the behavior of systems in a more natural way than invariants of corresponding non-robust BIP models. Robust BIP models take imprecision due to values delivered by sensors into account. Invariants of robust BIP models tend to be inductive and are also invariants of the original non-robust BIP model. Therefore they may be used by our verification tools and it is easy to show their correctness in a higher-order theorem prover. The presented work is developed to verify the results of a deadlock-checking tool for embedded systems after their computations. Therewith, we gain confidence in the provided analysis results.

scholarly journals Sensitivity Analysis for Hybrid Systems and Systems With Memory

2019 ◽  
Vol 14 (9) ◽  
Author(s):  
Radu Serban ◽  
Antonio Recuero
Keyword(s):  
Hybrid Systems ◽  
Exponential Model ◽  
Differential Algebraic Equations ◽  
Mode Switching ◽  
Continuous Systems ◽  
Algebraic Equations ◽  
Adjoint Sensitivity ◽  
Adjoint Systems ◽  
Systems With Memory ◽  
With Memory

We present an adjoint sensitivity method for hybrid discrete—continuous systems, extending previously published forward sensitivity methods (FSA). We treat ordinary differential equations (ODEs) and differential-algebraic equations (DAEs) of index up to two (Hessenberg) and provide sufficient solvability conditions for consistent initialization and state transfer at mode switching points, for both the sensitivity and adjoint systems. Furthermore, we extend the analysis to so-called hybrid systems with memory where the dynamics of any given mode depend explicitly on the states at the last mode transition point. We present and discuss several numerical examples, including a computational mechanics problem based on the so-called exponential model (EM) constitutive material law for steel reinforcement under cyclic loading.

Inverse Problems in Vibration

1986 ◽  
Vol 39 (7) ◽  
pp. 1013-1018 ◽  
Author(s):  
Graham M. L. Gladwell
Keyword(s):  
Inverse Problems ◽  
Eigenvalue Problems ◽  
Discrete Systems ◽  
Free Vibrations ◽  
Continuous Systems ◽  
Thin Beam ◽  
Inverse Eigenvalue Problems ◽  
Elastic Systems ◽  
Inverse Eigenvalue ◽  
Sturm Liouville

This article concerns infinitesimal free vibrations of undamped elastic systems of finite extent. A review is made of the literature relating to the unique reconstruction of a vibrating system from natural frequency data. The literature is divided into two groups—those papers concerning discrete systems, for which the inverse problems are closely related to matrix inverse eigenvalue problems, and those concerning continuous systems governed either by one or the other of the Sturm–Liouville equations or by the Euler–Bernoulli equation for flexural vibrations of a thin beam.

scholarly journals Reasoning About Loops Using Vampire

10.29007/tcvj ◽  
2018 ◽  
Author(s):  
Laura Kovács ◽  
Simon Robillard
Keyword(s):  
Order Logic ◽  
Theorem Prover ◽  
Program Correctness ◽  
Command Language ◽  
Rule Based ◽  
Invariant Generation ◽  
Partial Correctness ◽  
First Order ◽  
Deductive Systems ◽  
Fully Automatic

In 2009, the symbol elimination method for loop invariant generationwas introduced, which used saturationtheorem proving in first-order logic to generate quantified invariantsof programs with arrays. Symbol elimination is fully automatic,requires no user guidance, and it is the first ever approach able togenerate invariants with alternations of quantifiers. In this paperwe describe a number of improvements and extensions to symbolelimination and invariant generation using first-order theoremproving, in particular the Vampire theorem prover. Rather than beinglimited to a specific programming language, our approach to reasoningabout loops in Vampire relies on a simple guarded command language forits input, which can be used as an interface for more complex andrealistic imperative languages. We propose new ways for extendingquantified loop properties describing valid loop properties, bysimplifying the properties over array updates and next staterelations. We also extend symbol elimination with pre- andpost-conditions of loops. We use the loop specification to generateonly invariants that are relevant, that is, invariants that are neededfor proving partial correctness of loops. Further, we turn symbolelimination into an automatic approach proving program correctness,providing an alternative method to Hoare-rule based loop verificationor other deductive systems. We present our newly redesignedimplementation of loop reasoning in Vampire and also report onexperimental results.

scholarly journals Tool Presentation: Isabelle/HOL for Reachability Analysis of Continuous Systems

10.29007/b3wr ◽  
2018 ◽  
Author(s):  
Fabian Immler
Keyword(s):  
Distinctive Feature ◽  
Reachability Analysis ◽  
Theorem Prover ◽  
Continuous Systems ◽  
Affine Arithmetic ◽  
Discretization Errors ◽  
Runge Kutta

We present a tool for reachability analysis of continuous systems based onaffine arithmetic and Runge-Kutta methods. The distinctive feature of our toolis its verification in the interactive theorem prover Isabelle/HOL: thealgorithm is guaranteed to compute safe overapproximations, taking into accountall round-off and discretization errors.

Non-stationary dynamic system characteristics recovery from three test signals

2020 ◽  
pp. 9-15
Author(s):  
Ilia V. Boikov ◽  
Nikolay P. Krivulin
Keyword(s):  
Dynamical Systems ◽  
Impulse Response ◽  
Discrete Systems ◽  
Exact Formula ◽  
Algebraic Expression ◽  
Continuous Systems ◽  
Exact Reconstruction ◽  
Input Signals ◽  
The Laplace Transform ◽  
System Output

Algorithms of exact restoration in an analytical form of dynamic characteristics of non-stationary dynamic systems are constructed. Non-stationary continuous dynamical systems modeled by Volterra integral equations of the first kind and non-stationary discrete dynamical systems modeled by discrete analogues of Volterra integral equations of the first kind are considered.The article consists of an introduction and three sections: 1) The exact restoration of the dynamic characteristics of continuous systems, 2) The restoration of the transition characteristics of discrete systems, 3) Conclusions. The introduction provides a statement of the problem and provides an overview of dynamical systems for which algorithms for exact reconstruction in ananalytical form of the impulse response (in the case of continuous systems) and the transition characteristic (in the case of discrete systems) are constructed. In the first section, the algorithm is constructed for the exact reconstruction of the impulse response of an non-stationary continuous dynamic system from three interconnected input signals. The first signal may be arbitrary, the second and third signals are associated with the first signal by integral operator. The exact formula for the Laplace transform of the impulse response, represented by an algebraic expression from the Laplace transform of the system output signals, is given. A model example illustrating the effectiveness of the algorithm is given. The practical application of the presented algorithm isdiscussed. In the second section, an algorithm is constructed for the exact reconstruction of the transition response of a non-stationary discrete dynamical system from three input signals that are interconnected. The first signal may be arbitrary, the second and third signals are associated with the first summing operator. The exact formula of the Z-transform of the transition characteristic is presented, which is represented by an algebraic expression from the Z-transform of the system output signals. A model example is given. The “Conclusions” section provides a summary of the results presented in the article and describes the dynamic systems to which the proposed algorithms can be extended.

Discrete Finite Element Method Application for Analysis of Unreinforced-Masonry Underground Structures

2015 ◽  
Vol 2522 (1) ◽  
pp. 131-136 ◽  
Author(s):  
Iraj H. P. Mamaghani
Keyword(s):  
Finite Element Method ◽  
Finite Element ◽  
Discrete Systems ◽  
Unreinforced Masonry ◽  
Continuous Systems ◽  
Underground Structures ◽  
Interface Elements ◽  
Underground Openings ◽  
Discrete Finite Element ◽  
Element Method

Unreinforced-masonry underground structures are composed of a finite number of distinct interacting blocks that have length scales relatively comparable with the underground openings of interest. Therefore, these structures are ideal candidates for modeling as discrete systems instead of as continuous systems. The discrete finite element method (DFEM) developed by the author to model discontinuous media consisting of blocks of arbitrary shapes was adopted for the static analysis of unreinforced masonry underground structures. The developed DFEM was based on the principles of the finite element method incorporating contact elements. The DFEM considers blocks as subdomains and represents them by solid elements. Contact elements, which are far superior to joint or interface elements, are used to model block interactions such as sliding or separation. In this study, the DFEM is briefly reviewed; then, through some illustrative examples, the applicability of the DFEM to the analysis of unreinforced-masonry underground structures is examined and discussed. It is shown that the DFEM provides an efficient tool for researchers and practical engineers in designing, analyzing, and studying the behavior of unreinforced masonry underground structures under static loading.

Sign in / Sign up

Export Citation Format

Share Document