Formal Verification of Temporal Properties for Parametrized Concurrent Programs and Concurrent Data Structures

Los tipos de datos concurrentes son implementaciones concurrentes de las abstracciones de datos clásicas, con la diferencia de que han sido específicamente diseñados para aprovechar el gran paralelismo disponible en las modernas arquitecturas multiprocesador y multinúcleo. La correcta manipulación de los tipos de datos concurrentes resulta esencial para demostrar la completa corrección de los sistemas de software que los utilizan. Una de las mayores dificultades a la hora de diseñar y verificar tipos de datos concurrentes surge de la necesidad de tener que razonar acerca de un número arbitrario de procesos que invocan estos tipos de datos de manera concurrente. Esto requiere considerar sistemas parametrizados. En este trabajo estudiamos la verificación formal de propiedades temporales de sistemas concurrentes parametrizados, poniendo especial énfasis en programas que manipulan estructuras de datos concurrentes. La principal dificultad a la hora de razonar acerca de sistemas concurrentes parametrizados proviene de la interacción entre el gran nivel de concurrencia que éstos poseen y la necesidad de razonar al mismo tiempo acerca de la memoria dinámica. La verificación de sistemas parametrizados resulta en sí un problema desafiante debido a que requiere razonar acerca de estructuras de datos complejas que son accedidas y modificadas por un numero ilimitado de procesos que manipulan de manera simultánea el contenido de la memoria dinámica empleando métodos de sincronización poco estructurados. En este trabajo, presentamos un marco formal basado en métodos deductivos capaz de ocuparse de la verificación de propiedades de safety y liveness de sistemas concurrentes parametrizados que manejan estructuras de datos complejas. Nuestro marco formal incluye reglas de prueba y técnicas especialmente adaptadas para sistemas parametrizados, las cuales trabajan en colaboración con procedimientos de decisión especialmente diseñados para analizar complejas estructuras de datos concurrentes. Un aspecto novedoso de nuestro marco formal es que efectúa una clara diferenciación entre el análisis del flujo de control del programa y el análisis de los datos que se manejan. El flujo de control del programa se analiza utilizando reglas de prueba y técnicas de verificación deductivas especialmente diseñadas para lidiar con sistemas parametrizados. Comenzando a partir de un programa concurrente y la especificación de una propiedad temporal, nuestras técnicas deductivas son capaces de generar un conjunto finito de condiciones de verificación cuya validez implican la satisfacción de dicha especificación temporal por parte de cualquier sistema, sin importar el número de procesos que formen parte del sistema. Las condiciones de verificación generadas se corresponden con los datos manipulados. Estudiamos el diseño de procedimientos de decisión especializados capaces de lidiar con estas condiciones de verificación de manera completamente automática. Investigamos teorías decidibles capaces de describir propiedades de tipos de datos complejos que manipulan punteros, tales como implementaciones imperativas de pilas, colas, listas y skiplists. Para cada una de estas teorías presentamos un procedimiento de decisión y una implementación práctica construida sobre SMT solvers. Estos procedimientos de decisión son finalmente utilizados para verificar de manera automática las condiciones de verificación generadas por nuestras técnicas de verificación parametrizada. Para concluir, demostramos como utilizando nuestro marco formal es posible probar no solo propiedades de safety sino además de liveness en algunas versiones de protocolos de exclusión mutua y programas que manipulan estructuras de datos concurrentes. El enfoque que presentamos en este trabajo resulta ser muy general y puede ser aplicado para verificar un amplio rango de tipos de datos concurrentes similares. Abstract Concurrent data types are concurrent implementations of classical data abstractions, specifically designed to exploit the great deal of parallelism available in modern multiprocessor and multi-core architectures. The correct manipulation of concurrent data types is essential for the overall correctness of the software system built using them. A major difficulty in designing and verifying concurrent data types arises by the need to reason about any number of threads invoking the data type simultaneously, which requires considering parametrized systems. In this work we study the formal verification of temporal properties of parametrized concurrent systems, with a special focus on programs that manipulate concurrent data structures. The main difficulty to reason about concurrent parametrized systems comes from the combination of their inherently high concurrency and the manipulation of dynamic memory. This parametrized verification problem is very challenging, because it requires to reason about complex concurrent data structures being accessed and modified by threads which simultaneously manipulate the heap using unstructured synchronization methods. In this work, we present a formal framework based on deductive methods which is capable of dealing with the verification of safety and liveness properties of concurrent parametrized systems that manipulate complex data structures. Our framework includes special proof rules and techniques adapted for parametrized systems which work in collaboration with specialized decision procedures for complex data structures. A novel aspect of our framework is that it cleanly differentiates the analysis of the program control flow from the analysis of the data being manipulated. The program control flow is analyzed using deductive proof rules and verification techniques specifically designed for coping with parametrized systems. Starting from a concurrent program and a temporal specification, our techniques generate a finite collection of verification conditions whose validity entails the satisfaction of the temporal specification by any client system, in spite of the number of threads. The verification conditions correspond to the data manipulation. We study the design of specialized decision procedures to deal with these verification conditions fully automatically. We investigate decidable theories capable of describing rich properties of complex pointer based data types such as stacks, queues, lists and skiplists. For each of these theories we present a decision procedure, and its practical implementation on top of existing SMT solvers. These decision procedures are ultimately used for automatically verifying the verification conditions generated by our specialized parametrized verification techniques. Finally, we show how using our framework it is possible to prove not only safety but also liveness properties of concurrent versions of some mutual exclusion protocols and programs that manipulate concurrent data structures. The approach we present in this work is very general, and can be applied to verify a wide range of similar concurrent data types.

Development and implementation of an air quality integrated assessment modelling system for the Iberian Peninsula

La mejora de la calidad del aire es una tarea eminentemente interdisciplinaria. Dada la gran variedad de ciencias y partes involucradas, dicha mejora requiere de herramientas de evaluación simples y completamente integradas. La modelización para la evaluación integrada (integrated assessment modeling) ha demostrado ser una solución adecuada para la descripción de los sistemas de contaminación atmosférica puesto que considera cada una de las etapas involucradas: emisiones, química y dispersión atmosférica, impactos ambientales asociados y potencial de disminución. Varios modelos de evaluación integrada ya están disponibles a escala continental, cubriendo cada una de las etapas antesmencionadas, siendo el modelo GAINS (Greenhouse Gas and Air Pollution Interactions and Synergies) el más reconocido y usado en el contexto europeo de toma de decisiones medioambientales. Sin embargo, el manejo de la calidad del aire a escala nacional/regional dentro del marco de la evaluación integrada es deseable. Esto sin embargo, no se lleva a cabo de manera satisfactoria con modelos a escala europea debido a la falta de resolución espacial o de detalle en los datos auxiliares, principalmente los inventarios de emisión y los patrones meteorológicos, entre otros. El objetivo de esta tesis es presentar los desarrollos en el diseño y aplicación de un modelo de evaluación integrada especialmente concebido para España y Portugal. El modelo AERIS (Atmospheric Evaluation and Research Integrated system for Spain) es capaz de cuantificar perfiles de concentración para varios contaminantes (NO2, SO2, PM10, PM2,5, NH3 y O3), el depósito atmosférico de especies de azufre y nitrógeno así como sus impactos en cultivos, vegetación, ecosistemas y salud como respuesta a cambios porcentuales en las emisiones de sectores relevantes. La versión actual de AERIS considera 20 sectores de emisión, ya sea equivalentes a sectores individuales SNAP o macrosectores, cuya contribución a los niveles de calidad del aire, depósito e impactos han sido modelados a través de matrices fuentereceptor (SRMs). Estas matrices son constantes de proporcionalidad que relacionan cambios en emisiones con diferentes indicadores de calidad del aire y han sido obtenidas a través de parametrizaciones estadísticas de un modelo de calidad del aire (AQM). Para el caso concreto de AERIS, su modelo de calidad del aire “de origen” consistió en el modelo WRF para la meteorología y en el modelo CMAQ para los procesos químico-atmosféricos. La cuantificación del depósito atmosférico, de los impactos en ecosistemas, cultivos, vegetación y salud humana se ha realizado siguiendo las metodologías estándar establecidas bajo los marcos internacionales de negociación, tales como CLRTAP. La estructura de programación está basada en MATLAB®, permitiendo gran compatibilidad con software típico de escritorio comoMicrosoft Excel® o ArcGIS®. En relación con los niveles de calidad del aire, AERIS es capaz de proveer datos de media anual y media mensual, así como el 19o valor horario más alto paraNO2, el 25o valor horario y el 4o valor diario más altos para SO2, el 36o valor diario más alto para PM10, el 26o valor octohorario más alto, SOMO35 y AOT40 para O3. En relación al depósito atmosférico, el depósito acumulado anual por unidad de area de especies de nitrógeno oxidado y reducido al igual que de azufre pueden ser determinados. Cuando los valores anteriormente mencionados se relacionan con características del dominio modelado tales como uso de suelo, cubiertas vegetales y forestales, censos poblacionales o estudios epidemiológicos, un gran número de impactos puede ser calculado. Centrándose en los impactos a ecosistemas y suelos, AERIS es capaz de estimar las superaciones de cargas críticas y las superaciones medias acumuladas para especies de nitrógeno y azufre. Los daños a bosques se calculan como una superación de los niveles críticos de NO2 y SO2 establecidos. Además, AERIS es capaz de cuantificar daños causados por O3 y SO2 en vid, maíz, patata, arroz, girasol, tabaco, tomate, sandía y trigo. Los impactos en salud humana han sido modelados como consecuencia de la exposición a PM2,5 y O3 y cuantificados como pérdidas en la esperanza de vida estadística e indicadores de mortalidad prematura. La exactitud del modelo de evaluación integrada ha sido contrastada estadísticamente con los resultados obtenidos por el modelo de calidad del aire convencional, exhibiendo en la mayoría de los casos un buen nivel de correspondencia. Debido a que la cuantificación de los impactos no es llevada a cabo directamente por el modelo de calidad del aire, un análisis de credibilidad ha sido realizado mediante la comparación de los resultados de AERIS con los de GAINS para un escenario de emisiones determinado. El análisis reveló un buen nivel de correspondencia en las medias y en las distribuciones probabilísticas de los conjuntos de datos. Las pruebas de verificación que fueron aplicadas a AERIS sugieren que los resultados son suficientemente consistentes para ser considerados como razonables y realistas. En conclusión, la principal motivación para la creación del modelo fue el producir una herramienta confiable y a la vez simple para el soporte de las partes involucradas en la toma de decisiones, de cara a analizar diferentes escenarios “y si” con un bajo coste computacional. La interacción con políticos y otros actores dictó encontrar un compromiso entre la complejidad del modeladomedioambiental con el carácter conciso de las políticas, siendo esto algo que AERIS refleja en sus estructuras conceptual y computacional. Finalmente, cabe decir que AERIS ha sido creado para su uso exclusivo dentro de un marco de evaluación y de ninguna manera debe ser considerado como un sustituto de los modelos de calidad del aire ordinarios. ABSTRACT Improving air quality is an eminently inter-disciplinary task. The wide variety of sciences and stakeholders that are involved call for having simple yet fully-integrated and reliable evaluation tools available. Integrated AssessmentModeling has proved to be a suitable solution for the description of air pollution systems due to the fact that it considers each of the involved stages: emissions, atmospheric chemistry, dispersion, environmental impacts and abatement potentials. Some integrated assessment models are available at European scale that cover each of the before mentioned stages, being the Greenhouse Gas and Air Pollution Interactions and Synergies (GAINS) model the most recognized and widely-used within a European policy-making context. However, addressing air quality at the national/regional scale under an integrated assessment framework is desirable. To do so, European-scale models do not provide enough spatial resolution or detail in their ancillary data sources, mainly emission inventories and local meteorology patterns as well as associated results. The objective of this dissertation is to present the developments in the design and application of an Integrated Assessment Model especially conceived for Spain and Portugal. The Atmospheric Evaluation and Research Integrated system for Spain (AERIS) is able to quantify concentration profiles for several pollutants (NO2, SO2, PM10, PM2.5, NH3 and O3), the atmospheric deposition of sulfur and nitrogen species and their related impacts on crops, vegetation, ecosystems and health as a response to percentual changes in the emissions of relevant sectors. The current version of AERIS considers 20 emission sectors, either corresponding to individual SNAP sectors or macrosectors, whose contribution to air quality levels, deposition and impacts have been modeled through the use of source-receptor matrices (SRMs). Thesematrices are proportionality constants that relate emission changes with different air quality indicators and have been derived through statistical parameterizations of an air qualitymodeling system (AQM). For the concrete case of AERIS, its parent AQM relied on the WRF model for meteorology and on the CMAQ model for atmospheric chemical processes. The quantification of atmospheric deposition, impacts on ecosystems, crops, vegetation and human health has been carried out following the standard methodologies established under international negotiation frameworks such as CLRTAP. The programming structure isMATLAB ® -based, allowing great compatibility with typical software such as Microsoft Excel ® or ArcGIS ® Regarding air quality levels, AERIS is able to provide mean annual andmean monthly concentration values, as well as the indicators established in Directive 2008/50/EC, namely the 19th highest hourly value for NO2, the 25th highest daily value and the 4th highest hourly value for SO2, the 36th highest daily value of PM10, the 26th highest maximum 8-hour daily value, SOMO35 and AOT40 for O3. Regarding atmospheric deposition, the annual accumulated deposition per unit of area of species of oxidized and reduced nitrogen as well as sulfur can be estimated. When relating the before mentioned values with specific characteristics of the modeling domain such as land use, forest and crops covers, population counts and epidemiological studies, a wide array of impacts can be calculated. When focusing on impacts on ecosystems and soils, AERIS is able to estimate critical load exceedances and accumulated average exceedances for nitrogen and sulfur species. Damage on forests is estimated as an exceedance of established critical levels of NO2 and SO2. Additionally, AERIS is able to quantify damage caused by O3 and SO2 on grapes, maize, potato, rice, sunflower, tobacco, tomato, watermelon and wheat. Impacts on human health aremodeled as a consequence of exposure to PM2.5 and O3 and quantified as losses in statistical life expectancy and premature mortality indicators. The accuracy of the IAM has been tested by statistically contrasting the obtained results with those yielded by the conventional AQM, exhibiting in most cases a good agreement level. Due to the fact that impacts cannot be directly produced by the AQM, a credibility analysis was carried out for the outputs of AERIS for a given emission scenario by comparing them through probability tests against the performance of GAINS for the same scenario. This analysis revealed a good correspondence in the mean behavior and the probabilistic distributions of the datasets. The verification tests that were applied to AERIS suggest that results are consistent enough to be credited as reasonable and realistic. In conclusion, the main reason thatmotivated the creation of this model was to produce a reliable yet simple screening tool that would provide decision and policy making support for different “what-if” scenarios at a low computing cost. The interaction with politicians and other stakeholders dictated that reconciling the complexity of modeling with the conciseness of policies should be reflected by AERIS in both, its conceptual and computational structures. It should be noted however, that AERIS has been created under a policy-driven framework and by no means should be considered as a substitute of the ordinary AQM.

Ol-Prx 3, a member of an additional class of homeobox genes, is unimodally expressed in several domains of the developing and adult central nervous system of the medaka (Oryzias latipes)

Large-scale genetic screens for mutations affecting early neurogenesis of vertebrates have recently been performed with an aquarium fish, the zebrafish. Later stages of neural morphogenesis have attracted less attention in small fish species, partly because of the lack of molecular markers of developing structures that may facilitate the detection of discrete structural alterations. In this context, we report the characterization of Ol-Prx 3 (Oryzias latipes-Prx 3). This gene was isolated in the course of a large-scale screen for brain cDNAs containing a highly conserved DNA binding region, the homeobox helix-three. Sequence analysis revealed that this gene belongs to another class of homeobox genes, together with a previously isolated mouse ortholog, called OG-12 [Rovescalli, A. C., Asoh, S. & Nirenberg, M. (1996) Proc. Natl. Acad. Sci. USA 93, 10691–10696] and with the human SHOX gene [Rao, E., Weiss, B., Fukami, M., Rump, A., Niesler, B., et al. (1997) Nat. Genet. 16, 54–62], thought to be involved in the short-stature phenotype of Turner syndrome patients. These three genes exhibit a moderate level of identity in the homeobox with the other genes of the paired-related (PRX) gene family. Ol-Prx 3, as well as the PRX genes, are expressed in various cartilaginous structures of head and limbs. These genes might thus be involved in common regulatory pathways during the morphogenesis of these structures. Moreover, this paper reports a complex and monophasic pattern of Ol-Prx 3 expression in the central nervous system, which differs markedly from the patterns reported for the PRX genes, Prx 3 excluded: this gene begins to be expressed in a variety of central nervous system territories at late neurula stage. Strikingly, it remains turned on in some of the derivatives of each territory during the entire life of the fish. We hope this work will thus help identify common features for the PRX 3 family of homeobox genes.

The insect endosymbiont Sodalis glossinidius utilizes a type III secretion system for cell invasion

Sodalis glossinidius is a maternally transmitted secondary endosymbiont residing intracellularly in tissues of the tsetse flies, Glossina spp. In this study, we have used Tn5 mutagenesis and a negative selection procedure to derive a S. glossinidius mutant that is incapable of invading insect cells in vitro and is aposymbiotic when microinjected into tsetse. This mutant strain harbors Tn5 integrated into a chromosomal gene sharing high sequence identity with a type III secretion system invasion gene (invC) previously identified in Salmonella enterica. With the use of degenerate PCR, we have amplified a further six Sodalis inv/spa genes sharing high sequence identity with type III secretion system genes encoded by Salmonella pathogenicity island 1. Phylogenetic reconstructions based on the inv/spa genes of Sodalis and other members of the family Enterobacteriaceae have consistently identified a well-supported clade containing Sodalis and the enteric pathogens Shigella and Salmonella. These results suggest that Sodalis may have evolved from an ancestor with a parasitic intracellular lifestyle, possibly a latter-day entomopathogen. These observations lend credence to a hypothesis suggesting that vertically transmitted mutualistic endosymbionts evolve from horizontally transmitted parasites through a parasitism–mutualism continuum.

Fibroblast growth factor (FGF) homologous factors: new members of the FGF family implicated in nervous system development.

Four new members of the fibroblast growth factor (FGF) family, referred to as fibroblast growth factor homologous factors (FHFs), have been identified by a combination of random cDNA sequencing, data base searches, and degenerate PCR. Pairwise comparisons between the four FHFs show between 58% and 71% amino acid sequence identity, but each FHF shows less than 30% identity when compared with other FGFs. Like FGF-1 (acidic FGF) and FGF-2 (basic FGF), the FHFs lack a classical signal sequence and contain clusters of basic residues that can act as nuclear localization signals. In transiently transfected 293 cells FHF-1 accumulates in the nucleus and is not secreted. Each FHF is expressed in the developing and adult nervous systems, suggesting a role for this branch of the FGF family in nervous system development and function.

Identification of a virulence locus encoding a second type III secretion system in Salmonella typhimurium.

Mapping the insertion points of 16 signature-tagged transposon mutants on the Salmonella typhimurium chromosome led to the identification of a 40-kb virulence gene cluster at minute 30.7. This locus is conserved among all other Salmonella species examined but is not present in a variety of other pathogenic bacteria or in Escherichia coli K-12. Nucleotide sequencing of a portion of this locus revealed 11 open reading frames whose predicted proteins encode components of a type III secretion system. To distinguish between this and the type III secretion system encoded by the inv/spa invasion locus known to reside on a pathogenicity island, we refer to the inv/spa locus as Salmonella pathogenicity island (SPI) 1 and the new locus as SPI2. SPI2 has a lower G+C content than that of the remainder of the Salmonella genome and is flanked by genes whose products share greater than 90% identity with those of the E. coli ydhE and pykF genes. Thus SPI2 was probably acquired horizontally by insertion into a region corresponding to that between the ydhE and pykF genes of E. coli. Virulence studies of SPI2 mutants have shown them to be attenuated by at least five orders of magnitude compared with the wild-type strain after oral or intraperitoneal inoculation of mice.

Toward the ultimate synthesis/recognition system.

This paper predicts speech synthesis, speech recognition, and speaker recognition technology for the year 2001, and it describes the most important research problems to be solved in order to arrive at these ultimate synthesis and recognition systems. The problems for speech synthesis include natural and intelligible voice production, prosody control based on meaning, capability of controlling synthesized voice quality and choosing individual speaking style, multilingual and multidialectal synthesis, choice of application-oriented speaking styles, capability of adding emotion, and synthesis from concepts. The problems for speech recognition include robust recognition against speech variations, adaptation/normalization to variations due to environmental conditions and speakers, automatic knowledge acquisition for acoustic and linguistic modeling, spontaneous speech recognition, naturalness and ease of human-machine interaction, and recognition of emotion. The problems for speaker recognition are similar to those for speech recognition. The research topics related to all these techniques include the use of articulatory and perceptual constraints and evaluation methods for measuring the quality of technology and systems.

Identity Entrepreneurs

In my previous article Racial Capitalism, I examined the ways in which white individuals and predominantly white institutions derive value from non-white racial identity. This process flows from our intense social and legal preoccupation with diversity. And it results in the commodification of non-white racial identity, with negative implications for both individuals and society. This Article picks up where Racial Capitalism left off in three ways. As a foundation, it first expands the concept of racial capitalism to identity categories more generally, explaining that individual in-group members and predominantly in-group institutions — usually individuals or institutions that are white, male, straight, wealthy, and so on — can and do derive value from out-group identities. Second, the Article turns from the overarching system of identity capitalism to the myriad ways that individual out-group members actively participate in that system. In particular, I examine how out-group members leverage their out-group status to derive social and economic value for themselves. I call such out-group participants identity entrepreneurs. Identity entrepreneurship is neither inherently good nor inherently bad. Rather, it is a complicated phenomenon with both positive and negative consequences. Finally, the Article considers the appropriate response to identity entrepreneurship. We should design laws and policies to maximize both individual agency and access to information for out-group members. Such reforms would protect individual choice while making clear the consequences of identity entrepreneurship both for individual identity entrepreneurs and for the out-group as a whole. A range of legal doctrines interact with and influence identity entrepreneurship, including employment discrimination under Title VII, rights of privacy and publicity, and intellectual property. Modifying these doctrines to take account of identity entrepreneurship will further progress toward an egalitarian society in which in-group and out-group identities are valued equally.

Redrawing Identity Boundaries through Integration Policies: Strategies of Inclusion/Exclusion of Immigrants in Québec and South Tyrol. EDAP Paper 01/2013

Following the research agenda introduced by Will Kymlicka, this qualitative study offers an interpretation of how the sub-national elites of Québec and South Tyrol police the integration of immigrants. For these national minority groups, which are constantly undergoing a process of redefinition of their collective identities by differentiating themselves from the Others who do not belong to the in-group, immigrants have progressively become the most significant Others as they are not part of the original system of compromises. This article questions how sub-national elites are handling this relatively new kind of ethnocultural diversity brought about by large-scale permanent immigration on two levels: first, the political narrative of the ruling sub-national parties, their electoral appeals, manifestos and speeches; second, the policy arrangements for the integration of immigrants in education, language and social policy. The initial approach of the article is pessimistic, as it assumes that sub-national elites will marginalize immigrants to please core nationalist supporters. In fact, the hypotheses to be tested are whether the national minority groups of Québec and South Tyrol engage in a process of reconstruction of their ethnic identity bounded by opposition to real or imagined Others – the newcomers; and whether they adopt practical measures that force newcomers to be assimilated into the group or to be marginalized. The comparison between Québec and South Tyrol provides a basic understanding of the impact of immigration in two sub-national polities that are very different, but still adopt similar political narratives and policy strategies with regard to the integration of newcomers.

Peer review of a formal verification/design proof methodology : summary of a sub-working-group meeting /

Bibliography: p. 48.

The Delsarte speaker, or Modern elocution designed especially for young folks and amateurs.

Mode of access: Internet.

The Universal standard speaker; a handbook of entertainment for all occassions; including rules for the training of the voice and the use of gesture.

Mode of access: Internet.

Criticizing groups from the inside and the outside: An identity perspective on the intergroup sensitivity effect

Research on group criticism has demonstrated that criticisms are received less defensively when made by an ingroup member than when made by an outsider (the intergroup sensitivity effect). Three experiments tested the extent to which this effect is driven by social identity concerns or by judgments of how experienced the source of the criticism is. In Experiments I and 2, Australians who criticized Australia (ingroup critics) were met with less defensiveness than were foreigners who criticized Australia (outgroup critics), regardless of the amount of experience the foreigner had with Australia. Furthermore, the effects of speaker type on evaluations were mediated by perceptions of the extent to which the criticisms were intended to be constructive but not by perceptions of experience. Finally, Experiment 3 indicated that although experience does not help outgroup critics, a lack of experience can hurt ingroup critics. Recommendations are provided as to how people can reduce defensiveness when making group criticisms.

Off-line signature verification and forgery detection using fuzzy modeling

Automatic signature verification is a well-established and an active area of research with numerous applications such as bank check verification, ATM access, etc. This paper proposes a novel approach to the problem of automatic off-line signature verification and forgery detection. The proposed approach is based on fuzzy modeling that employs the Takagi-Sugeno (TS) model. Signature verification and forgery detection are carried out using angle features extracted from box approach. Each feature corresponds to a fuzzy set. The features are fuzzified by an exponential membership function involved in the TS model, which is modified to include structural parameters. The structural parameters are devised to take account of possible variations due to handwriting styles and to reflect moods. The membership functions constitute weights in the TS model. The optimization of the output of the TS model with respect to the structural parameters yields the solution for the parameters. We have also derived two TS models by considering a rule for each input feature in the first formulation (Multiple rules) and by considering a single rule for all input features in the second formulation. In this work, we have found that TS model with multiple rules is better than TS model with single rule for detecting three types of forgeries; random, skilled and unskilled from a large database of sample signatures in addition to verifying genuine signatures. We have also devised three approaches, viz., an innovative approach and two intuitive approaches using the TS model with multiple rules for improved performance. (C) 2004 Pattern Recognition Society. Published by Elsevier Ltd. All rights reserved.