This practice-based research articulates a performer's perspective from within the rapidly expanding field of mixed music, wherein traditional acoustic instruments are augmented by means of live electronics. Contemporary technology presents a panoply of sonic and interactive affordances and diverse avenues of potential for a contemporary practice of the clarinet. Pursuing a move from a technically passive approach towards self-efficient onstage operation, the author articulates a journey in which a hybridity of instrumental expertise and technical naivety develops into an embedded practice. A framework of humanising is proposed to establish codes of practice based on the embodied skill and priorities of the onstage performer. A pragmatic and personal approach emerges to managing issues of sound, control, and engagement, with an emphasis on viable rehearsal and performance practices that ultimately privilege an ongoing attention to liveness. The portfolio of sound recordings and the observances contained in this thesis contribute to a growing body of performer-led accounts in a rich environment for the development of new creative work and collaboration, and to facilitating access to interactive music for performers wishing to explore the field. A set of case studies trace three broad roles across a spectrum of creative agency within an interdisciplinary practice of the clarinet, situated at a nexus of diverse approaches - from performing composed works (executant interpreter) to non-idiomatic free improvisation (enactive composer), via hybrid works that blur these authorial distinctions (enabled interpreter). Negotiating multiple, interdependent influences within these respective performance ecologies, and moving over time from a status of technical novice towards one of proficiency and expertise (Dreyfus & Dreyfus 1980), a growing sense of embodied instrumentality is encountered (Nijs et al. 2009). The additional technology becomes less an extension of the instrument, rather the performer becomes present in a new holistic entity (Riva 2009; Rebelo 2006), with an attendant, ongoing re-evaluation of personal sound concept. Instrumental musicianship is reframed as inhabiting an assemblage of tools that filter and resonate physical energy, identity, and culture, and is directed towards an optimal performing presence.

Well-behaved SNC covers well-behaved and various classes of FC (free-choice) and is not included in AC (asymmetric choice). An SNC allows internal choices and concurrency and hence is powerful for irodeling. Any SNC is bounded and its liveness conditions are simple. An integrated algorithm, has been presented for verification of a net being SNC and its liveness with polynomial time complexity. Scholars often need to verify properties on nets appearing in literatures. Verification by CAD tool is less desirable than that by hand due to the extra efforts to input the model aid learn to use the tool. We propose to manually search the maximum SNC component followed by locating bad siphons in an incremental manner. We then apply Lautenback's Maridng Condition (MC) for liveness to berify the property of liveness. But there are two drawbacks associated with the above MC. First, it guarantees only deadlock-freeness, and not necessary liveness. We have identified the structure cause for this and developed its livess conditions correspondingly. Second a net may be live even if the MC is not satisfied. We have identified the structure cause for this. The MC has been readjusted based on our proposed new theorey.

<p>Biometrics deals with identifying individuals with help of their biological data. Fingerprint scanning is the most common method of the biometric methods available today. The security of fingerprint scanners has however been questioned and previous studies have shown that fingerprint scanners can be fooled with artificial fingerprints, i.e. copies of real fingerprints. The fingerprint recognition systems are evolving and this study will discuss the situation of today. </p><p>Two approaches have been used to find out how good fingerprint recognition systems are in distinguishing between live fingers and artificial clones. The first approach is a literature study, while the second consists of experiments. </p><p>A literature study of liveness detection in fingerprint recognition systems has been performed. A description of different liveness detection methods is presented and discussed. Methods requiring extra hardware use temperature, pulse, blood pressure, electric resistance, etc., and methods using already existent information in the system use skin deformation, pores, perspiration, etc. </p><p>The experiments focus on making artificial fingerprints in gelatin from a latent fingerprint. Nine different systems were tested at the CeBIT trade fair in Germany and all were deceived. Three other different systems were put up against more extensive tests with three different subjects. All systems werecircumvented with all subjects'artificial fingerprints, but with varying results. The results are analyzed and discussed, partly with help of the A/R value defined in this report.</p>

Biometrics deals with identifying individuals with help of their biological data. Fingerprint scanning is the most common method of the biometric methods available today. The security of fingerprint scanners has however been questioned and previous studies have shown that fingerprint scanners can be fooled with artificial fingerprints, i.e. copies of real fingerprints. The fingerprint recognition systems are evolving and this study will discuss the situation of today. Two approaches have been used to find out how good fingerprint recognition systems are in distinguishing between live fingers and artificial clones. The first approach is a literature study, while the second consists of experiments. A literature study of liveness detection in fingerprint recognition systems has been performed. A description of different liveness detection methods is presented and discussed. Methods requiring extra hardware use temperature, pulse, blood pressure, electric resistance, etc., and methods using already existent information in the system use skin deformation, pores, perspiration, etc. The experiments focus on making artificial fingerprints in gelatin from a latent fingerprint. Nine different systems were tested at the CeBIT trade fair in Germany and all were deceived. Three other different systems were put up against more extensive tests with three different subjects. All systems werecircumvented with all subjects'artificial fingerprints, but with varying results. The results are analyzed and discussed, partly with help of the A/R value defined in this report.

Cette thèse revisite les algorithmes standards pour les problèmes d'accessibilité et de vivacité des automates temporisés. L'algorithme standard pour tester l'accessibilité consiste à utiliser l'inclusion de zones pour explorer efficacement un arbre de recherche abstrait. Cependant, l'ordre du parcours du graphe a une forte incidence sur l'efficacité de l'algorithme. Dans cette thèse nous introduisons deux stratégies, nommées ranking et waiting, et une combinaison des deux. De nombreux exemples montrent que la combinaison des deux stratégies aide l'algorithme d'accessibilité à éviter des explorations non nécessaires. Le problème de vivacité est couramment vérifiées par l'analyse des cycles dans l'automate temporisé. Contrairement à l'algorithme d'accessibilité, l'algorithme pour l'analyse de vivacité ne peut pas librement utiliser l'inclusion de zones. Par conséquent, il y a des situations où l'algorithme doit faire une longue exploration avant de conclure l'existence d'un cycle. Nous proposons une analyse accélérée des cycles, nommées w-iterability checking, qui permet d'améliorer la performance de l'algorithme de vivacité des automates temporisés. En plus, nous proposons une modélisation du mécanisme de démarrage du protocole FlexRay. La modélisation permet à vérifier le mécanisme dans configurations différents du réseau FlexRay. Nous présentons également un outil de visualisation qui aide à mieux comprendre le fonctionnement des algorithmes d'analyse. / This thesis revisits the standard algorithms for reachability and liveness analysis of timed automata. The standard algorithm for reachability analysis consists in using zone inclusion to efficiently explore a finite abstract zone graph of a timed automaton. It has been observed that the search order may strongly affect the performance of the algorithm. For the same algorithm, one search order may introduce a lot more exploration than another. In order to deal with the search order problem, we propose two strategies, named ranking strategy and waiting strategy, and a combination of the two. We show on a number of examples, the combining strategy helps to reduce unnecessary exploration in the standard algorithms. The standard algorithm for liveness analysis consists in looking for reachability of cycles in timed automata. But unlike the algorithm for safety analysis, the algorithm for liveness analysis cannot freely use zone inclusion. Consequently, there are situations where the algorithm has to perform a long exploration before reporting the result. In this thesis, we propose an accelerated checking for cycles in timed automata, named !-iterability checking, to improve the performance of the state-of-the-art algorithm for liveness analysis of timed automata. Furthermore, we present a new model for the startup procedure of FlexRay. The model allows to verify the procedure on different configurations of FlexRay networks. It also allows to evaluate the performance of our new strategies for safety analysis of timed automata. In addition, we present a methodology that uses visualization tools to get more insights into the execution of the algorithms.

The thesis contributes to the theoretical study of Petri net theory. We conduct boundedness and liveness structural analysis of Synchronized Choice nets (SNC) based on fundamental structures in Petri nets and identified as first-order structures. By studying these structures, the study proposes two ways of preserving good properties: addition of second-order structures or other asymmetric structures. Liveness of these new SNC nets is studied based on the concept of siphons and traps. We prove that SNC nets thus formed are structurally bounded and live. The thesis extends this class of nets to those with pure TP and PT first-order structures and explores its structural and marking conditions. Based on this, we introduce a new class of Synchronized Choice nets called Expanded Synchronized Choice nets.

Att skapa attraktiva program är en av TV-producenternas huvuduppgifter. Mycket i detta arbete handlar om att etablera och behålla kontakt med TV-tittare genom tilltal, dvs. olika sätt att involvera TV-tittare i handlingen i programmen, i vilket studiopublikens skratt spelar en viktig roll. Deras skratt påverkar liveness som är TV-tittarnas känsla av spontanitet. I denna studie analyseras tilltal i situationer kring studiopublikens skratt i pratshower med kändisar som är orienterade mot humor och underhållning ("Hellenius hörna" och "Robins"). Interaktionen i dessa situationer studeras med hjälp av Conversation Analysis, Grices teori om samtalsprinciper samt Goffmans teorier om ramar och ansikte. Syftet med studien är att analysera det tilltal som skapar studiopublikens skratt och på detta sätt engagerar TV-tittarna, samt att upptäcka återkommande mönster i tilltalsstrukturer. Resultaten av studien visar att skratt skapas i samarbete mellan värden, gäster och studiopubliken, att olika slags avvikelser (rambrott) från bl.a. samtalsnormer, som skapar kontrast och skratt samt leder till frekventa orienteringskiften (ramskiften), är normen för denna sorts interaktion och tilltal. Småprat är den kategori som innehåller flest avvikelser, som därmed skapar mest skratt och bidrar mest till liveness. Olika typer av småprat, mönster i dem samt andra mönster identifierades.

This thesis outlines the structure and functionality of a selection of webseries, webshows, and eSports casting examples, in order to add to the discourse on online video. Webtelevision, or Web TV production, distribution, and financing systems will be detailed in the case studies made; and industry actors such as entrepreneurs, independents, corporations and conglomerates will be discussed and identified. Who are the producers, the advertisers, the distribution platforms, the sponsors, the rights holders, and how do they interact? In exploring the structure of some examples of Web TV, I wish to debunk the online-amateur association as an inaccurate or insufficient description which permeates much prior academic study on online video. Webshow content, business strategies, legal and copyright issues, as well as fan culture aspects will also be investigated; and in regards to eSports, the question of televised as opposed to streamcast tournaments will be examined.

Abstract Because of its natural and non-intrusive interaction, identity verification and recognition using facial information is among the most active areas in computer vision research. Unfortunately, it has been shown that conventional 2D face recognition techniques are vulnerable to spoofing attacks, where a person tries to masquerade as another one by falsifying biometric data and thereby gaining an illegitimate advantage. This thesis explores different directions for software-based face anti-spoofing. The proposed approaches are divided into two categories: first, low-level feature descriptors are applied for describing the static and dynamic characteristic differences between genuine faces and fake ones in general, and second, complementary attack-specific countermeasures are investigated in order to overcome the limitations of generic spoof detection schemes. The static face representation is based on a set of well-known feature descriptors, including local binary patterns, Gabor wavelet features and histogram of oriented gradients. The key idea is to capture the differences in quality, light reflection and shading by analysing the texture and gradient structure of the input face images. The approach is then extended to the spatiotemporal domain when both facial appearance and dynamics are exploited for spoof detection using local binary patterns from three orthogonal planes. It is reasonable to assume that no generic spoof detection scheme is able to detect all known, let alone unseen, attacks scenarios. In order to find out well-generalizing countermeasures, the problem of anti-spoofing is broken into two attack-specific sub-problems based on whether the spoofing medium can be detected in the provided view or not. The spoofing medium detection is performed by describing the discontinuities in the gradient structures around the detected face. If the display medium is concealed outside the view, a combination of face and background motion correlation measurement and texture analysis is applied. Furthermore, an open-source anti-spoofing fusion framework is introduced and its system-level performance is investigated more closely in order to gain insight on how to combine different anti-spoofing modules. The proposed spoof detection schemes are evaluated on the latest benchmark datasets. The main findings of the experiments are discussed in the thesis. / Tiivistelmä Kasvokuvaan perustuvan henkilöllisyyden tunnistamisen etuja ovat luonnollinen vuorovaikutus ja etätunnistus, minkä takia aihe on ollut erittäin aktiivinen tutkimusalue konenäön tutkimuksessa. Valitettavasti tavanomaiset kasvontunnistustekniikat ovat osoittautuneet haavoittuvaisiksi hyökkäyksille, joissa kameralle esitetään jäljennös kohdehenkilön kasvoista positiivisen tunnistuksen toivossa. Tässä väitöskirjassa tutkitaan erilaisia ohjelmistopohjaisia ratkaisuja keinotekoisten kasvojen ilmaisuun petkuttamisen estämiseksi. Työn ensimmäisessä osassa käytetään erilaisia matalan tason piirteitä kuvaamaan aitojen ja keinotekoisten kasvojen luontaisia staattisia ja dynaamisia eroavaisuuksia. Työn toisessa osassa esitetään toisiaan täydentäviä hyökkäystyyppikohtaisia vastakeinoja, jotta yleispätevien menetelmien puutteet voitaisiin ratkaista ongelmaa rajaamalla. Kasvojen staattisten ominaisuuksien esitys perustuu yleisesti tunnettuihin matalan tason piirteisiin, kuten paikallisiin binäärikuvioihin, Gabor-tekstuureihin ja suunnattujen gradienttien histogrammeihin. Pääajatuksena on kuvata aitojen ja keinotekoisten kasvojen laadun, heijastumisen ja varjostumisen eroavaisuuksia tekstuuria ja gradienttirakenteita analysoimalla. Lähestymistapaa laajennetaan myös tila-aika-avaruuteen, jolloin hyödynnetään samanaikaisesti sekä kasvojen ulkonäköä ja dynamiikkaa irroittamalla paikallisia binäärikuvioita tila-aika-avaruuden kolmelta ortogonaaliselta tasolta. Voidaan olettaa, ettei ole olemassa yksittäistä yleispätevää vastakeinoa, joka kykenee ilmaisemaan jokaisen tunnetun hyökkäystyypin, saati tuntemattoman. Näin ollen työssä keskitytään tarkemmin kahteen hyökkäystilanteeseen. Ensimmäisessä tapauksessa huijausapuvälineen reunoja ilmaistaan analysoimalla gradienttirakenteiden epäjatkuvuuksia havaittujen kasvojen ympäristössä. Jos apuvälineen reunat on piilotettu kameran näkymän ulkopuolelle, petkuttamisen ilmaisu toteutetaan yhdistämällä kasvojen ja taustan liikkeen korrelaation mittausta ja kasvojen tekstuurianalyysiä. Lisäksi työssä esitellään vastakeinojen yhdistämiseen avoimen lähdekoodin ohjelmisto, jonka avulla tutkitaan lähemmin menetelmien fuusion vaikutuksia. Tutkimuksessa esitetyt menetelmät on kokeellisesti vahvistettu alan viimeisimmillä julkisesti saatavilla olevilla tietokannoilla. Tässä väitöskirjassa käydään läpi kokeiden päähavainnot.

L’objectif général de cette thèse est le développement de méthodes mathématiques correctes et efficaces en pratique pour prouver automatiquement la correction de logiciels. Plus précisément, cette thèse est fondée sur la théorie de l’interprétation abstraite, un cadre mathématique puissant pour l’approximation du comportement des programmes. En particulier, cette thèse se concentre sur la preuve des propriétés de vivacité des programmes, qui représentent des conditions qui doivent être réalisés ultimement ou de manière répétée pendant l’exécution du programme. La terminaison des programmes est la propriété de vivacité la plus fréquemment considérée. Cette thèse conçoit des nouvelles approximations, afin de déduire automatiquement des conditions suffisantes pour la terminaison des programmes et synthétiser des fonctions de rang définies par morceaux, qui fournissent des bornes supérieures sur le temps d’attente avant la terminaison. Les approximations sont paramétriques dans le choix entre l’expressivité et le coût des approximations sous-jacentes, qui maintiennent des informations sur l’ensemble des valeurs possibles des variables du programme ainsi que les relations numériques possibles entre elles. Cette thèse développe également un cadre d’interprétation abstraite pour prouver des propriétés de vivacité, qui vient comme une généralisation du cadre proposé pour la terminaison. En particulier, le cadre est dédié à des propriétés de vivacité exprimées dans la logique temporelle, qui sont utilisées pour s’assurer qu’un événement souhaitable se produit une fois ou une infinité de fois au cours de l’exécution du programme. Comme pour la terminaison,des fonctions de rang définies par morceaux sont utilisées pour déduire des préconditions suffisantes pour ces propriétés, et fournir des bornes supérieures sur le temps d’attente avant un événement souhaitable. Les résultats présentés dans cette thèse ont été mis en œuvre dans un prototype d’analyseur. Les résultats expérimentaux montrent qu’il donne de bons résultats sur une grande variété de programmes, il est compétitif avec l’état de l’art, et il est capable d’analyser des programmes qui sont hors de la portée des méthodes existantes. / The overall aim of this thesis is the development of mathematically sound and practically efficient methods for automatically proving the correctness of computer software. More specifically, this thesis is grounded in the theory of abstract interpretation, a powerful mathematical framework for approximating the behavior of programs. In particular, this thesis focuses on provingprogram liveness properties, which represent requirements that must be eventually or repeatedly realized during program execution. Program termination is the most prominent liveness property. This thesis designs new program approximations, in order to automatically infer sufficient preconditions for program termination and synthesize so called piecewisedefined ranking functions, which provide upper bounds on the waiting time before termination. The approximations are parametric in the choice between the expressivity and the cost of the underlying approximations, which maintain information about the set of possible values of the program variables along with the possible numerical relationships between them. This thesis also contributes an abstract interpretation framework for proving liveness properties, which comes as a generalization of the framework proposedfor termination. In particular, the framework is dedicated to liveness properties expressed in temporal logic, which are used to ensure that some desirable event happens once or infinitely many times during program execution. As for program termination, piecewise-defined ranking functions are used to infer sufficient preconditions for these properties, and to provide upper boundson the waiting time before a desirable event. The results presented in this thesis have been implemented into a prototype analyzer. Experimental results show that it performs well on a wide variety of benchmarks, it is competitive with the state of the art, and is able to analyze programs that are out of the reach of existing methods.