Modeling of ALFA Programs Using PVS Theorem Prover

In Safety critical software failure can have a high price. Such software should be free of errors before it is put into operation. Application of formal methods in the Software Development Life Cycle helps to ensure that the software for safety critical missions are ultra reliable. PVS theorem prover, a formal method tool, can be used for the formal verification of software in ADA Language for Flight Software Application (ALFA.). This paper describes the modeling of ALFA programs for PVS theorem prover. An ALFA2PVS translator is developed which automatically converts the software in ALFA to PVS specification. By this approach the software can be verified formally with respect to underflow/overflow errors and divide by zero conditions without the actual execution of the code.

Modeling of ALFA Programs Using PVS Theorem Prover

In Safety critical software failure can have a high price. Such software should be free of errors before it is put into operation. Application of formal methods in the Software Development Life Cycle helps to ensure that the software for safety critical missions are ultra reliable. PVS theorem prover, a formal method tool, can be used for the formal verification of software in ADA Language for Flight Software Application (ALFA.). This paper describes the modeling of ALFA programs for PVS theorem prover. An ALFA2PVS translator is developed which automatically converts the software in ALFA to PVS specification. By this approach the software can be verified formally with respect to underflow/overflow errors and divide by zero conditions without the actual execution of the code

Computer Theorem Proving and HoTT

Theorem-proving is a one-player game. The history of computer programs being the players goes back to 1956 and the ‘LT’ LOGIC THEORY MACHINE of Newell, Shaw and Simon. In game-playing terms, the ‘initial position’ is the core set of axioms chosen for the particular logic and the ‘moves’ are the rules of inference. Now, the Univalent Foundations Program at IAS Princeton and the resulting ‘HoTT’ book on Homotopy Type Theory have demonstrated the success of a new kind of experimental mathematics using computer theorem proving.

The transaction cost economics theory of the family firm: family-based human asset specificity and the bifurcation bias

We develop a transaction cost economics theory of the family firm, building upon the concepts of family-based asset specificity, bounded rationality, and bounded reliability. We argue that the prosperity and survival of family firms depend on the absence of a dysfunctional bifurcation bias. The bifurcation bias is an expression of bounded reliability, reflected in the de facto asymmetric treatment of family vs. nonfamily assets (especially human assets). We propose that absence of bifurcation bias is critical to fostering reliability in family business functioning. Our study ends the unproductive divide between the agency and stewardship perspectives of the family firm, which offer conflicting accounts of this firm type's functioning. We show that the predictions of the agency and stewardship perspectives can be usefully reconciled when focusing on how family firms address the bifurcation bias or fail to do so.

A scenario for torus T(2) destruction via a global bifurcation

We show a scenario of a two-frequeney torus breakdown, in which a global bifurcation occurs due to the collision of a quasi-periodic torus T(2) with saddle points, creating a heteroclinic saddle connection. We analyze the geometry of this torus-saddle collision by showing the local dynamics and the invariant manifolds (global dynamics) of the saddle points. Moreover, we present detailed evidences of a heteroclinic saddle-focus orbit responsible for the type-if intermittency induced by this global bifurcation. We also characterize this transition to chaos by measuring the Lyapunov exponents and the scaling laws. (C) 2007 Elsevier Ltd. All rights reserved.

ON THE SUPERCRITICALITY OF THE FIRST HOPF BIFURCATION IN A DELAY BOUNDARY PROBLEM

The goal of this paper is to analyze the character of the first Hopf bifurcation (subcritical versus supercritical) that appears in a one-dimensional reaction-diffusion equation with nonlinear boundary conditions of logistic type with delay. We showed in the previous work [Arrieta et al., 2010] that if the delay is small, the unique non-negative equilibrium solution is asymptotically stable. We also showed that, as the delay increases and crosses certain critical value, this equilibrium becomes unstable and undergoes a Hopf bifurcation. This bifurcation is the first one of a cascade occurring as the delay goes to infinity. The structure of this cascade will depend on the parameters appearing in the equation. In this paper, we show that the first bifurcation that occurs is supercritical, that is, when the parameter is bigger than the delay bifurcation value, stable periodic orbits branch off from the constant equilibrium.

Structurable superalgebras of Cartan type

We describe the simple Lie superalgebras arising from the unital structurable superalgebras of characteristic 0 and construct four series of the unital simple structurable superalgebras of Cartan type. We give a classification of simple structurable superalgebras of Cartan type over an algebraically closed field F of characteristic 0. Together with the Faulkner theorem on the classification of classical such superalgebras, it gives a classification of the simple structurable superalgebras over F. Crown Copyright (C) 2010 Published by Elsevier Inc. All rights reserved.

PERIODIC PERTURBATION of QUADRATIC SYSTEMS WITH TWO INFINITE HETEROCLINIC CYCLES

Conselho Nacional de Desenvolvimento Científico e Tecnológico (CNPq)

Hartman-Grobman decomposition when in presence of jumps in the relative degree of the dynamics in an energy harvesting device

This work deals with the nonlinear piezoelectric coupling in vibration-based energy harvesting, done by A. Triplett and D.D. Quinn in J. of Intelligent Material Syst. and Structures (2009). In that paper the first order nonlinear fundamental equation has a three dimensional state variable. Introducing both observable and control variables in such a way the controlled system became a SISO system, we can obtain as a corollary that for a particular choice of the observable variable it is possible to present an explicit functional relation between this variable one, and the variable representing the charge harvested. After-by observing that the structure in the Input-Output decomposition essentially changes depending on the relative degree changes, presenting bifurcation branches in its zero dynamics-we are able in to identify this type of bifurcation indicating its close relation with the Hartman - Grobman theorem telling about decomposition into stable and the unstable manifolds for hyperbolic points.

Landau and Kolmogoroff type polynomial inequalities

Let 0type inequalitiesparallel to f((f))parallel to(2) less than or equal to A parallel to f(m)parallel to + B parallel to f parallel to/ A theta(k) + B mu(k),with certain constants theta(k)e mu(k), which hold for every f is an element of pi(n) (pi(n) denotes the space of real algebraic polynomials of degree not exceeding n).For the particular case j=1 and m=2, we provide a complete characterisation of the positive constants A and B, for which the corresponding Landau type polynomial inequalities parallel to f'parallel to less than or equal toA parallel to f parallel to + B parallel to f parallel to/ A theta(k) + B mu(k)hold. In each case we determine the corresponding extremal polynomials for which equalities are attained.

NONDEGENERATE UMBILICS, THE PATH FORMULATION and GRADIENT BIFURCATION PROBLEMS

Fundação de Amparo à Pesquisa do Estado de São Paulo (FAPESP)

A comment on a nonideal centrifugal vibrator machine behavior with soft and hard springs

This paper concerns a type of rotating machine (centrifugal vibrator), which is supported on a nonlinear spring. This is a nonideal kind of mechanical system. The goal of the present work is to show the striking differences between the cases where we take into account soft and hard spring types. For soft spring, we prove the existence of homoclinic chaos. By using the Melnikov's Method, we show the existence of an interval with the following property: if a certain parameter belongs to this interval, then we have chaotic behavior; otherwise, this does not happen. Furthermore, if we use an appropriate damping coefficient, the chaotic behavior can be avoided. For hard spring, we prove the existence of Hopf's Bifurcation, by using reduction to Center Manifolds and the Bezout Theorem (a classical result about algebraic plane curves).

On the appearance of a Hopf bifurcation in a non-ideal mechanical problem

In this paper we studied a non-ideal system with two degrees of freedom consisting of a dumped nonlinear oscillator coupled to a rotatory part. We investigated the stability of the equilibrium point of the system and we obtain, in the critical case, sufficient conditions in order to obtain an appropriate Normal Form. From this, we get conditions for the appearance of Hopf Bifurcation when the difference between the driving torque and the resisting torque is small. It was necessary to use the Bezout Theorem, a classical result of Algebraic Geometry, in the obtaining of the foregoing results. (C) 2003 Elsevier Ltd. All rights reserved.

Quantum entanglement and fixed point Hopf bifurcation

We present the qualitative differences in the phase transitions of the mono-mode Dicke model in its integrable and chaotic versions. These qualitative differences are shown to be connected to the degree of entanglement of the ground state correlations as measured by the linear entropy. We show that a first order phase transition occurs in the integrable case whereas a second order in the chaotic one. This difference is also reflected in the classical limit: for the integrable case the stable fixed point in phase space undergoes a Hopf type whereas the second one a pitchfork type bifurcation. The calculation of the atomic Wigner functions of the ground state follows the same trends. Moreover, strong correlations are evidenced by its negative parts. (c) 2006 Elsevier B.V. All rights reserved.

Path formulation for Z(2) circle plus Z(2)-equivariant bifurcation problems

M. Manoel and I. Stewart 0101) classify Z(2) circle plus Z(2)-equivariant bifurcation problems up to codimension 3 and 1 modal parameter, using the classical techniques of singularity theory of Golubistky and Schaeffer [8]. In this paper we classify these same problems using an alternative form: the path formulation (Theorem 6.1). One of the advantages of this method is that the calculates to obtain the normal forms are easier. Furthermore, in our classification we observe the presence of only one modal parameter in the generic core. It differs from the classical classification where the core has 2 modal parameters. We finish this work comparing our classification to the one obtained in [10].