355 resultados para Correctness
Resumo:
Les surfaces de subdivision fournissent une méthode alternative prometteuse dans la modélisation géométrique, et ont des avantages sur la représentation classique de trimmed-NURBS, en particulier dans la modélisation de surfaces lisses par morceaux. Dans ce mémoire, nous considérons le problème des opérations géométriques sur les surfaces de subdivision, avec l'exigence stricte de forme topologique correcte. Puisque ce problème peut être mal conditionné, nous proposons une approche pour la gestion de l'incertitude qui existe dans le calcul géométrique. Nous exigeons l'exactitude des informations topologiques lorsque l'on considère la nature de robustesse du problème des opérations géométriques sur les modèles de solides, et il devient clair que le problème peut être mal conditionné en présence de l'incertitude qui est omniprésente dans les données. Nous proposons donc une approche interactive de gestion de l'incertitude des opérations géométriques, dans le cadre d'un calcul basé sur la norme IEEE arithmétique et la modélisation en surfaces de subdivision. Un algorithme pour le problème planar-cut est alors présenté qui a comme but de satisfaire à l'exigence topologique mentionnée ci-dessus.
Resumo:
Il y a des problemes qui semblent impossible a resoudre sans l'utilisation d'un tiers parti honnete. Comment est-ce que deux millionnaires peuvent savoir qui est le plus riche sans dire a l'autre la valeur de ses biens ? Que peut-on faire pour prevenir les collisions de satellites quand les trajectoires sont secretes ? Comment est-ce que les chercheurs peuvent apprendre les liens entre des medicaments et des maladies sans compromettre les droits prives du patient ? Comment est-ce qu'une organisation peut ecmpecher le gouvernement d'abuser de l'information dont il dispose en sachant que l'organisation doit n'avoir aucun acces a cette information ? Le Calcul multiparti, une branche de la cryptographie, etudie comment creer des protocoles pour realiser de telles taches sans l'utilisation d'un tiers parti honnete. Les protocoles doivent etre prives, corrects, efficaces et robustes. Un protocole est prive si un adversaire n'apprend rien de plus que ce que lui donnerait un tiers parti honnete. Un protocole est correct si un joueur honnete recoit ce que lui donnerait un tiers parti honnete. Un protocole devrait bien sur etre efficace. Etre robuste correspond au fait qu'un protocole marche meme si un petit ensemble des joueurs triche. On demontre que sous l'hypothese d'un canal de diusion simultane on peut echanger la robustesse pour la validite et le fait d'etre prive contre certains ensembles d'adversaires. Le calcul multiparti a quatre outils de base : le transfert inconscient, la mise en gage, le partage de secret et le brouillage de circuit. Les protocoles du calcul multiparti peuvent etre construits avec uniquements ces outils. On peut aussi construire les protocoles a partir d'hypoth eses calculatoires. Les protocoles construits a partir de ces outils sont souples et peuvent resister aux changements technologiques et a des ameliorations algorithmiques. Nous nous demandons si l'efficacite necessite des hypotheses de calcul. Nous demontrons que ce n'est pas le cas en construisant des protocoles efficaces a partir de ces outils de base. Cette these est constitue de quatre articles rediges en collaboration avec d'autres chercheurs. Ceci constitue la partie mature de ma recherche et sont mes contributions principales au cours de cette periode de temps. Dans le premier ouvrage presente dans cette these, nous etudions la capacite de mise en gage des canaux bruites. Nous demontrons tout d'abord une limite inferieure stricte qui implique que contrairement au transfert inconscient, il n'existe aucun protocole de taux constant pour les mises en gage de bit. Nous demontrons ensuite que, en limitant la facon dont les engagements peuvent etre ouverts, nous pouvons faire mieux et meme un taux constant dans certains cas. Ceci est fait en exploitant la notion de cover-free families . Dans le second article, nous demontrons que pour certains problemes, il existe un echange entre robustesse, la validite et le prive. Il s'effectue en utilisant le partage de secret veriable, une preuve a divulgation nulle, le concept de fantomes et une technique que nous appelons les balles et les bacs. Dans notre troisieme contribution, nous demontrons qu'un grand nombre de protocoles dans la litterature basee sur des hypotheses de calcul peuvent etre instancies a partir d'une primitive appelee Transfert Inconscient Veriable, via le concept de Transfert Inconscient Generalise. Le protocole utilise le partage de secret comme outils de base. Dans la derniere publication, nous counstruisons un protocole efficace avec un nombre constant de rondes pour le calcul a deux parties. L'efficacite du protocole derive du fait qu'on remplace le coeur d'un protocole standard par une primitive qui fonctionne plus ou moins bien mais qui est tres peu couteux. On protege le protocole contre les defauts en utilisant le concept de privacy amplication .
Resumo:
En synthèse d'images réalistes, l'intensité finale d'un pixel est calculée en estimant une intégrale de rendu multi-dimensionnelle. Une large portion de la recherche menée dans ce domaine cherche à trouver de nouvelles techniques afin de réduire le coût de calcul du rendu tout en préservant la fidelité et l'exactitude des images résultantes. En tentant de réduire les coûts de calcul afin d'approcher le rendu en temps réel, certains effets réalistes complexes sont souvent laissés de côté ou remplacés par des astuces ingénieuses mais mathématiquement incorrectes. Afin d'accélerer le rendu, plusieurs avenues de travail ont soit adressé directement le calcul de pixels individuels en améliorant les routines d'intégration numérique sous-jacentes; ou ont cherché à amortir le coût par région d'image en utilisant des méthodes adaptatives basées sur des modèles prédictifs du transport de la lumière. L'objectif de ce mémoire, et de l'article résultant, est de se baser sur une méthode de ce dernier type[Durand2005], et de faire progresser la recherche dans le domaine du rendu réaliste adaptatif rapide utilisant une analyse du transport de la lumière basée sur la théorie de Fourier afin de guider et prioriser le lancer de rayons. Nous proposons une approche d'échantillonnage et de reconstruction adaptative pour le rendu de scènes animées illuminées par cartes d'environnement, permettant la reconstruction d'effets tels que les ombres et les réflexions de tous les niveaux fréquentiels, tout en préservant la cohérence temporelle.
Resumo:
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.
Resumo:
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
Resumo:
Unit Commitment Problem (UCP) in power system refers to the problem of determining the on/ off status of generating units that minimize the operating cost during a given time horizon. Since various system and generation constraints are to be satisfied while finding the optimum schedule, UCP turns to be a constrained optimization problem in power system scheduling. Numerical solutions developed are limited for small systems and heuristic methodologies find difficulty in handling stochastic cost functions associated with practical systems. This paper models Unit Commitment as a multi stage decision making task and an efficient Reinforcement Learning solution is formulated considering minimum up time /down time constraints. The correctness and efficiency of the developed solutions are verified for standard test systems
Resumo:
Unit commitment is an optimization task in electric power generation control sector. It involves scheduling the ON/OFF status of the generating units to meet the load demand with minimum generation cost satisfying the different constraints existing in the system. Numerical solutions developed are limited for small systems and heuristic methodologies find difficulty in handling stochastic cost functions associated with practical systems. This paper models Unit Commitment as a multi stage decision task and Reinforcement Learning solution is formulated through one efficient exploration strategy: Pursuit method. The correctness and efficiency of the developed solutions are verified for standard test systems
Resumo:
This paper describes certain findings of intonation and intensity study of emotive speech with the minimal use of signal processing algorithms. This study was based on six basic emotions and the neutral, elicited from 1660 English utterances obtained from the speech recordings of six Indian women. The correctness of the emotional content was verified through perceptual listening tests. Marked similarity was noted among pitch contours of like-worded, positive valence emotions, though no such similarity was observed among the four negative valence emotional expressions. The intensity patterns were also studied. The results of the study were validated using arbitrary television recordings for four emotions. The findings are useful to technical researchers, social psychologists and to the common man interested in the dynamics of vocal expression of emotions
Resumo:
Analysis by reduction is a linguistically motivated method for checking correctness of a sentence. It can be modelled by restarting automata. In this paper we propose a method for learning restarting automata which are strictly locally testable (SLT-R-automata). The method is based on the concept of identification in the limit from positive examples only. Also we characterize the class of languages accepted by SLT-R-automata with respect to the Chomsky hierarchy.
Resumo:
Analysis by reduction is a method used in linguistics for checking the correctness of sentences of natural languages. This method is modelled by restarting automata. All types of restarting automata considered in the literature up to now accept at least the deterministic context-free languages. Here we introduce and study a new type of restarting automaton, the so-called t-RL-automaton, which is an RL-automaton that is rather restricted in that it has a window of size one only, and that it works under a minimal acceptance condition. On the other hand, it is allowed to perform up to t rewrite (that is, delete) steps per cycle. Here we study the gap-complexity of these automata. The membership problem for a language that is accepted by a t-RL-automaton with a bounded number of gaps can be solved in polynomial time. On the other hand, t-RL-automata with an unbounded number of gaps accept NP-complete languages.
Resumo:
Aufgrund der breiten aktuellen Verwendung des Mythen-Begriffs in Kunst und Werbung, aber darüber hinaus auch in nahezu allen Bereichen gesellschaftlichen Lebens und vor allem in der Philosophie ergibt sich die Notwendigkeit, einen erweiterten Mythos-Begriff über das Historisch-Authentische hinaus zu verfolgen. Ausgehend von einer strukturalen Annäherung an den Mythos-Begriff im Sinne des von Roland Barthes vorgeschlagenen sekundären semiologischen Systems, d.h. einer semiologischen Sinnverschiebung zur Schaffung einer neuen – mythischen – Bedeutung, fordert diese neue Bedeutung eine Analyse, eine Mythenanalyse heraus. Dies ist deshalb so entscheidend, weil eben diese neue Bedeutung ihr mythisches Profil im Sinne von Hans Blumenberg durch forcierte Bedeutsamkeit für Individuen oder für bestimmte gesellschaftliche Gruppierungen unterlegt, z.B. durch bewusst intensive Wiederholung eines Themas oder durch unerwartete Koinzidenzen von Ereignissen oder durch Steigerung bzw. Depotenzierung von Fakten. Der erweiterte Mythen-Begriff verlangt nach einer Strukturierung und führt dabei zu unterschiedlichen Mythen-Ansätzen: zum Ursprungsstoff des authentischen Mythos und darauf basierender Geisteslage, zum Erkennen eines reflektierten Mythos, wenn es um das Verhältnis Mythos/Aufklärung geht, zum Zeitgeist-Mythos mit seinen umfangreichen Ausprägungen ideologischer, affirmativer und kritischer Art oder zu Alltagsmythen, die sich auf Persönlichkeitskulte und Sachverherrlichungen beziehen. Gerade der letztere Typus ist das Terrain der Werbung, die über den Gebrauchswert eines Produktes hinaus Wert steigernde Tauschwerte durch symbolische Zusatzattribute erarbeiten möchte. Hierbei können Markenmythen unterschiedlichster Prägung entstehen, denen wir täglich im Fernsehen oder im Supermarkt begegnen. Die Manifestation des Mythos in der Kunst ist einerseits eine unendliche Transformationsgeschichte mythischer Substanzen und andererseits ein überhöhender Bezug auf Zeitgeisterscheinungen, etwa bei dem Mythos des Künstlers selbst oder der durch ihn vorgenommenen „Verklärung des Gewöhnlichen“. Die Transformationsprozesse können u.a . prototypisch an zwei Beispielketten erläutert werden, die für den Kunst/Werbung-Komplex besonders interessant sind, weil ihr Charakter sich in einem Fall für die Werbung als äußerst Erfolg versprechend erwiesen hat und weil sich im zweiten Fall geradezu das Gegenteil abzeichnet: Zum einen ist es die Mythengestalt der Nymphe, jene jugendliche, erotisch-verführerische Frauengestalt, die über ihre antiken Wurzeln als Sinnbild der Lebensfreude und Fruchtbarkeit hinaus in und nach der Renaissance ihre Eignung als Verbildlichung der Wiederzulassung des Weiblichen in der Kunst beweist und schließlich der Instrumen-talisierung der Werbung dient. Im anderen Fall ist es die Geschichte der Medusa, die man idealtypisch als die andere Seite der Nympha bezeichnen kann. Hier hat Kunst Auf-klärungsarbeit geleistet, vor allem durch die Verschiebung des medusischen Schreckens von ihr weg zu einer allgemein-medusischen Realität, deren neue Träger nicht nur den Schrecken, sondern zugleich ihre Beteiligung an der Schaffung dieses Schreckens auf sich nehmen. Mythosanalyse ist erforderlich, um die Stellungnahmen der Künstler über alle Epochen hinweg und dabei vor allem diese Transformationsprozesse zu erkennen und im Sinne von Ent- oder Remythologisierung einzuordnen. Die hierarchische Zuordnung der dabei erkannten Bedeutungen kann zu einem Grundbestandteil einer praktischen Philosophie werden, wenn sie einen Diskurs durchläuft, der sich an Jürgen Habermas’ Aspekt der Richtigkeit für kommunikatives Handeln unter dem Gesichtspunkt der Toleranz orientiert. Dabei ist nicht nur zu beachten, dass eine verstärkte Mythenbildung in der Kunst zu einem erweiterten Mythen-begriff und damit zu dem erweiterten, heute dominierenden Kunstbegriff postmoderner Prägung geführt hat, sondern dass innerhalb des aktuellen Mythenpakets sich die Darstellungen von Zeitgeist- und Alltagsmythen zu Lasten des authentischen und des reflektierten Mythos entwickelt haben, wobei zusätzlich werbliche Markenmythen ihre Entstehung auf Verfahrensvorbildern der Kunst basieren. Die ökonomische Rationalität der aktuellen Gesellschaft hat die Mythenbildung keines-wegs abgebaut, sie hat sie im Gegenteil gefördert. Der neuerliche Mythenbedarf wurde stimuliert durch die Sinnentleerung der zweckrationalisierten Welt, die Ersatzbedarf anmeldete. Ihre Ordnungsprinzipien durchdringen nicht nur ihre Paradedisziplin, die Ökonomie, sondern Politik und Staat, Wissenschaft und Kunst. Das Umschlagen der Aufklärung wird nur zu vermeiden sein, wenn wir uns Schritt für Schritt durch Mythenanalyse unserer Unmündigkeit entledigen.
Resumo:
Analysis by reduction is a method used in linguistics for checking the correctness of sentences of natural languages. This method is modelled by restarting automata. Here we study a new type of restarting automaton, the so-called t-sRL-automaton, which is an RL-automaton that is rather restricted in that it has a window of size 1 only, and that it works under a minimal acceptance condition. On the other hand, it is allowed to perform up to t rewrite (that is, delete) steps per cycle. We focus on the descriptional complexity of these automata, establishing two complexity measures that are both based on the description of t-sRL-automata in terms of so-called meta-instructions. We present some hierarchy results as well as a non-recursive trade-off between deterministic 2-sRL-automata and finite-state acceptors.
Resumo:
Diabetes mellitus is a disease where the glucosis-content of the blood does not automatically decrease to a ”normal” value between 70 mg/dl and 120 mg/dl (3,89 mmol/l and 6,67 mmol/l) between perhaps one hour (or two hours) after eating. Several instruments can be used to arrive at a relative low increase of the glucosis-content. Besides drugs (oral antidiabetica, insulin) the blood-sugar content can mainly be influenced by (i) eating, i.e., consumption of the right amount of food at the right time (ii) physical training (walking, cycling, swimming). In a recent paper the author has performed a regression analysis on the influence of eating during the night. The result was that one ”bread-unit” (12g carbon-hydrats) increases the blood-sugar by about 50 mg/dl, while one hour after eating the blood-sugar decreases by about 10 mg/dl per hour. By applying this result-assuming its correctness - it is easy to eat the right amount during the night and to arrive at a fastening blood-sugar (glucosis-content) in the morning of about 100 mg/dl (5,56 mmol/l). In this paper we try to incorporate some physical exercise into the model.
Resumo:
Distributed systems are one of the most vital components of the economy. The most prominent example is probably the internet, a constituent element of our knowledge society. During the recent years, the number of novel network types has steadily increased. Amongst others, sensor networks, distributed systems composed of tiny computational devices with scarce resources, have emerged. The further development and heterogeneous connection of such systems imposes new requirements on the software development process. Mobile and wireless networks, for instance, have to organize themselves autonomously and must be able to react to changes in the environment and to failing nodes alike. Researching new approaches for the design of distributed algorithms may lead to methods with which these requirements can be met efficiently. In this thesis, one such method is developed, tested, and discussed in respect of its practical utility. Our new design approach for distributed algorithms is based on Genetic Programming, a member of the family of evolutionary algorithms. Evolutionary algorithms are metaheuristic optimization methods which copy principles from natural evolution. They use a population of solution candidates which they try to refine step by step in order to attain optimal values for predefined objective functions. The synthesis of an algorithm with our approach starts with an analysis step in which the wanted global behavior of the distributed system is specified. From this specification, objective functions are derived which steer a Genetic Programming process where the solution candidates are distributed programs. The objective functions rate how close these programs approximate the goal behavior in multiple randomized network simulations. The evolutionary process step by step selects the most promising solution candidates and modifies and combines them with mutation and crossover operators. This way, a description of the global behavior of a distributed system is translated automatically to programs which, if executed locally on the nodes of the system, exhibit this behavior. In our work, we test six different ways for representing distributed programs, comprising adaptations and extensions of well-known Genetic Programming methods (SGP, eSGP, and LGP), one bio-inspired approach (Fraglets), and two new program representations called Rule-based Genetic Programming (RBGP, eRBGP) designed by us. We breed programs in these representations for three well-known example problems in distributed systems: election algorithms, the distributed mutual exclusion at a critical section, and the distributed computation of the greatest common divisor of a set of numbers. Synthesizing distributed programs the evolutionary way does not necessarily lead to the envisaged results. In a detailed analysis, we discuss the problematic features which make this form of Genetic Programming particularly hard. The two Rule-based Genetic Programming approaches have been developed especially in order to mitigate these difficulties. In our experiments, at least one of them (eRBGP) turned out to be a very efficient approach and in most cases, was superior to the other representations.
Resumo:
I have designed and implemented a system for the multilevel verification of synchronous MOS VLSI circuits. The system, called Silica Pithecus, accepts the schematic of an MOS circuit and a specification of the circuit's intended digital behavior. Silica Pithecus determines if the circuit meets its specification. If the circuit fails to meet its specification Silica Pithecus returns to the designer the reason for the failure. Unlike earlier verifiers which modelled primitives (e.g., transistors) as unidirectional digital devices, Silica Pithecus models primitives more realistically. Transistors are modelled as bidirectional devices of varying resistances, and nodes are modelled as capacitors. Silica Pithecus operates hierarchically, interactively, and incrementally. Major contributions of this research include a formal understanding of the relationship between different behavioral descriptions (e.g., signal, boolean, and arithmetic descriptions) of the same device, and a formalization of the relationship between the structure, behavior, and context of device. Given these formal structures my methods find sufficient conditions on the inputs of circuits which guarantee the correct operation of the circuit in the desired descriptive domain. These methods are algorithmic and complete. They also handle complex phenomena such as races and charge sharing. Informal notions such as races and hazards are shown to be derivable from the correctness conditions used by my methods.