Comparison for DNA primary sequence

In this article, two schemes are suggested based on three exons of beta-globin gene belonging to 10 species for comparison of DNA primary sequences. At first, the positions of four nucleic acid bases were extracted, and then based on the information, as the numerical characterization of DNA sequences, the sequence invariants were derived. Sequences comparisons of 10 species selected in this work by using these invariants were performed. The results, especially with scheme 2, are quite satisfactory.

On highly discriminating molecular topological index

A highly discriminating molecular topological index, EAID, is proposed based on the extended adjacency matrix. A systematic search for degeneracy was performed for 3 807 434 alkane trees, 202 558 complex cyclic or polycyclic graphs, and 430 472 structures containing heteroatoms. No counterexamples (two or more nonisomorphic structures with the same EAID number) were found. This is a hitherto unheard of power of discrimination. Thus EAID might be possibly used as supplementary reference for CAS Registry Numbers for structure documentation.

A new topological index for the Changchun institute of applied chemistry C-13 NMR information system

A method to assign a single number representation for each atom (node) in a molecular graph, Atomic IDentification (AID) number, is proposed based on the counts of weighted paths terminated on that atom. Then, a new topological index, Molecular IDentification (MID) number is developed from AID. The MID is tested systematically, over half a million of structures are examined, and MID shows high discrimination for various structural isomers. Thus it can be used for documentation in the Changchun Institute of Chemistry C-13 NMR information system.

ESTIMATION OF THE ONE-PHASE STRUCTURE SEMINVARIANTS IN THE SINGLE ISOMORPHOUS REPLACEMENT CASE - AN APPLICATION OF HAUPTMANS DISTRIBUTION

A method for estimating the one-phase structure seminvariants (OPSSs) having values of 0 or pi has been proposed on the basis of the probabilistic theory of the three-phase structure invariants for a pair of isomorphous structures [Hauptman (1982). Acta Cryst. A38, 289-294]. The test calculations using error-free diffraction data of protein cytochrome c(550) and its PtCl42- derivative show that reliable estimates of a number of the OPSSs can be obtained. The reliability of the estimation increases with the increase of the differences between diffraction intensities of the native protein and its heavy-atom derivative. A means to estimate the parameters of the distribution from the diffraction ratio is suggested.

PROBABILISTIC ESTIMATION OF THE STRUCTURE SEMINVARIANTS IN THE MONOCLINIC AND ORTHORHOMBIC SYSTEMS WHEN ANOMALOUS SCATTERERS ARE PRESENT

The estimate formulas for the two-phase structure seminvariants (TPSSs) in the presence of anomalous scattering are obtained from the estimate of the two-phase structure invariants [Hauptman (1982). Acta Cryst. A38, 632-641; Giacovazzo (1983). Acta Cryst.

A NEW SCHEME FOR ASSIGNMENT OF A CANONICAL CONNECTION TABLE

A new algorithm for deriving canonical numbering of atoms in a molecular graph has been developed. Some graph invariants, such as node properties, degree (connectivity), topological path, the smallest node ring index, etc., are encoded together to partit

Algebraic Functions For Recognition

In the general case, a trilinear relationship between three perspective views is shown to exist. The trilinearity result is shown to be of much practical use in visual recognition by alignment --- yielding a direct method that cuts through the computations of camera transformation, scene structure and epipolar geometry. The proof of the central result may be of further interest as it demonstrates certain regularities across homographies of the plane and introduces new view invariants. Experiments on simulated and real image data were conducted, including a comparative analysis with epipolar intersection and the linear combination methods, with results indicating a greater degree of robustness in practice and a higher level of performance in re-projection tasks.

Recognizing 3-D Objects Using 2-D Images

We discuss a strategy for visual recognition by forming groups of salient image features, and then using these groups to index into a data base to find all of the matching groups of model features. We discuss the most space efficient possible method of representing 3-D models for indexing from 2-D data, and show how to account for sensing error when indexing. We also present a convex grouping method that is robust and efficient, both theoretically and in practice. Finally, we combine these modules into a complete recognition system, and test its performance on many real images.

Era uma vez dentro de nós!

Dissertação apresentada à Universidade Fernando Pessoa como parte dos requisitos para obtenção do grau de Mestre em Criatividade e Inovação

Safe Compositional Network Sketches: NetSketch Tool Implementation

Numerous problems exist that can be modeled as traffic through a network in which constraints exist to regulate flow. Vehicular road travel, computer networks, and cloud based resource distribution, among others all have natural representations in this manner. As these networks grow in size and/or complexity, analysis and certification of the safety invariants becomes increasingly costly. The NetSketch formalism introduces a lightweight verification framework that allows for greater scalability than traditional analysis methods. The NetSketch tool was developed to provide the power of this formalism in an easy to use and intuitive user interface.

Modal Matching for Correspondence and Recognition

Modal matching is a new method for establishing correspondences and computing canonical descriptions. The method is based on the idea of describing objects in terms of generalized symmetries, as defined by each object's eigenmodes. The resulting modal description is used for object recognition and categorization, where shape similarities are expressed as the amounts of modal deformation energy needed to align the two objects. In general, modes provide a global-to-local ordering of shape deformation and thus allow for selecting which types of deformations are used in object alignment and comparison. In contrast to previous techniques, which required correspondence to be computed with an initial or prototype shape, modal matching utilizes a new type of finite element formulation that allows for an object's eigenmodes to be computed directly from available image information. This improved formulation provides greater generality and accuracy, and is applicable to data of any dimensionality. Correspondence results with 2-D contour and point feature data are shown, and recognition experiments with 2-D images of hand tools and airplanes are described.

Safe Compositional Network Sketches: Tool & Use Cases

NetSketch is a tool that enables the specification of network-flow applications and the certification of desirable safety properties imposed thereon. NetSketch is conceived to assist system integrators in two types of activities: modeling and design. As a modeling tool, it enables the abstraction of an existing system so as to retain sufficient enough details to enable future analysis of safety properties. As a design tool, NetSketch enables the exploration of alternative safe designs as well as the identification of minimal requirements for outsourced subsystems. NetSketch embodies a lightweight formal verification philosophy, whereby the power (but not the heavy machinery) of a rigorous formalism is made accessible to users via a friendly interface. NetSketch does so by exposing tradeoffs between exactness of analysis and scalability, and by combining traditional whole-system analysis with a more flexible compositional analysis approach based on a strongly-typed, Domain-Specific Language (DSL) to specify network configurations at various levels of sketchiness along with invariants that need to be enforced thereupon. In this paper, we overview NetSketch, highlight its salient features, and illustrate how it could be used in applications, including the management/shaping of traffic flows in a vehicular network (as a proxy for CPS applications) and in a streaming media network (as a proxy for Internet applications). In a companion paper, we define the formal system underlying the operation of NetSketch, in particular the DSL behind NetSketch's user-interface when used in "sketch mode", and prove its soundness relative to appropriately-defined notions of validity.

Safe Compositional Network Sketches: The Formal Framework

NetSketch is a tool for the specification of constrained-flow applications and the certification of desirable safety properties imposed thereon. NetSketch is conceived to assist system integrators in two types of activities: modeling and design. As a modeling tool, it enables the abstraction of an existing system while retaining sufficient information about it to carry out future analysis of safety properties. As a design tool, NetSketch enables the exploration of alternative safe designs as well as the identification of minimal requirements for outsourced subsystems. NetSketch embodies a lightweight formal verification philosophy, whereby the power (but not the heavy machinery) of a rigorous formalism is made accessible to users via a friendly interface. NetSketch does so by exposing tradeoffs between exactness of analysis and scalability, and by combining traditional whole-system analysis with a more flexible compositional analysis. The compositional analysis is based on a strongly-typed Domain-Specific Language (DSL) for describing and reasoning about constrained-flow networks at various levels of sketchiness along with invariants that need to be enforced thereupon. In this paper, we define the formal system underlying the operation of NetSketch, in particular the DSL behind NetSketch's user-interface when used in "sketch mode", and prove its soundness relative to appropriately-defined notions of validity. In a companion paper [6], we overview NetSketch, highlight its salient features, and illustrate how it could be used in two applications: the management/shaping of traffic flows in a vehicular network (as a proxy for CPS applications) and in a streaming media network (as a proxy for Internet applications).

Verification with Natural Contexts: Soundness of Safe Compositional Network Sketches

In research areas involving mathematical rigor, there are numerous benefits to adopting a formal representation of models and arguments: reusability, automatic evaluation of examples, and verification of consistency and correctness. However, accessibility has not been a priority in the design of formal verification tools that can provide these benefits. In earlier work [30] we attempt to address this broad problem by proposing several specific design criteria organized around the notion of a natural context: the sphere of awareness a working human user maintains of the relevant constructs, arguments, experiences, and background materials necessary to accomplish the task at hand. In this report we evaluate our proposed design criteria by utilizing within the context of novel research a formal reasoning system that is designed according to these criteria. In particular, we consider how the design and capabilities of the formal reasoning system that we employ influence, aid, or hinder our ability to accomplish a formal reasoning task – the assembly of a machine-verifiable proof pertaining to the NetSketch formalism. NetSketch is a tool for the specification of constrained-flow applications and the certification of desirable safety properties imposed thereon. NetSketch is conceived to assist system integrators in two types of activities: modeling and design. It provides capabilities for compositional analysis based on a strongly-typed domain-specific language (DSL) for describing and reasoning about constrained-flow networks and invariants that need to be enforced thereupon. In a companion paper [13] we overview NetSketch, highlight its salient features, and illustrate how it could be used in actual applications. In this paper, we define using a machine-readable syntax major parts of the formal system underlying the operation of NetSketch, along with its semantics and a corresponding notion of validity. We then provide a proof of soundness for the formalism that can be partially verified using a lightweight formal reasoning system that simulates natural contexts. A traditional presentation of these definitions and arguments can be found in the full report on the NetSketch formalism [12].