A Pattern Recognition Model of Voice-Based Personal Verification Systems for Forensic Applications

Abstract-The success of automatic speaker recognition in laboratory environments suggests applications in forensic science for establishing the Identity of individuals on the basis of features extracted from speech. A theoretical model for such a verification scheme for continuous normaliy distributed featureIss developed. The three cases of using a) single feature, b)multipliendependent measurements of a single feature, and c)multpleindependent features are explored.The number iofndependent features needed for areliable personal identification is computed based on the theoretcal model and an expklatory study of some speech featues.

A computational algorithm for the verification of tautologies in propositional calculus

A computational algorithm (based on Smullyan's analytic tableau method) that varifies whether a given well-formed formula in propositional calculus is a tautology or not has been implemented on a DEC system 10. The stepwise refinement approch of program development used for this implementation forms the subject matter of this paper. The top-down design has resulted in a modular and reliable program package. This computational algoritlhm compares favourably with the algorithm based on the well-known resolution principle used in theorem provers.

Identity for harmonic oscillator brackets

An identity satisfied by the harmonic oscillator (Talmi-Moshinsky) brackets is derived from two equivalent methods for evaluating an integral often encountered in cluster model studies.

Verification of the applicability of lattice model to concrete fracture by AE study

Notched three-point bend specimens (TPB) were tested under crack mouth opening displacement (CMOD) control at a rate of 0.0004 mm/s and the entire fracture process was simulated using a regular triangular two-dimensional lattice network only over the expected fracture proces zone width. The rest of the beam specimen was discretised by a coarse triangular finite element mesh. The discrete grain structure of the concrete was generated assuming the grains to be spherical. The load versus CMOD plots thus simulated agreed reasonably well with the experimental results. Moreover, acoustic emission (AE) hits were recorded during the test and compared with the number of fractured lattice elements. It was found that the cumulative AE hits correlated well with the cumulative fractured lattice elements at all load levels thus providing a useful means for predicting when the micro-cracks form during the fracturing process, both in the pre-peak and in the post-peak regimes.

Formal Verification of Full-Wave Rectifier: A Case Study

We present a case study of formal verification of full-wave rectifier for analog and mixed signal designs. We have used the Checkmate tool from CMU [1], which is a public domain formal verification tool for hybrid systems. Due to the restriction imposed by Checkmate it necessitates to make the changes in the Checkmate implementation to implement the complex and non-linear system. Full-wave rectifier has been implemented by using the Checkmate custom blocks and the Simulink blocks from MATLAB from Math works. After establishing the required changes in the Checkmate implementation we are able to efficiently verify, the safety properties of the full-wave rectifier.

A generalized mathematical theory and experimental verification of proportional notches

A theory and generalized synthesis procedure is advocated for the design of weir notches and orifice-notches having a base in any given shape, to a depth a, such that the discharge through it is proportional to any singular monotonically-increasing function of the depth of flow measured above a certain datum. The problem is reduced to finding an exact solution of a Volterra integral equation in Abel form. The maximization of the depth of the datum below the crest of the notch is investigated. Proof is given that for a weir notch made out of one continuous curve, and for a flow proportional to the mth power of the head, it is impossible to bring the datum lower than (2m − 1)a below the crest of the notch. A new concept of an orifice-notch, having discontinuity in the curve and a division of flow into two distinct portions, is presented. The division of flow is shown to have a beneficial effect in reducing the datum below (2m − 1)a from the crest of the weir and still maintaining the proportionality of the flow. Experimental proof with one such orifice-notch is found to have a constant coefficient of discharge of 0.625. The importance of this analysis in the design of grit chambers is emphasized.

Generalization of Dynkin's Identity and Some Applications

Let X(t) be a right continuous temporally homogeneous Markov pro- cess, Tt the corresponding semigroup and A the weak infinitesimal genera- tor. Let g(t) be absolutely continuous and r a stopping time satisfying E.( S f I g(t) I dt) < oo and E.( f " I g'(t) I dt) < oo Then for f e 9iJ(A) with f(X(t)) right continuous the identity Exg(r)f(X(z)) - g(O)f(x) = E( 5 " g'(s)f(X(s)) ds) + E.( 5 " g(s)Af(X(s)) ds) is a simple generalization of Dynkin's identity (g(t) 1). With further restrictions on f and r the following identity is obtained as a corollary: Ex(f(X(z))) = f(x) + k! Ex~rkAkf(X(z))) + n-1E + (n ) )!.E,(so un-1Anf(X(u)) du). These identities are applied to processes with stationary independent increments to obtain a number of new and known results relating the moments of stopping times to the moments of the stopped processes.

Wavelength/Time Multiple-Pulses-per-Row codes: Construction and verification

Two dimensional Optical Orthogonal Codes (OOCs) named Wavelength/Time Multiple-Pulses-per-Row (W/T MPR) codes suitable for use in incoherent fiber-optic code division multiple access (FO-CDMA) networks are reported in [6]. In this paper, we report the construction of W/T MPR codes, using Greedy Algorithm (GA), with distinct 1-D OOCs [1] as the row vectors. We present the W/T MPR codes obtained using the GA. Further, we verify the correlation properties of the generated W/T MPR codes using Matlab.

Experimental Verification of the Lateral Periodicity of Axially Periodic Incoherent Fields Using the Lau Effect

General' objects, which are specially prepared to possess restricted spatial frequency spectra, have been used in the conventional Lau experiment to obtain experimental proof for the existence of lateral periodicity arising from axial periodicity, for a subclass of axially periodic wavefields in an incoherent situation.

A matrix identity and perturbation expressions

An identity expressing formally the diagonal and off-diagonal elements of an inverse of a matrix is deduced employing operator techniques. Several well-known perturbation expressions for the self-energy are deduced as special cases. A new approximation and other applications following from the above formalism are briefly indicated through illustrations from a perturbed harmonic oscillator, chemisorption approximations and Kelly's result in the problem of electron correlation.

Both Surface Proteins (VP4 and VP7) of an Asymptomatic Neonatal Rotavirus Strain (1321) Have High Levels of Sequence Identity with the Homologous Proteins of a Serotype 10 Bovine Rotavirus

The nucleotide sequence of genes 4 and 9, encoding the outer capsid proteins VP4 and VP7 of a serotype 10 tissue culture-adapted strain, 1321, representative of asymptomatic neonatal rotaviruses isolated from neonates in Bangalore, India, were determined. Comparison of nucleotide and deduced amino acid sequences of 1321 VP4 and VP7 with previously published sequences of various serotypes revealed that both genes were highly homologous to the respective genes of serotype 10 bovine rotavirus, B223. The VP4 of 1321 represents a new human P serotype and the 1321 and related strains represent the first description of neonatal rotaviruses that appear to derive both surface proteins from an animal rotavirus.

Automatic verification of distributed logic specifications

Formal specification is vital to the development of distributed real-time systems as these systems are inherently complex and safety-critical. It is widely acknowledged that formal specification and automatic analysis of specifications can significantly increase system reliability. Although a number of specification techniques for real-time systems have been reported in the literature, most of these formalisms do not adequately address to the constraints that the aspects of 'distribution' and 'real-time' impose on specifications. Further, an automatic verification tool is necessary to reduce human errors in the reasoning process. In this regard, this paper is an attempt towards the development of a novel executable specification language for distributed real-time systems. First, we give a precise characterization of the syntax and semantics of DL. Subsequently, we discuss the problems of model checking, automatic verification of satisfiability of DL specifications, and testing conformance of event traces with DL specifications. Effective solutions to these problems are presented as extensions to the classical first-order tableau algorithm. The use of the proposed framework is illustrated by specifying a sample problem.

Off-line signature verification using genetically optimized weighted features

This paper is concerned with off-line signature verification. Four different types of pattern representation schemes have been implemented, viz., geometric features, moment-based representations, envelope characteristics and tree-structured Wavelet features. The individual feature components in a representation are weighed by their pattern characterization capability using Genetic Algorithms. The conclusions of the four subsystems teach depending on a representation scheme) are combined to form a final decision on the validity of signature. Threshold-based classifiers (including the traditional confidence-interval classifier), neighbourhood classifiers and their combinations were studied. Benefits of using forged signatures for training purposes have been assessed. Experimental results show that combination of the Feature-based classifiers increases verification accuracy. (C) 1999 Pattern Recognition Society. Published by Elsevier Science Ltd. All rights reserved.