C A R Hoare

Paul Sabatier

Arturo Tlacaélel

Curiel Díaz

Using formal logic to represent Sign Language phonetics in semi-automatic annotation tasks

There are two ways of constructing a software design: one way is to make it so simple that there are obviously no deficiencies, and the other way is to make it so complicated that there are no obvious deficiencies. The first method is far more difficult."

Pour ces raisons, le travail présenté dans ce document a comme objectif la construction d'une représentation abstraite de la LS ; plus précisément, le but est de pouvoir représenter des collections de vidéo LS (corpus) de manière formelle. En générale, il s'agit de construire une couche de représentation intermédiaire, permettant de faire de la reconnaissance automatique indépendamment des technologies de suivi et des corpus utilisés pour la recherche. Cette couche corresponde à un système de transition d'états (STE), spécialement crée pour représenter la nature parallèle des LS. En plus, elle peut-être annoté avec de formules logiques pour son analyse, à travers de la vérification de modèles.

Finalement, la création de cet outil à permit l'implémentation d'un système d'annotation semiautomatique, basé sur les principes théoriques du formalisme. Globalement, le système reçoit des vidéos LS et les transforme dans un STE valide. Ensuite, un module fait de la vérification formelle sur le STE, en utilisant une base de données de formules crée par un expert en LS. Les formules représentent des propriétés lexicales à chercher dans le STE. Le produit de ce processus, est une annotation qui peut être corrigé par des utilisateurs humains, et qui est utilisable dans des domaines d'études tels que la linguistique.

contributed to the making of this dissertation.

First of all, I want to thank Conacyt (Mexico) for financing my postgraduate studies.

I'm aware that I've acquired a moral debt with the mexican people and, for the entirety of my professional career, I'll try my best to repay it.

Next, I would like to thank M. Christophe COLLET, my advisor, to whom I'm truly grateful both for his support, and for putting up with my antagonistic character and my perpetually outlandish approaches. I know I was a very difficult research trainee. I was recklessly stubborn; sometimes I pushed carelessly towards very heavy stuff, without having the slightless notion of where I was, or even where I wanted to go. If this document has any structure, at all, it is because you managed to keep me from aimlessly wandering into the desert of worthless ideas that can be my mind. Thank you.

I'd also like to thank my committee, professors Annelies BRAFFORT, Onno CRASBORN and Nicholas ASHER. I appreciate your observations, your patience and, most of all, your questions, which unexpectedly gave me a better understanding of my own work.

Special thanks to Prof. BRAFFORT, who took the time to painstakingly review each of my dissertation drafts, considerably lifting the quality of the final document.

My sincere thanks to Dr. Sergio RAJSBAUM, who gave me the time I needed to work on my manuscript's corrections, when I should have been working on novel solutions to distributed computing problems. I greatly appreciate your encouragement and concern these last few months, which ended up being crucial for bringing this endeavor to a happy conclusion. Unlike Mario VARGAS LLOSA, the 2010 Nobel Prize in literature, I've had more than fourteen minutes to reflect upon the significance of my own, rather minor, distinction. Now that my reflection time has passed, I can see clearly how important it was for me to have it. Thanks for your consideration.

Thanks to one of the most brilliant and passionate girls I know, my dear sister Jade CURIEL, who took time out of her schedule to read and propose changes to my linguistics chapter. I really appreciated your input. Not only were you the first person to read a portion of my thesis, but your observations heavily influenced how I presented all of the linguistic content. In addition, I ended up citing almost every reference you sent my way.

Thanks for all that.

On a more personal note, I want to thank Mme. Chantal MORAND, who received me at the airport my first day in France and helped me on every step of my journey, right until v the very last minute. Merci, je n'aurais pas pu y arriver sans toute votre aide! Cette thèse vous appartient autant qu'à moi, vraiment.

I also want to thank Mme. Catherine STASIULIS, whom I met during one of my multiple clashes with bureaucracy. J'ai vraiment apprécié ton soutien, qui est arrivé pendant une période très sombre de ma vie où j'existais par inertie, isolé dans un pays étranger, sans savoir qu'est-ce que j'étais en train de faire. T'es la seule à se rendre compte que j'étais au bord du gouffre. Merci, je n'aurais pas pu m'en sortir tout seul.

Thanks to Rémi DUBOT, my research brother, my guide to french culture and, above all, a true friend. Sans doute un des meilleurs. J'ai toujours admiré ta capacité, ton élan et la force de tes principes. Quand je trouvais la thèse insupportable, tu étais toujours là pour alléger la charge; sans nos discussions, je l'aurais laissé tomber il y a longtemps.

Merci. J'espère que l'on se croisera dans le futur.

My deepest gratitude to my good friend Claudio GUTIERREZ, with whom I've laughed non-stop from the moment we met. De tí aprendí a llevar las cosas más a la ligera. Me alegro que hayamos sorteado juntos el choque cultural que significaron todos estos años, el drama y la angustia de ser expatriados, de llegar a un sistema académico del cual no teníamos un claro marco de referencia. Gracias por todo el apoyo, por interesarte en mi tema de investigación y por las palabras de aliento.

I humbly thank Monia BEN MLOUKA for keeping my interest in the area alive, by providing me with French Sign Language (LSF) lessons. J'ai vraiment aimé ces séances qui m'ont gonflé l'esprit, qui m'ont donné des nouvelles idées et, surtout, qui m'ont permis de mieux te connaitre. Merci.

I can't stop mentioning Matilde GONZALEZ, the reason I came to France in the first place. Gracias por haberme integrado, por introducirme a vicios que no sabía que tenía y por los invaluables consejos que me diste sobre el funcionamiento de Christophe.

Thanks to Alain CROUZIL for stopping by to talk from time to time, even if I ended up leaving the office after dark. Surtout, merci de m'avoir aidé à surveiller les locaux la nuit.

I want to thank Anaïs MEALLIER, the first non-academic to whom I had to describe my work as a "researcher". Si cela te semblait trop ridicule c'est normal : globalement, je ne fais que de choses ridicules. Dans tout cas, j'apprécie que tu continues à t'intéresser pour ma vie, même trois ans après d'être partie. Merci.

All my gratitude to Teodora SZASZ and her wonderful mind. J'apprécie énormément que tu aies dédié autant du temps à entendre mes folies. J'en dis tellement que, maintenant, j'ai peur pour ta santé. Sinon, l'on s'est bien amusés. Moi trop, je pense. Dans tout cas, mult ¸umesc.

Contents vii

Thanks to Bérengère MATHIEU, who helped me forget the grief of leaving my old life behind by being a supportive and honest friend. Discuter avec toi est un énorme plaisir.

Notre jeu sera un succès sans précédant. Merci.

I also want to thank Camille NADAL, who arrived to brighten my days after weeks of solitude, while I was in the middle of writing. Quand tu es arrivée, je commençais à péter un câble. En plus de la solitude, j'en avais tellement marre de la rédaction que mon cerveau n'arrivait plus à s'organiser. Tu m'as aidé à regagner le contrôle. Grâce à ça, j'ai pu finir le premier brouillon. Merci.

Thanks to Edna HERNANDEZ, one of the few who had to endure my worst behavior during writing, well beyond what I thought she was capable of. La neta me aguantaste más de lo que yo hubiera esperado, especialmente sabiendo que tú tambien estabas en medio de la redacción. Aunque bueno, considerando que nos conocimos en una borrachera, debería ya saber que tienes aguante. Gracias por el apoyo incondicional. No me es indiferente.

Thanks to Alexander DIAZ, Victor FUENTES and Eduardo PACHECO, who kept in touch regardless of the slight disadvantage of living on the other side of the world; an impressive feat, considering my loathing for social networks. Gracias por el apoyo, por soportar las interminables letanías que suelo escribir y por continuar incluyendome en sus vidas.

Once more, thanks to my sister Jade. Gracias por chismosearme cosas al teléfonosobre todo los asuntos jugosos -y por hacer de IT en la casa durante mi ausencia. La verdad es que luego si me alegrabas los días.

Thanks to my parents, Arturo CURIEL and Graciela DIAZ, for giving me their unconditional support all these years, and for teaching me that hard work is more important than intelligence. A ustedes mi más grande reconocimiento. No me quedan palabras para describir lo mucho que aprecio su confianza, su apoyo. No merezco padres como ustedes. Gracias.

Thanks to the monsters from my nightmares, who keep me from standing still. I'm sure they'll eventually catch me . . . until then, it is oddly reassuring to know they are there, trying.

Last but not least, thanks to Sombra the cat for taking my place at home during these long years. Now that my family loves her more than they love me, I have gained the Holds H A and H B are characterized by postures A and B, respectively. The movement between holds is a transition from postures A to B. . . . 2.6 Information contained in each time-unit for the H-M-H sign ROAD LSF . . . 2.7 The transition movement M BC , between H B and H C , is a co-articulation. 2.8 The transition movement M CD , before part of a sign, is now a co-articulation. 2.9 Spatialization of FRIEND LSF to the right of the signer. . . . . . . . . . . . 2.10 Hand agrees with space location to produce "Call a friend". . . . . . . . 2.11 TREE LSF is an example of an iconic sign. . . . . . . . . . . . . . . . . . . 2.12 PAUSE LSF uses iconicity in a metaphoric way, by representing a pause as a physical "break". . . . ), while holding a POINTING configuration. 12 3.7 SignWriting contact symbols to represent "touch", "grasp", "strike", "brush", "rub" and "enter". . . . . . . . . . . . . . . . . . . . . . . . . . . 3.8 SignWriting places of articulation and their possible modificators. 13 . . . 3.9 SignWriting hand configurations. 14

List of Figures

Introduction

Sign Languages (SLs) are the visual-gestural languages of Deaf people. Broadly speaking, signers achieve communication through the simultaneous use of their hands and several other Non-Manual Features (NMFs), which work together to convey a message. Distinct information can be transmitted by modifying both very notorious and subtle parameters [Stokoe 1960, p. 16]; as such, changes on hand positions, shapes or movements are just as important as less salient elements like head tilting, eye gaze or body orientation [Bahan 1996, Engberg-Pedersen 2003].

This phenomenon where several body parts work simultaneously to achieve communication is called multimodality. Essentially, each modality corresponds to an individual communication channel, which carries the information produced by a single body part while signing. The signer parts involved on the articulation of SL utterances (hands, head, elbows, mouth, etc.) are called articulators. Signers receive information by observing how every articulator interacts with the others. This simultaneous nature of SL is further enriched with complex linguistic phenomena like role shifting, where signers change their point of view to "act the part" of another character during signing [Lillo-Martin 1995]. It is by way of these complex interactions that signers are capable of generating discourse with the same expressive power than vocal languages.

The use of space plays a crucial role in SL. It is through spatial relations that signers are able to expressing complex nuances on their reasoning [START_REF] Emmorey | [END_REF]]. Accordingly, space has been observed to fulfill diverse linguistic roles, notably by providing mappings between discrete spatial regions and discourse referents [Padden 2010a]. So, for instance, a signer will commonly map a specific spatial location (e.g. by pointing) to a person, a place or an object, and will continue referring to the same entity by unambiguously acknowledging the assigned location. This phenomenon is commonly known as spatialization.

SLs arise naturally within Deaf communities [Senghas 2004], and provide the same expressive power as do vocal speech [START_REF] Sandler | [END_REF]]. Subsequently, they serve as standalone communication systems, and exist independently from vocal languages. However, more often than not they are influenced in their structure by socio-cultural aspects related to the surrounding hearing culture [Battison 1978[START_REF] Kwong | [END_REF]].

There is no universal SL, just as there is no universal vocal language; SLs vary from country to country and from region to region. Even geographically close communities can develop independent SLs, with differing degrees of mutual intelligibility [Padden 2010b].

In addition, internal variations can be observed between signers of different generations [Woodward 1976], social classes [START_REF] Parks | [END_REF]], genders [Sutton-Spence 1999b, p. 23] and ethnic origins [Solomon 2010].

It is also important to note that SLs lack of writing systems. The aforementioned simultaneity of SL parameters and their reliance on space, complicates the creation of a faithful written representation. Proposals like SignWriting [Sutton 2000], have tried to provide a written form to SLs with some success. Still, several usability considerations have undermined their utility outside of some very specific use cases, notably in research [Antinoro Pizzuto 2010, p. 211].

A more thorough introduction to SL characteristics is presented in Chapter 2 (p. 21).

The rest of this chapter presents a brief description of SL research, specially its relationship with computer science. Furthermore, the text portrays -very succinctlythe problematic at hand, and ponders about how existing tools from different domains could be used to address complex problems in the field. Lastly, the final section lists the contributions of this work, and intuitively spells out the core details of the proposed solutions.

Sign Language Research

The interest in the study of SL linguistics, has contributed towards the development of new research lines in several areas. A significant part of SL studies, are focused on deaf education [Marschark 2001] and SL acquisition [Baker 2009b]. Moreover, researchers have been able to interpret results in these fields through the lenses of neurobiology and psychology, by observing short and long term effects of SL proficiency on the human brain [START_REF] Emmorey | [END_REF]].

From the point of view of education, the main interest in the area has been to assess and improve the quality of Deaf instruction. Research goes from the creation of revised pedagogic strategies in schools [START_REF][END_REF]], to their effects on Deaf children development [Calderon 2000]. These efforts mainly strive to increase literacy rates among the Deaf, as well as to improve their integration with the surrounding hearing culture [START_REF] Mayer | [END_REF][START_REF] Antia | [END_REF].

Research in Deaf education has led to new studies on SL acquisition and its outcomes both on hearing and Deaf individuals. Work in the field has been able to document brain changes across different signing populations [Neville 1997[START_REF] Nishimura | [END_REF]], which has in turn contributed to a better understanding of the human brain. In this regard, research has shown that SL learning has positive effects on the long term linguistic development of signers [Daniels 1996[START_REF] Goodwyn | [END_REF]] and on their overall neurological evolution [START_REF] Emmorey | [END_REF]]. This diversity of new SL studies, has called for further research on SLs themselves, especially on how their linguistic characteristics differ from those of vocal languages.

For this reason, new lines have emerged on how to generate and compare meaningful linguistic data [Baker 2009a], which has led in particular to the creation of SL corpora.

Corpus-linguistics and Sign Language

In corpus-linguistics, a corpus (plural corpora) is a collection of naturally occurring language samples, intended to be representative of the language [START_REF] Biber | [END_REF]]. In order to be considered representative, corpora need not only be "large enough", but samples must be selected following specific criteria depending on the purpose of its creation [Bowker 2002, p. 10]. For instance, to study use of space in SL, the collection could be based on empirical observations of spatialization occurrences. Finally, it is crucial for corpora to be representable as a digital resource, as corpus-linguistics relies on the use of computers for language analysis [Biber 1998, p. 4].

Corpora are commonly annotated with linguistic information [Baker 2006, p. 6], which allows researchers to derive conclusions from data. Annotations can go from the purely symbolic, to even carry meta-data about the speakers. In that sense, they can be as simple as labeling words with their syntactic function (i.e. verb, noun, etc), or as complex as noting the socio-political role of the corpus participants [Warren 2004].

Aside from annotation, corpora analysis benefits from another technique called transcription. Broadly speaking, a transcript intends to represent information from one medium into another [Jenks 2011, pp. 2-6]. Contrary to annotation, transcripts try to give rigorous depictions of the original information, by applying a series of symbolic conventions [Lapadat 1999, p. 68]. For example, phonetic transcription can be done by using the International Phonetic Alphabet, so as to precisely convey the sounds produced by vocal utterances. Finally, it is important to emphasize that transcription seeks to create a literal representation of the source material and not to translate it, just as IPA does with vocal language sounds.

Corpus-linguistics has become a valuable resource in linguistic studies, since it readily uses new technology to discover otherwise difficult to find patterns. Current vocal corpora are usually comprehensive enough to describe a wide array of linguistic phenomena over vast amounts of information [Partington 1998, pp. 2-4]; difficulties arise, nonetheless, when working with SLs corpora.

Sign Language Corpora

Similarly to vocal languages, a SL corpus is a digital compilation of language samples documenting its use. However, because of their lack of a written representation, SL corpora are bound to be kept as video collections, whereas their vocal counterparts can usually be kept as textual records. This constraint alone is enough to complicate their creation, since it imposes the development of specialized tools for their storage, capture and analysis, among others [Johnston 2006, pp. 10-12]. These conditions hinder the growth and availability of corpora, both because of technical and financial limitations.

Commonly, different capture technologies are adopted with each new SL corpus, which has resulted on a very heterogeneous environment. Existing corpora have been created with professional video cameras [START_REF] Hanke | [END_REF]], 3D sensors [Stefanov 2013], motion capture technology [Lu 2010] and even by collecting televised SL broadcasts [START_REF] Forster | [END_REF]].

Moreover, each media carries its own distribution formats, which can lead to further segmentation issues between different resources. Finally, the access to financial sources such as research grants, can also have an impact on variability; for example, projects like the Dicta-sign corpus [START_REF] Matthes | [END_REF]], built by several research teams across Europe, was able to produce 25 hours of high definition annotated data, which required spending on technology which was not readily available for less-financed corpora.

Differences in capture, distribution and storage formats, complicate the task of amassing big SL data repositories like the ones existing for vocal languages. For reference, the British National Corpus, an English language corpus, holds more than 100 million words [START_REF] Leech | Geoffrey Leech. 100 million words of English: the British National Corpus (BNC)[END_REF]]. Likewise, the Leipzig Corpora Collection, which documents more than 20 vocal languages, holds about 30 thousand sentences on its worst documented language and as many as 30 million on the best documented [START_REF] Biemann | [END_REF]]. However, with SLs, even large corpora pale in comparison with the sizes of written language collections. A big SL corpus like the DGS Corpus Project has about 2.25 million signs [Nishio 2010], while the majority of the documented corpora hold only a few hundreds of sentences [Morrissey 2005[START_REF] Bungerot | [END_REF]].

Transcription and Annotation of Sign Language Corpora

Transcription and annotation of SL corpora are highly specialized, time-consuming, endeavors [START_REF] Neidle | [END_REF][START_REF] Forster | [END_REF]. Each new corpus invariably leads to the production of machine-readable transcripts and annotations (see Subsection 1.1.1 p. 3). They are mainly used for scientific research, thus they usually can't be created by signers with no linguistics training whatsoever [Chen Pichler 2010, p. 4]. Even with simple notations tasks, SL experts are needed to prove that the produced documents are exploitable [START_REF] Börstell | [END_REF]]. For this reason, it is acknowledged in the literature that there is a lack of experts capable of fulfilling the notation needs of the domain [Johnston 2006, p. 12]. Incidentally, notations are prone to human-error [Fanghella 2012, p. 59], as they tend to be very detailed; hence, it is a common practice to double check notes in order to avoid inconsistencies, which increases the quantity of work needed for the task.

Regardless of their significance, there is no clear consensus on which coding systems should be used for transcripts and annotations [START_REF] Pizzuto | [END_REF], Miller 2001[START_REF] Van Der | [END_REF].

Furthermore, no standard notation guidelines exist [START_REF] Schembri | [END_REF], Johnston 2011]. This situation results in variations between different notation teams, even over the same corpus [Müller de Quadros 2014, p. 97].

Transcripts of SL corpora are created by way of symbolic representation systems [Hoiting 2003], akin to those mentioned on page 2. Consequently, corpus transcription faces the same kind of problems as the development of all-purpose SL writing systems; namely, the difficulty to accurately convey every aspect of visual communication by way of a written document. Furthermore, transcripts tend to be very complex, considering the high quantity of parameters that must be represented [Johnston 2010, p. 19]. As a result, their creation is usually reserved for the study of very specific linguistic phenomena [Morgan 2003], making annotation the preferred method to represent SL information in corpora.

Most of the existing corpus annotations are glosses [START_REF] Pizzuto | [END_REF]]. Essentially, glossing consists in adding a one or two word description, a gloss note, to a visually recognized element in the corpus. Frequently, these notes are merely words from a vocal language; however, in some cases, simple coding systems are created to better represent the elements of interest [van der Hulst 2010, pp. 29-35]. The process ensures the creation of small, machine-readable notes, which are easier to create than transcripts, and can be used alongside corpus multimedia as needed [Johnston 2010, p. 24].

Glosses are usually created with a specific purpose, and can be of different types. Hence, a single corpus can spawn several kinds of glosses, being the most common the ones produced by the observation of lexical signs (e.g. dictionary signs), non-lexical signs

Computer Science and Sign Language

The relationship between SL and Computer Science (CS) is wide, going from the development of tools for theoretical linguistics to practical applications directed towards Deaf integration. In particular, major efforts exist on the areas of SL synthesis and recognition, both of which are involved on various projects of other areas. Also, research along these lines tend to overlap with linguistics on their need for corpora, which can prove troublesome due to the low availability of big SL data repositories (see Subsection 1.1.1.1, p. 4).

Sign Language Synthesis

Synthesis centers around the creation of artificial SL utterances, performed by animated human avatars [START_REF] Bangham | [END_REF][START_REF] Filhol | [END_REF][START_REF] Michael Kipp | Sign Language Avatars: Animation and Comprehensibility[END_REF]. The main objective is to communicate relevant information to Deaf users, in situations where no SL translation exists. Figure 1.2 shows the example of a signing avatar. Research has shown that humans respond naturally to movement of biological origin [Vercher 2006, pp. 6-8]. In this regard, a more organic synthesis can effectively enhance the comprehensibility of artificial utterances [Rezzoug 2006, p. 1]. For this reason, the creation of copora for synthesis is a common occurrence, since the development of more realistic animations relies on these to learn from human signers to accurately render signing motion [Lu 2010, Lefebvre-Albaret 2013].

Synthesis deals also with SL representation issues. The movements of the avatars are usually controlled by way of technical notation languages like the Signing Gesture Markup Language (SiGML) [Elliott 2004]. Formalisms like these produce very detailed utterance descriptions, which serve as mechanical instructions for the avatar to follow.

The produced descriptions are closely related to SL transcription and its multiple issues (see Subsection 1.1.1.2, p. 5). Indeed SiGML, for example, is based upon the Hamburg Notation System (HamNoSys) notation [Bangham 2000, pp. 4-5], only adapted to avoid describing features that cannot be animated by the target system. Figure 3.13 (see p.

53)

shows the example of a sign description created in SiGML.

Other representation languages used in synthesis have gone beyond the purely geometrical into higher level descriptions. For instance, the classifier-predicates models by [Huenerfauth 2006], enables the representation of "invisible objects" around a signer. In the same vein, the Zebedee representation formalism developed by [Filhol 2009] holds similar capabilities, permitting the representation of SLs at higher levels rather than by giving thorough geometric configurations.

As with corpus annotation, the representation languages used for SL synthesis tend to be very heterogeneous due to the variety of the available resources. Additionally, each description formalism must adapt to the limits imposed by its avatar's synthesis engine, which may encompass different constraints in terms of: space, expressivity of the depicted articulators, and even synctactic rules. For example, variations on how the signing space is modeled during generation, may lead to differing representation capabilities [Braffort 2008]. Consider the case of entities located in space: the places where an entity is positioned, the possible internal relationships and any semantic modifications they may suffer, have to be expresible by the selected description formalism, which adapts to the underlying representation of space by the engine.

For this reason, existing technical notations are designed around different principles: detailed spatial representation [START_REF] Marshall | [END_REF]]; accurate description of NMF [START_REF] Niewiadomski | [END_REF]; synchronization between body movements [Filhol 2012a] or for the compositional use of very low level movement descriptions [START_REF][END_REF]].

In some cases, these representations go beyond being purely mechanical. Some efforts have been made to develop higher level representations, capable of describing grammatical constructions rather than just geometrical animation recipes [Losson 1998[START_REF] Marshall | [END_REF]].

However, work in the area is limited by a lack of consensus on how to interpret some SL linguistic phenomena [START_REF] Sigal | [END_REF][START_REF] Meier | Modality and Structure in Signed and Spoken Languages[END_REF], which ultimately shows how intertwined SL linguistics can be with areas like computer science.

Finally, a couple of all-purpose synthesis engines are readily available for commercial use [START_REF][END_REF]], as well as several research projects focused on exploring different use cases of this technology. Among these, notable examples are the signing of recurrent information like the weather [Verlinden 2002], the creation of educational materials [START_REF] Karpouzis | [END_REF]], on-the-fly translation of text to SL [START_REF] Xu | [END_REF][START_REF] Boulares | [END_REF], the distribution of internet content [START_REF] Kennaway | [END_REF]] and solutions enabling translation from written language to SL [Zhao 2000].

Sign Language Recognition

Research in SL recognition is focused on the development of technology related to the automatic translation of SL into speech, written or else, and the automatic identification of SL linguistic characteristics [START_REF] Cooper | [END_REF]]. It involves the creation of tools for the capture, representation and automatic analysis of SL utterances [START_REF] Ong | [END_REF]].

Most of the existing work on the area is based on the use of SL corpora [Cooper 2011, p. 4]. Recognition research takes advantage of machine learning algorithms to find significant patterns on SL data. Essentially, corpora are used as a source of training and test sets for machine learning tasks; that is, corpus samples are selected to both teach an algorithm what to classify, and to evaluate how effective the classification is [Wu 1999[START_REF] Ong | [END_REF]].

The idea is that, once the algorithms are developed and tested, their use can be extended to other corpora or to create practical applications.

Recognition covers a wide range of tasks going from the identification of complete sentences [START_REF] Starner | [END_REF]] to the detection of phonetic properties, those measurable by electronic means. However, both technical and theoretical issues on the field have impeded the development of SL recognition technology [START_REF] Morrissey | [END_REF]]; Natural Language Processing (NLP) techniques often rely on sizable amounts of data to work with [START_REF] Banko | [END_REF], Brill 2003[START_REF] Halevy | [END_REF]], which is difficult to obtain with SLs. Moreover, the problem is accentuated by the lack of a written representation (see Section 1, p. 2). Consequently, the reliance on corpora arises a series of technical problems related to their format, low availability, lack of annotation and overall heterogeneity (see Subsection 1.1.1.1, p. 4).

Even at the most basic level, SLs recognition is not straightforward. Ample knowledge on the studied language and a solid linguistic theory are often needed to train recognition algorithms [Cuxac 2007a, pp. 12-14]. However, the lack of consensus regarding some SL linguistic characteristics [START_REF] Sigal | [END_REF][START_REF] Meier | Modality and Structure in Signed and Spoken Languages[END_REF] and the low availability of experts are common occurrences in field (see Subsection 1.1.1.2, p. 5). For instance, lets take the example of multimodality (see Section 1, p. 1). The interactions between the signer's body parts involved in communication are combinatorial in nature. As such, a single change in one of them can modify the meaning of the information given by the others [Brugman 2002, p. 177]. In addition, some of the combinations may be completely devoid of meaning as is the case with co-articulations, the arbitrary movement combinations signers execute when passing from one sign to another [Segouat 2009]. How and when body movements synchronize to create meaning is a subject of discussion in SL linguistics; however, adopting a synchronization model is fundamental even to recognize individual signs [Brugman 2002, Filhol 2012a].

The different physical characteristic of the modalities are also an issue for corpus-based recognition. Each modality usually requires individualized classification techniques to take in account the physical constraints of the signer's body. A notorious example of this are the differences between NMFs and manual features; the hands are usually very prominent and have ample degrees of articulation [START_REF] Rehg | [END_REF]], whereas NMFs tend to be more difficult to follow and have to be treated with different techniques [Liu 2014, p. 673].

As a consequence, the quality of the information that can be automatically extracted from corpora will necessarily be constrained by their technical characteristics, since the technology used on their capture can favor the detection of certain features while inhibiting others [Wu 1999, pp. 4-5]. These problems impair the portability of recognition algorithms, as they imply that it won't always be possible to ensure similar recognition rates across corpora of different origins.

With this in mind, several tools have been developed with the purpose of enabling feature recognition on both recent and older corpora, regardless of any existing technical limitations [Dreuw 2008b]. For example, some projects have tried to do some analysis by calculating position information of hands and head on existing 2D corpora [START_REF] Gonzalez | [END_REF]].

Others have used 3D tracking algorithms to analyze signing more reliably, by exploiting spatial information [START_REF] Nickel | Pointing Gesture Recognition Based on 3D-tracking of Face, Hands and Head Orientation[END_REF]]. Motion caption approaches have also been developed, where the combined use of wearable sensors and cameras enable recognition of complex features alongside tracking [Mehdi 2002].

Regardless of the underlying technology, most research projects on SL recognition fall into two main categories: isolated and continuous. Isolated recognition attempts to single out sign appearances on corpora; that is, the system is trained with a specific set of signs, and it automatically analyzes where in the corpus these signs appear [Grobel 1997]. In contrast, continuous recognition tries to identify signs on a sequence; each signing video is analyzed and segmented into possible signs, then the system attempts to determine what sign corresponds to each segment [START_REF] Liang | [END_REF]]. It is mainly continuous recognition which has to deal with complex phenomena like co-articulations, as here the system has to take in account synchronization issues to achieve segmentation [START_REF] Gonzalez | [END_REF]].

In either case, the use of solid computational and linguistic models is necessary to achieve good recognition rates, specially since the number of possible combinations that could potentially convey meaning is intractable without prior language knowledge [Vogler 2001, p. 358-359].

Most of the existing work on SL recognition has centered on the identification of lexical signs [Ong 2005, p. 874], both in continuous or isolated sign recognition. Unfortunately, there exist serious size limitations in the majority of cases [Wang 2002, p. 1]. Additionally, the low scalability of corpora complicates the creation of rich sign-based recognition models [Bauer 2002a, p. 436], which indirectly forces the training vocabularies to be small. This has lead to increased interest on raising the sizes of these vocabularies, which has gained traction over the years [Ong 2005, pp. 886-887], although with somewhat limited success.

This situation has pushed research towards sub-lexical feature recognition, launching exploratory studies on SLs morphological characteristics of signs such as motion and posture analysis [START_REF] Lefebvre-Albaret | [END_REF]; sign segmentation [START_REF] Gonzalez | [END_REF]]; the study of coarticulations [Fang 2007, Segouat 2009]; hand configuration classification [Hamada 2004];

facial-movement analysis [Vogler 2007] and on the synchronization between manual and non-manual features [START_REF] Ma | [END_REF][START_REF] Vogler | [END_REF]]. Sub-lexical research has also benefited from the introduction of new, cheaper, capture technology [Zafrulla 2011, p. 280], which has increased the quantity of exploitable information on new recognition corpora.

Finally, research above the lexical level has mainly focused on the detection of complete sentences [START_REF] Starner | [END_REF][START_REF] Zahedi | [END_REF]], sign alignment between different SLs [START_REF] Chiu | [END_REF] and recognition of some spatiotemporal features [Kelly 2009]. However, little-to-no work has been directed towards SL discourse translation. This is because translation relies on both lexical recognition and on correctly interpreting the complex physical interactions of articulators (see Section 1, p. 1), non-trivial tasks themselves [Cuxac 2007a]. Nonetheless, some discourse analysis models have been developed [START_REF] Braffort | [END_REF], Dalle 2006] in an effort to at least determine which is the minimum level of automatic analysis needed, to develop a discourse translator.

The Problem of Semi-Automatic Annotation

Annotation plays an important role in computer-aided SL research; it is by way of annotation that automatic systems can discriminate relevant information from corpora, to be used in research [Dreuw 2008a, p. 1]. By reading annotations, systems become capable of removing noisy video-frames automatically, effectively creating ground truths for machine learning algorithms [START_REF] Moehrmann | [END_REF]]. However, the annotation process is very time consuming and requires the participation of human experts, since only them are capable of judging which features are relevant enough to be annotated. Nevertheless, regardless of expert availability the task may appear endless, since new linguistic hypotheses may diminish (or increase) the perceived importance of notable features, thus leading to new annotation demands [Brugman 2002]. This implicitly points towards a constant annotation cycle, were experts elaborate over previous iterations. Moreover, due to the multimodal nature of SLs, needing different types of gloss is a common occurrence (see Subsection 1.1.1.2, p. 5), increasing even more the dimensions of the task.

Different research projects entail different annotation needs. In SL synthesis, for instance, glosses can be used to manually indicate where the relevant movements to be learned are [START_REF] Arikan | [END_REF][START_REF] Chao | [END_REF]. For example, a system trying to mimic natural eyebrow movement, will most likely require a gloss marking every interval where the signer is actively using his eyebrows in a meaningful manner.

SL recognition, more than synthesis, relies on annotated video-data. It is by way of linguistic annotation data that an algorithm collects enough information to recognize individual signs [START_REF] Nickel | Pointing Gesture Recognition Based on 3D-tracking of Face, Hands and Head Orientation[END_REF][START_REF] Ding | [END_REF], relevant facial features [Von Agris 2008, p. 3] and signing or non-signing segmentation patterns [START_REF] Han | [END_REF], Yang 2009]. In this regard, annotations are used to make sense of data in automatic tasks and, as such, serve as ground truths for evaluating how effective each task can be [START_REF] Moehrmann | Semi-automatic Image Annotation[END_REF]].

Additionally, recognition techniques can serve as support for many areas; in synthesis, for example, recognition algorithms can be used to find grammatically significant movements [START_REF] Erdem | [END_REF], Neidle 2009], which could later lead to better quality synthesis.

Despite of the importance of annotations for SL research, their availability is limited.

The ever present need for linguistic experts, the high specialization of annotation tasks (see Subsection 1.1.1.2, p. 5) and the heterogeneity of corpora (see Subsection 1.1.1.1, p.

4), hampers the production of new, correct annotations. The problematic further deepens if we consider that new linguistic knowledge can weight on the adequacy of previous and future annotations [Schembri 2010, p. 3], which points to the need of constant annotation cycles over the same corpus. This situation has prompted research on the automation of at least part of the annotation process, in an effort to streamline the creation of new annotations regardless of corpora [START_REF] Neidle | [END_REF][START_REF] Braffort | [END_REF], Dreuw 2008a].

Different automatic and semi-automatic annotation projects have emerged, with applications in SL research. Research on annotation of image datasets covers the detection of relevant gestures in conversation [Wilson 1996], the identification of human actions [START_REF] Duchenne | [END_REF]] and annotation of body language [Chippendale 2006]. Other efforts more directly related to SL come in the form of complete platforms with automatic annotation algorithm integration [START_REF] Neidle | [END_REF][START_REF] Braffort | [END_REF]], the development of automation modules for already existing annotation tools [Dreuw 2008a] or the creation of corpus-specific software, aimed to ease annotation and transcription of distinct corpora [Yang 2006[START_REF] Pitsikalis | [END_REF][START_REF] Gonzalez | [END_REF]].

Unfortunately, automatic support for annotation relies on the same techniques used for SL recognition. Consequently, researchers have to deal with the same kind of problems present in the aforementioned area; namely the lack of homogeneous corpus data, shaky theoretical linguistic frameworks and the absence of a written representation [START_REF] Morrissey | [END_REF]].

Moreover, this relationship between the two areas implies that the development of new annotation algorithms depends on the existence of previous annotations from which to learn from. Consequently, it's not difficult to see that, being a recognition task in itself, the creation of an automatic annotation algorithms will only be possible for existing annotation schemes where enough data is available; annotations based on new linguistic hypotheses, and cases with annotation few examples, will still be difficult to create.

In short, automatic annotation is limited by:

-The lack of a written representation, which contributes to the scarcity of large data repositories, as the ones needed for the application of classical NLP techniques;

the heterogeneity of corpus-data, which complicates the reutilization of automatic analysis algorithms across different corpora;

the changing nature of annotation tasks, very theory-dependent, which hampers the development of standard annotation templates.

In this regard, the work presented in this thesis is geared towards the representation of SL in semi-automatic annotation tasks, as introduced in the next section.

Contributions

This thesis, presents the application of formal methods for the description of SL in computer-based research. Roughly, formal methods are mathematically-based techniques used to rigorously describe (specify) complex systems and their properties. They provide theoretical tools to build, develop and validate systems regardless of their complexity, maximizing confidence and minimizing unexpected behaviors [Monin 2003]. To this end, formal methods often rely on formal specification languages to specify system processes.

A description created with a specification language is called a formal specification, and they serve as guidelines on how a system should work. One of their main advantages is that they can be mathematically verified. That is, it is possible for an automatic algorithm to determine whether the described system satisfies certain properties or not, ensuring that the described process is error-free. The driving idea behind this document's contributions, is that the same techniques can be used to specify SL productions and verify their characteristics, which in turn can provide some insight into the development of automatic annotation systems.

Several industries rely on the use of formal methods for the implementation of their industrial processes. For instance, formal verification is commonly used in the development of safety-critical systems [START_REF] Bowen | [END_REF]], communication technology [START_REF] Barbulescu | [END_REF]],

cloud computing [START_REF] Boer | [END_REF]] and complex software systems [START_REF] Woodcock | [END_REF]]. Finally, formal methods are not limited to industrial uses; the same tools have applications for research in biology [START_REF] Hartel | [END_REF][START_REF] Zambach | [END_REF]], group interaction [START_REF] Hoek | [END_REF]] and linguistics [START_REF] Kamp | [END_REF][START_REF] Moss | [END_REF].

This thesis presents the utilization of formal methods to transform corpora into an intermediate representation layer, where automatic annotation algorithms can work in better conditions than when working directly with video sequences. The main idea is that corpora can be described with a formal specification language, instead of a classical SL transcription language. Moreover, we prove that the proposed formal language is more expressive than any of the existing SL notations, and that it can be adapted to use the same symbolic conventions.

By describing each corpus with a single formal specification language, heterogeneity becomes less of a problem. Incidentally, this can increase the sizes of the available datasets. Moreover, any algorithm developed to work with these formal representations of corpora can be reused on any new corpus, given that it can be described with the same language. In essence, this method permits seeing each corpus as a standalone system with well-defined rules. The added advantage is that annotations can be conceived as observable properties of the system and, as such, can be found by way of formal verification. A diagram depicting the process is presented in Figure 1.3. More information on formal methods and their applications can be found on Section 3.4, Chapter 3 (p. 67)

The Propositional Dynamic Logic for Sign Language

A modal logic was chosen as a formal specification language based for corpora: the Propositional Dynamic Logic (PDL). This logic was originally created to specify and prove properties on computer programs [START_REF] Fischer | [END_REF]]. PDL uses the modal operators [a] and a to denote necessity and possibility, respectively. For instance, the expression [a]p has the meaning that, after performing action a, p will necessarily hold. On the other hand, the expression a p describes the situation where, after executing action a, p may possibly hold.

In general, PDL permits the encoding of change by way of formulae. For instance, the formula f 1 → [a]f 2 can be read as "If f 1 holds, then f 2 will necessarily hold if action a is executed". When f 1 is a proposition meaning "my bucket has water", a is the action "I empty my bucket" and f 2 is the negation of f 1 , then the formula reads "if my bucket has water, then necessarily my bucket won't have water if I empty my bucket". The same idea can be applied to SL articulators, so as to model them in terms of their actions.

For example, if f 1 is a proposition meaning "the right hand is touching the head", action a is the action "the right hand moves to the chest" and, once again, f 2 is the negation of f 1 , then the formula would read "if the right hand is touching the head, then it won't be touching the head if it moves to the chest".

For SLs, a particular variant of the PDL was developed, the Propositional Dynamic Logic for Sign Language (PDL SL ). With the PDL SL , articulators are interpreted as independent agents, where each articulator has its own set of valid actions and propositions, and executes them without influence from the others. It is important to note that this does not reflect the relationship between articulators in linguistics: in real life, articulators are often dependent on each other, for various reasons. However, it is important for PDL SL to be able to establish these kind of relationships explicitly rather than implicitly, as this contributes to the flexibility of the language.

The simultaneous execution of different actions by several articulators yield distinct situations, which can be modeled as graphs for formulae interpretation. In essence, these graphs depict time intervals without change as vertices, while the edges are taken to represent intervals where changes occurred. Returning to articulator independence, it is the graph where any dependent articulatory actions clearly show, as they will always occur simultaneously, on the same edges. A more detailed explanation of this interpretation can be found on Chapter 4, p. 77.

The use of a formal logic as specification language brings flexibility to the task, since it is possible to encode any information by formulae as long as it can be thought of as a propositions (i.e. a true-false statements). This adaptability, alongside the existence of well established inference and verification methods, makes it a good choice to deal with situations where incomplete or erroneous information is present; by using logic, it is possible to prove automatically and without ambiguity whether a certain specification is inconsistent and correct it. Additionally, the inherent compositionality of formulae makes it possible to mix them, separate them and reuse them to create new expressions, which comes useful to specify multimodality (see section 1 p. 1).

Finally, the use of logic not only benefits corpus specification, but enables the creation of annotation templates. These are none other than PDL SL formulae describing the desired properties to be found on corpora. So, for instance, if the formula

f 1 → [a]f 2
seen above where to be verified on a corpus (with f 1 being that the right hand touches the head, f 1 ≡ ¬f 2 and a meaning that the right hand moves to the chest), the result would be every state where the right hand started touching the head and ended over the chest. This information can then be poured into an annotation tool, in order for a human expert corroborate the results and correct the annotation if needed, simplifying the overall process.

The complete definition of PDL SL is given on Chapter 4, p. 77.

Semi-automatic Annotation using PDL SL

The choice of PDL SL , led to the creation of a framework for the implementation of semi-automatic annotators based on this logic. The framework was designed to follow the architecture presented in Figure 1.4. The idea is that the system receives an untreated corpus, converts it into a graph respecting the definitions given by the PDL SL and uses it to generate an editable annotation file. Several modules along the way let the users determine how the corpus will be analyzed, what kind of annotations will it generate and how the graph will be created. Roughly, the Division Module uses a feature tracker to follow the articulators of interest and determine if there were any changes at any given time. The implementation developed for this thesis, uses a head and hands tracking algorithm [Gonzalez 2011] The merged graph is passed to the Logic verification module, where an automatic algorithm performs the annotation procedure. The module receives a "Formula Database", which contains a series of formulae created by a human annotator. Each formula encodes the description of a desired annotation as a property, so that the module can use it as input for a logic verification algorithm (see Subsection 3.4.1,p. 68). The verification procedure is straightforward; for each state on the graph, the module will verify if each formula on the database is satisfied. If it is, it will add it to the list of proposed annotations, alongside the corresponding time-frame where the annotation was found. If a formula is not satisfied, it is simply discarded.

Finally, the list with the proposed annotations is converted to the format of a multimodal annotation tool. Here, an expert can change the automatic results to correct mistakes or to add more information to the final gloss.

A more detailed presentation of the annotation framework and the implemented algorithms can be found in Chapter 5, p. 99.

Empirical Application of PDL SL to Sign Language Annotation

The final contribution of this work, consists on the analysis of the use of the proposed annotation framework on real world data. For this, a set of properties were encoded as PDL SL formulae and were later given to an automatic annotator, implemented with the help of the annotation framework previously presented. The process was used to find properties over videos from the Dicta-sign corpus [START_REF] Matthes | [END_REF]]. An example of a resulting gloss can be seen on figure 1.5. In the image, a user defined the property BOTH as RIGHT ∧ LEFT; that is, the system has to find every time interval where both the right and left hands are static (marked as KEYPOSTURE on the figure). The obtained results and their qualitative analysis are detailed on Chapter 6, p. 129.

Conclusions

In brief, this thesis presents a series of problems related to the semi-automatic annotation of SL corpora and a method of solving them by way of a formal logic:

-The lack of a written representation for SL corpora was addressed by the use of a formal specification language, the PDL SL , which let annotation algorithms work with an intermediate corpus-representation rather than directly with images;

-the heterogeneity of corpus-data was acknowledged by the creation of an automatic annotation framework, designed to create graph representations from any corpus regardless of the technology used for its creation; and, finally, the changing nature of annotation tasks was faced by using PDL SL formulae as annotation templates, which can be easily changed and reused to adapt to different needs.

A more thorough analysis of this work's results can be read in Chapter 7, p. 147.

Chapter 2

Sign Language Overview

Sign Languages (SLs) are complete, complex standalone visual languages. They are often independent from vocal communication systems [START_REF] Emmorey | [END_REF]] and they are not universal. In particular, they are as varied as vocal languages, have the same expressive power than these, and possess their own particular grammars and vocabularies [Wilbers 1987]. There do exist artificial SLs like the International Sign Language (ISL) trying to improve global Deaf communication. In essence, ISL follows the same philosophy than Esperanto [Tonkin 1997], in the sense that it tries to group common grammatical structures and signs into a single language to facilitate learning [START_REF] Mckee | [END_REF]].

Nevertheless, even in artificial cases like this one, lexical and syntactical variations are present, contributing to diversification [Beckner 2009, p. 15].

SLs can be found across most countries, in most cases with their own particular rules and linguistic characteristics. As such, British Sign Language (BSL) and American Sign Language (ASL) are completely different languages, even with low mutual intelligibility [McKee 2000]. Here, it is important to stress that SLs are not visual forms of vocal languages; as such, French Sign Language (LSF) and ASL, are completely different languages from French or English [START_REF] Emmorey | [END_REF]]. This doesn't mean that SLs are not influenced by vocal languages, but rather than their grammatical structures differ; they are not versions of the same language [Sutton-Spence 1999a].

Even though SLs are complete languages, they differ from speech in some aspects. Mainly:

-They are visual: SLs are based on gestural expressions, characterized by movement, rather than by sounds or written symbols.

-They have multimodal structures: they convey messages by way of complex interactions between the hands and other parts of the body.

It is important to note that there is a difference between multimodality as used in SL linguistics, and how the term is understood elsewhere. In vocal linguistics, multimodality refers to the use of different human communication channels at multiple levels of abstraction, which together are able to modify the meaning of a message [Gibbon 2009, p. 11]. As such, variations such as voice intonation could modify or reinforce what an utterance ultimately represents. In contrast, SL modalities contribute specific information to the task of building meaning;

in consequence, each of the different communication channels has a predefined role, crucial from the start for the formation of even the smallest meaning units [Cuxac 2007b, pp. 14-15].

-They make extensive use of space: spatial locations around the signers fill several grammatical roles and are fundamental to build discourse.

-They depict iconicity: signers depict with their body different levels iconic representation, going from mimicking characteristics of real-life objects, to assuming the role of an external entity during discourse [Cuxac 2007b].

The characterization of SL corporal expressions, has been an object of study in linguistics since the end of the XIX century; however, few linguistic studies exist, comparing the properties of SLs with respect to vocal languages. Regardless, some well established theories have emerged in the last few decades, geared towards gaining a better understanding of the underlying mechanisms ruling gestural communication.

In the following paragraphs, a brief cultural review is presented, outlining the evolution of SL and their study in western cultures. Following this short outline, a more thorough introduction to SL linguistics is presented, which extends until the end of this chapter.

Cultural Context

For the first decades of the XX century, SL research had been directed towards the acceptance of SLs as full-fledged natural languages; only in the last two decades, they have started gaining the same status as vocal languages around the world (e.g. as recently as 2005 for the European Union [Timmermans 2005]). Before that, SLs were hardly ever considered part of human language, and concepts such as regional denominations (like LSF or ASL) were not even heard of [Slobin 2006]. This constant struggle towards SL acceptance has had important effects, not only on how they are studied, but also on how the language themselves evolve [Frishberg 1975].

The earliest recorded mention of the Deaf and the existence of gestural languages, comes from Hellenic Greece. Both Plato and Aristotle made clear references of the use of SLs by their contemporaries [Cerney 2004]. However, the conception of the Deaf as a community united by language, or even just the use of SL in education, would not become a common practice until the XVI century [Baynton 1995]. Before that time, deafness was understood by following the initial hypothesis of Galen (the Greek physician), who thought that hearing was affected by speech and vice-versa. Therefore, integration was centered around forcing the Deaf to speak, assuming that it would improve their hearing [Eriksson 1998].

With time, religion played an important role on changing the views of the people on Deafness, promoting new forms of integration for the Deaf into society. For instance, the Deaf were allowed to participate ceremonies of the Hebrew tradition, even though it prohibited most people with disabilities from entering the temple. On medieval times, Christians worked with Deaf communities while trying to spread the Gospel among them [Tebbe-Grossman 2008]. Finally, around the XV century, Deaf education in Europe started to be completely overtook by catholic monks, in an effort to introduce them into confession [START_REF] Stokoe | [END_REF]]. As such, it was inside the monasteries that strong SL communities started to blossom.

The modern linguistic study of SLs can be traced back to France in 1750 [Cerney 2004].

On that year, Abbe Charles-Michel de l' Épée undertook the teaching of two deafmute sisters. From that moment on, and for nearly three decades, he directed an [START_REF] Sperling | [END_REF]] and overlooking SLs in favor of speech therapy. This school of thought is still prominent in several places around the world, since its supporters argue that it encourages integration [Hogan 2008]. However, the use of speech-based learning continues to be a contentious issue in Deaf education, to this day [Eriks-Brophy 2004].

In the next section, a brief introduction to SL characteristics is given. Simultaneously, some insight on how SLs linguistics are related to vocal language linguistics is presented, alongside some general notions of SL use.

Sign Language Linguistics

Linguistic research of SLs has gained new dimensions beyond the search for legitimacy, striving towards gaining knowledge about the languages themselves. To this end, linguists have adopted the basic hierarchical structure commonly used in vocal language linguistics [START_REF] Akmajian | [END_REF]], dividing language studies into hierarchical levels of analysis such like:

1. Phonology.-Studies the smallest units of sound in a language, called phonemes, and the implicit system of rules determining how these are produced by a speaker.

It is deeply related to phonetics, the science which studies how speech sounds are produced, transmitted and perceived by a speaker [Hayes 2008]. Thus, unlike phonology phonetics deals with real, measurable data.

2.

Morphology.-Describes how the smallest units of meaning, morphemes, are combined into lemmas 1 , or lexical units. In essence, it describes how words are formed [Lieber 2010].

3.

Syntax.-Explores how the composition of lexical units form sentences.

Complementary levels and alternate classifications can be found in the literature, however these three have long been of special interest for SL studies [Kegl 1976].

The aforementioned levels of description tend to build upwards from very small structures.

As such, for the rest of this document, aspects related to phonetics will be referred to as "low level" whereas more abstract concepts such as morphology or syntax will be identified as "higher" levels.

Phonology and Phonetics

As explained in previous paragraphs, phonology is mainly concerned about language sounds and how they are combined by humans for communication. More generally, it may be understood as the basis for linguistic study, since it aims to describe the smallest language units well before the formation of meaning. However, when talking about SLs, phonology is not properly related to sound, but rather to the movements and forms

1. Not to be confused with the term lemma as used in mathematics, where it is usually characterized as a "helping" or "minor" theorem with respect to a more powerful result. Further appearances of the term will refer to the mathematical convention, rather than the linguistics one.

that human signers adopt while signing. In this manner, SL phonology rests on the assumption that signs are constructed upon meaningless building blocks, akin to vocal phonemes [Axelsson 2002, pp. 14-16].

By extension, SL phonetics centers around the physical elements intervening in the formation of these soundless phonemes: this is, where classical phonetics cares about productions of the vocal apparatus, its SL counterpart examines expression, posture, and other measurable visual aspects during articulation.

In vocal linguistics, articulation refers to the act of generating language sounds by affecting specific places of articulation 2 with speech organs such as lips, tongue or other.

Each of these, may have one or various places of articulation, which are areas such like the teeth or palate. Speech organs, also called articulators, may act as a places of articulation themselves and vice-versa, depending on their role during the formation of a phoneme. In essence, when an articulator affects a place of articulation, it changes the characteristics of the sound produced by the vocal cords. This enables speakers to generate a range of different phonemes, which are the minimal language noises forming utterances. Likewise, SL users articulate by affecting various places of articulation, in order to display phonetic configurations; the main difference, is that -instead of describing sounds -SL phonemes differ visually. As a result, it becomes apparent that SL phonemes are not articulated with the same speech organs used to generate vocal languages.

SLs are traditionally described as being mainly articulated by way of the hands, in concert with a set of other, non-manual, articulators. These visual organs affect places of articulation outside of the vocal tract, such as body and spatial regions distributed around the signer's upper body. In some cases, signers will even articulate on empty spatial locations, over places not directly touching their bodies. These fairly radical changes in language production, with respect to vocal languages, have lead to a tad of different theories trying to determine which visual cues are relevant for the phoneme formation process, and which are not [Axelsson 2002, pp. 14-16].

Phonemes, both in SL and vocal languages, are highly combinatoric in nature: the same set of units can create distinct meanings when produced in a particular order. Also, they differentiate from one another by changes on their phonetic features. It is important to note that, in vocal languages, each phoneme may correspond not only to a single sound, but to a set of different sounds; for instance, the sound related to the English vowel [a] may change between native speakers from different regions, whom may recognize the same phoneme even when spoken with different pronunciations. In this 2. Also points of articulation.

example, even though the sounds are not the same, they are still identified as being the same vowel. SL phonemes have been observed to follow the same principles, where each phoneme may have different realizations [Valli 2000, pp. 256 -257], based on how several visual phonetic features are modified. In later chapters, a more detailed overview of how phonetic features of SL are represented, since the main contribution of this thesis is devoted to provide new formal tools for SL phonetic representation. Nonetheless, a brief introduction to SL phoneme formation is given in the following subsections, starting with a brief description of the hands' functions as SL articulators, and their capabilities to display phonetic variations.

Hands

In SL, the hands are the most productive articulators. They are widely displayed during signing, and their flexibility and movement range let them articulate a vast number of different combinations. In essence, they roughly correspond to the definition of active articulators in articulatory phonetics of vocal languages [START_REF] Hillston | The Sounds of the World's Languages[END_REF]].

For their study, hands are distinguished as either dominant or non-dominant 3 . The dominant hand, is the hand that plays the active role during signing; this is, it is the one preferred to perform motor tasks. In contrast, the non-dominant hand plays a passive role during signing; in some cases, it will even remain static. Generally, the signer will use his or her dominant hand to execute larger, more complex motions, whereas the nondominant hand will usually be relegated to perform less salient movements [START_REF] Battison | Phonological deletion in American sign language[END_REF]].

The choice of right-dominant or left-dominant can vary from signer to signer; however, the roles' functions remain the same, regardless of which hand is playing which.

With respect to the use of the hands, signs can be classified into three categories:

-Single-hand signs.-These are signs where only one of the hands articulate, either the dominant or the non-dominant hand.

-Two-hand signs.-In these, both hands articulate simultaneously.

-Buoys.-This is a special case where one of the hands articulate (usually the dominant) while the other one remains fixed over some spatial location. The static hand serves as a deictic marker [Lyons 1977], usually referring towards a discourse entity or directly acting as the representation of one.

Hands can affect several articulation places around a signer's body, with the head, neck, torso and arms being the most common. Hands can also, and often do, serve as points of articulation for two-handed signs. For instance, in Figure 2.1, the signer articulates 3. Can be also referred to as the weak hand.

the right hand over the left hand, which remains fixed during the entire production of the sign. It is important to note that this is not, by any means, an exhaustive list; each SL will use its own distinct set of articulation places, which can differ in number and position from all the others. Figure 2.2 shows a rough diagram with these and other possible articulation places. The same phenomenon can be seen with vocal languages: they produce their own distinct set of sounds, depending on how speakers affect specific articulation places.

Broadly, these would correspond to passive articulators in vocal languages articulatory phonetics [START_REF] Hillston | The Sounds of the World's Languages[END_REF]].

It is not necessary for the signer to have physical contact with the body for the hands to articulate; they may hover around the approximate region, as long as the reference to a point of articulation is clear, as is the case with deixis in vocal languages [Lyons 1977]. As previously stated, there are also instances where the points of articulation are not bound to body parts. Some articulations take place on the neutral space, an unmarked physical space in front of the signer's chest, where signs with no fixed body location are produced. In these cases, the articulation place is not linked to the signer's body but to the space itself.

Other articulators

Besides the hands, other body parts can provide active articulation, such as the head or the mouth [Crasborn 2008b]. It is common for some articulation places to change between being active or passive during signing. For instance, the head is used as the articulation place for signs like EAT LSF or THINK LSF , as shown in Figure 2 However, the head will sometimes serve as articulator. For instance, in the sign SLEEP LSF , the signer articulates with his head by tilting it towards the open palm, as shown on In this sign, it is the palm who acts as the head's point of articulation. Other body parts such as the eyebrows, lips and cheeks hold similar characteristics, as they are also capable of articulation [Frawley 2006].

Multimodality

The flexible nature of SL articulators, gives origin to the phenomenon of multimodality:

multiple articulators acting synchronously to build language units together [START_REF] Sandler | [END_REF]].

As briefly explained at the beginning of this chapter, multimodality in the context of vocal languages has a different meaning than the one used to study SLs. In the former, multimodal information seems to modulate speech by giving, for example, iconic cues on different communication channels (voice, gesture, etc.), in order to better convey the semantics of a message [START_REF] Vigliocco | Language as a multimodal phenomenon: implications for language learning, processing and evolution[END_REF]]. In SL, however, multimodal information is crucial to understand any message, since very specific data is provided by each channel during the sign formation process 7 . In this sense, signers need to receive as much information as possible from all modalities, in order to render utterances understandable.

In other words, at any given time, several body parts such as the hands, head, lips and others, will articulate simultaneously in order to build a phoneme 8 . Just as with vocal languages, phonemes are rendered distinguishable by combining different articulation parameters in a unique way.

Informally, SL modalities can be interpreted as communication channels carrying the information generated by each articulator (manual or otherwise). Under this definition, the "right hand modality" makes reference to the channel that holds information produced by the right hand. 9 The information transmitted by each individual channel will be necessarily unique, since articulators are morphologically different from each other and play very specific roles in utterance production.

The Movement-Hold Model

Signers manage to arrange their articulations into well defined time-units. A time-unit, is none other than the interval of time in which a phoneme takes place. The morphological 7. SL linguists like [START_REF] Cuxac | La langue des signes française (LSF): les voies de l'iconocité[END_REF]], use a specific term for this phenomemon: multilinearity. 8. Some authors call the basic units of SLs cheremes, but this document will use the term phoneme for clarity. 9. The terms channel and modality will be used interchangeably for simplicity; nevertheless, the reader should be aware that the literature might define the same concepts under different names.

information contained inside a time-unit is called a posture. Broadly speaking, time-units are what constitutes phonemes in SLs; hence, their postures need to be unique enough to make them distinguishable from other phonemes. Similar to vocal languages, SL linguistics study how groups of phonemes build up to create meaning. Current sign-formation theories, adhere to the idea that the sequential structure of time-units is phonologically relevant; in this view, SL signs are formed by well-defined configuration sequences, which together convey meaning.

The first description framework developed under these assumptions was the Movement-Hold Model (MHM), proposed by [START_REF] Liddell | [END_REF]]. The MHM interprets time-units as utterance segments, and divides them into two distinct groups: Holds and Movements.

In essence, a Hold is a segment with a fixed posture; this is, its information won't change throughout the entire time-unit's duration. On the other hand, Movements are segments where changes do occur. Usually, Holds will be connected to Movements in the phonological sequence. In a way, Movements can be seen as transition segments between two postures, as shown in the diagram presented by Figure 2.5.

Hold (H

A ) Movement (M AB ) Hold (H B ) Posture A Posture A Posture B Posture B

Co-articulations

Co-articulation is the process of phonetic change where, after producing a phoneme, the organs involved in articulation adjust to produce the next one. In the case of SLs, this translates into the introduction of meaningless movements to the MHM sequence, as

shown by Figure 2.7.

Sign Co-articulation Sign

H A M AB H B M BC H C M CD H D Figure 2.7: The transition movement M BC , between H B and H C , is a co-articulation.
Movements M AB and M CD shown above, are integral parts of their respective signs. On the contrary, M BC exists just to serve as a stepping stone towards the articulation of

H C , coming from H B .
Depending on the previous and next segments in the sequence, previously significant

Movements can be reduced to co-articulations and vice-versa. Figure 2.8 shows a representation of this phenomenon.

Sign Co-articulation Sign

H A M AC H C M CD H D M DB H B Figure 2.8:
The transition movement M CD , before part of a sign, is now a coarticulation.

In Figure 2.7, the sequence H C → M CD → H D forms a sign, which renders M CD significant. However, the same sequence doesn't form a sign in Figure 2.8, turning M CD into a meaningless segment. This happens despite the fact that, in both cases, M CD appeared in the same order with respect to H C and H D . This goes on to show that the classification of Movements as co-articulations is not possible at the phonology, but rather relies on rules existing at the morphology.

Morphology and Lexicon

Morphology is the sub-discipline of linguistics that studies how the smallest meaning units, morphemes, combine to form lexemes, which are none other than words. It also studies how lexemes themselves are modified (inflected) by morphemes, combinatorially building semantic variations: for example, the lexeme walk can be inflected into the forms walks, walked or walking [Booij 2005, pp. 8-9]. Together, lexemes form lexicons, which are essentially indexes of conventionalized words in a language.

In SL, morphology deals with the internal structure of signs in two ways: it studies both the multimodal nature of SL morphemes -arising from the use of different articulation channels -, and the use of signs as grammatical affixes [START_REF] Aronoff | [END_REF]]. More intuitively, SL morphology studies both:

-how the alteration of direction, rhythm, or shape of a base sign, modifies its grammatical features;

-how sequentially concatenating signs (as prefixes or suffixes) to a base sign, affects its meaning.

Essentially, this duality in SL morphology yields an informal classification of signs, which divides them into easily identifiable groups for their study:

Lexical signs Also called dictionary signs, as these are the ones more likely to be found in dictionaries. Lexical signs have well-known meanings, as they make reference to specific concepts, objects and ideas. Roughly, these are the most closely related to vocal lexemes.

Grammatical signs

These are the ones used as affixes, to modify properties of lexical signs. Broadly, they "insert" meaning to surrounding lexemes during discourse [Contini-Morava 2000, pp. xii -xiv]. For instance, they can be used to mark aspects such as pronouns, number, to differentiate arguments, etc. These kinds of signs are difficult to define out of context, in part due to their grammatical function.

Finger-spelled signs Refers to sequences of hand configurations and movements used to represent single alphabet letters. These signs let the signer spell out mostly nouns, with particular emphasis to loan words [Padden 2003, pp. 18-22].

Alternate classifications may exist in the literature, depending on the studied language;

regardless, the basic rules of inflection remain consistent across different SLs, thus prompting further inquiries on the roles played by factors such as space, on different morphological case studies.

Space

Space plays an important role in SLs. It is through spatial relations that signers are capable of expressing complex reasoning [START_REF] Emmorey | [END_REF]]. Accordingly, space has been observed to fulfill diverse linguistic roles, notably deictic, by providing mappings towards discourse entities and other syntactical functions [Padden 2010a]. Signers will commonly map spatial locations to represent persons, places or objects, which activates the referred space regions. This phenomenon is called spatialization, and serves to keep track of discourse referents; once defined, space locations remain active as long as the signers keep acknowledging their existence. This avoids the need of redefining a referent multiple times over the same context. For example, Figure 2.9 shows a signer performing the lexical sign FRIEND LSF and then pointing to the side, indicating that the space to his right will represent a friend.

FRIEND LSF Spatialization to the right

Upper-view of active locations Similarly, new characteristics of the referred entity can be introduced by making reference to the active spatial location. Following the same example, if the signer performs UGLY LSF and points towards his right side, the utterance would translate as "friend is ugly".

In addition to referent localization and agreement, space in the morphology fulfills topographic functions, by permitting to specify how objects are physically located with respect to one another. For instance, in several SLs it is possible to express "a cat is over the fence" by assigning a location for fence and then signing cat just above [Engberg-Pedersen 1993[START_REF] Meir | Syntactic-semantic interaction in Israeli Sign Language verbs: The case of backwards verbs[END_REF], MacLaughlin 2000].

Sign Language Semantics

Semantics deals with linguistic signs [START_REF] Saussure | [END_REF]]; in particular, with how meaning is established and conveyed by language. In SL, this process is deeply linked with form and space since, contrary to vocal interlocutors, signers can use their bodies to provide rich visual representations of existing objects, situations and people, which in turn can produce complex discourse.

Iconicity

The term iconicity, refers to how the form of a sign, an icon, is directly linked to the meaning of the sign itself. Contrary to vocal languages, SLs rely heavily on iconicity, often as a central part of communication [START_REF] Liddell | [END_REF]]; the same behavior can be seen Iconicity is present in a large number of SL lexical signs, but not always with direct relation to physical objects; sometimes, the iconicity of a sign is related to a metaphor rather than to the form of a real, physical, object. An example is given by sign PAUSE LSF , presented in Figure 2.12.

PAUSE LSF Figure 2
.12: PAUSE LSF uses iconicity in a metaphoric way, by representing a pause as a physical "break".

The sign PAUSE LSF is performed by holding both hands together as if they were grasping an object, and then separating them abruptly as if breaking said object. The form of the sign relates then to the meaning of "break", which is metaphorically linked to the concept of "pause", but doesn't really involve the physical act of breaking something.

The iconic use of space is also a notorious characteristic of SLs [Padden 2010a]. For instance, to describe that a recipient is big, the signer can execute the sign RECIPIENT LSF with very exaggerated movements. Similarly, to express that an object is small, the signer will perform the sign with very short movements, delimiting the surface of the proposed object. In the same way, signers can outline the size of buildings, surfaces or spatial points of reference, which most of the time will remain active in space, in the position they were originally located. In this way, signers can describe the distribution of an auditorium, of a neighborhood, or any other complex scene, where they can either place themselves or other referents in order to establish complex relationships [Engberg-Pedersen 1993]. In a way, this transforms spatial regions into objects, which can be modified directly during discourse (similar to what happens in discourse deixis of vocal languages [Lyons 1977]). For example, the signer can "take" the recipient he originally placed in space (by mimicking the action of taking the object), and locate it elsewhere (by mimicking the release of the object in a different place).

Finally, the maximal expression of SL iconicity is shown by the role shifting phenomenon [START_REF] Cuxac | La langue des signes française (LSF): les voies de l'iconocité[END_REF]], where signers "act the part" of a discourse referent by taking their place and assuming their actions as their own [Lillo-Martin 1995]. In this way, the signer can directly show what a referent did or said from the referent's perspective.

During a role shift, the signer completely steps out of his own persona in order to mimic the behavior of the referent. In this situation the entire body expression becomes iconic, as it is completely influenced by the characteristics of the role taken. Putting everything together, it is easy to see that meaning in SL signs is deeply linked to multimodality at every level of study: it depends heavily on how signers interpret different forms -created by several articulators working simultaneously -over many layers of abstraction. As such, it becomes important to determine what individual functions each articulator may have, how they are modified to convey the images needed to build these forms and how they manage to produce unambiguous messages, as explained in the next section.

Parametric Sign Language Articulation

The information produced by utterances, can be modeled by way of discrete articulation parameters. Depending on their physical characteristics, articulators provide a set of different parameters in order to convey information. The hands will invariably produce a great amount of the overall message, since they are very flexible and can change their form easily. However, this is not to say that the information provided by Non-Manual Features (NMFs) is any less important; research shows that native signers identify signs faster if they have NMFs in them than if they don't [Wilbur 2009].

There are five classical parameters used in SL description 10 , based on the seminal work by [START_REF] Stokoe | [END_REF]]. They are enumerated here as follows:

1. Hand configuration.-Refers to the shape of the hand while signing. Due to the high flexibility of hands, the quantity of available configurations can be very high.

However, observations on various SLs have shown that only a relatively small subset of the possible configurations is commonly used implying that, at least in some cases, the quantity is not as big as it could be [Mann 2010]. Figure 2.14

shows some common hand configurations used in ASL. More complex phenomena such as repetition can also be described as part of this parameter; that is, whether a particular motion is executed just once, or several times as part of a single movement. As the existence of single-handed signs implies, not all articulators participate on the production of all signs; in the majority of cases, only a subset of the possible parameters is necessary to distinguish each. For this reason, some time-units may lack of movement, NMFs or even hand interaction, at all. This doesn't affect the underlying principle of sign formation but may, however, complicate low-level observations, due to the sheer amount of possible parameter combinations [START_REF] Liddell | [END_REF]]. This phenomenon will be apparent in the following chapters, where it will be explained how this combinatoric nature affects distinguishability of individual postures, which in turn can become an issue both for both representation and automatic recognition.

12. Image obtained from [START_REF] Venkatagiri | Lecture Notes on American Sign Language[END_REF]].

Chapter conclusion

This chapter has presented the main characteristics of SL linguistics, with special emphasis on how SLs are most commonly described at the phonetic level. SLs are the visual-gestural languages that members of the Deaf community use to communicate.

They differ from vocal languages in their production, as they are articulated in space by way of corporal movements. The complexity of their articulation parameters and phonological features, make them interesting subjects of study both in linguistics and computer science. However, their very particular characteristics make them difficult to transcribe by way of written notations, which can pose problems to automatic analysis tools.

Similar to vocal languages, SLs are usually studied with the help of corpora: digital compilations of language samples documenting their use, usually annotated with external data for their processing. However, because of the difficulty to represent them otherwise, SL corpora are forced to remain as video or motion capture collections, which have to be treated with specialized computer-based tools for their processing.

Interest in the use of software tools for the study of SL has sparked new research ventures, specially in areas such like SL recognition and SL synthesis. However, the enormous quantities of possible posture combinations -and the physical characteristics of articulators -pose a number of different problems that need to be solved before new automatic solutions can be developed. This is specially true for phonetic representation, which ultimately serves as the basis of language construction. For this reason, this thesis is exclusively centered around representation issues on the phonetic level, and it proposes a flexible phonetic description framework that can be used within computed-aided SL research tasks.

With this in mind, the next chapter presents a review of current research in computer science, aimed towards the study of SLs. Emphasis is put on how new projects tend to work on problems related to the recognition and, specially, representation of segmental features and signing parameters, with perspectives on building high level solutions from these smaller projects in the future.

Chapter 3

State of the Art

As interest in the study of Sign Language (SL) has increased, the development of new computer-based techniques for their analysis has become unavoidable. However, contrary to what happens in vocal language research, SL projects have to deal with corpus representation challenges from the very beginning. For example, discussions about adequate corpora formats [Crasborn 2008c, Braffort 2010[START_REF] Hanke | [END_REF]] and multimodal annotation standards [START_REF] Martell | [END_REF], Dreuw 2008a[START_REF] Schembri | [END_REF] With respect to SL notations for linguistic research, interest has hovered around the development of good transcription formalisms, in an effort to reduce reliance on video materials. Also, this road have been explored as a way to potentially increase the application of Natural Language Processing (NLP) algorithms to SLs corpora [Miller 2001[START_REF] Van Der | [END_REF]. However, the existence of contradicting views in favor [Hoiting 2003] and against [Johnston 2010] transcription, further shows the relative instability of the area, blocking the adoption of transcription as a widespread method of analysis.

Sign Language Representation

Despite opposition to thorough phonetic transcription, it is often necessary in research to describe detailed SL sub-lexical information for recognition and synthesis. This proves to be specially important for the latter (see Section 3.2 below), as the existing SL synthesizers tend to use some form of notation to encode their inputs. This has led to the development of very specialized description tools, which have been integrated

to corpus annotation software like [Hanke 2002], for example. As a consequence, sign description systems like the Stokoe Notation or Hamburg Notation System (HamNoSys)

have gained popularity among researchers, as they have served as the basis of various SL projects on different domains.

In the following sections, some of the existing notations used to represent SL in research tasks are described. In addition, a small presentation of SignWriting -a written SL system for common day-to-day use -is given, in an effort to contrast how SL representation may change, depending of its intended use.

Stokoe Notation

Before the year 1960, it was usually assumed by linguists that SL signs were indivisible, incapable of being represented by way of separable units like sounds in vocal language words. However, with the publication of the paper by [START_REF] Stokoe | [END_REF]], a new paradigm in SL studies was born, where signs could be effectively "cut" into subunits for their description. This enabled the author to develop his own transcription system, the Stokoe Notation, aiming to capture signing in a linear structure akin to written vocal language.

The author designed his notation to be employed as a tool for the linguistic study of SLs. It provides a set of typewritten symbols, used to represent articulation place, hand configuration and movement. Figure 3.1 shows a subset of these symbols. on their place in the chain. The disadvantage of using such a limited set of characters is that the resulting descriptions become highly encoded and barely iconic with respect to the actual signs, which can impact readability. In addition, non-standard characters are often needed to describe articulation parameters of SLs other than American Sign Language (ASL), which can further complicate the comprehensibility of the notation.

Even with its disadvantages, the Stokoe Notation proved to be a practical way to encode SL, a feat showcased by the author with the creation of a detailed ASL dictionary [Stokoe 1976]. Later projects have tried to conserve this practicality by following the same representation strategy, but taking advantage of new technologies to create specialized symbols rather than just re-purposing Latin characters. In this manner, new notations like HamNoSys improve the readability of their sign descriptions by using more iconic symbol sets, closer to the actual visual form of the represented sign.

HamnoSys

HamNoSys is a phonetic SL transcription system. Like the Stokoe Notation before, it was originally created for linguistic research; it was not intended to be used as a SL writing system for daily life, but rather as a tool to represent research resources [Hanke 2004].

To this end, HamNoSys defines a greater amount of notation symbols; it holds around Like the Stokoe Notation, HamNoSys descriptions are written as chains of positional characters. One of the differences between the two, however, is that in HamNoSys symbols are highly specialized, so they'll usually retain their meaning regardless of their position on the chain. In this case, positioning serves rather to enable the automatic processing of the transcribed data; computer systems are able to parse sign descriptions without ambiguity, as the positional structure is known. This advantages have proven useful for the creation of HamNoSys-based annotation software [Hanke 2001] and for the development of avatar-based synthesis technology [Elliott 2004]. Even though HamNoSys tends to be more iconic than the Stokoe Notation, it still depicts signs with a high level of abstraction. Furthermore, as it is intended to be used as a tool for linguistic research, signs are usually described with great detail. This results in long and complex chains of symbols, which in some cases can become difficult to read and write without help of an expert. A slightly different approach to these kind of representation systems is depicted by the SignWriting notation, which was developed to be used as a writing system for SLs rather than for linguistic research. For this reason, SignWriting avoids describing symbols in a sequential order in favor of highly iconic structures, in an effort to visually represent the physical formation of signs.

SignWriting

SignWriting is a SL representation system inspired on a notation originally developed to capture Ballet movements [Sutton 2000]. The main principle behind it, is for descriptions to be both precise and easy to read. Contrary to HamNoSys and the Stokoe Notation, SignWriting is effectively used by the ASL Deaf community as a written communication system and not only as a tool to represent SL in research.

Similarly to the Stokoe Notation and HamNoSys, SignWriting describes phonetic parameters by way of a set of symbols, defined to represent hand configurations, places of articulation and movements. However, SignWriting doesn't describe signs as chains of symbols but rather as very iconic glyphs, representing postures as they would be "seen" from the point of view of the signer. An example of a glyph can be seen on Figure 3.6. In the figure, the circle represents the back of the head, giving an spatial frame of reference for the depicted signer. The white square means that the back of the hand is oriented outwards, while the asterisk symbol ( * ) represents a simple touch to the head.

Figure 3.7 shows other possible contact symbols.

Figure 3.7: SignWriting contact symbols to represent "touch", "grasp", "strike", "brush", "rub" and "enter".

SignWriting glyphs rely on the morphology of the human body to establish spatial points of reference by drawing simple figures. The head, for example, is represented by a big circle, usually featured prominently. From there, places of articulation such as the shoulders, face or others are defined with respect to the head. This, in combination with special modification symbols, serve to represent complex parameters such as Non-Manual Feature (NMF) or body movement in a very intuitive way. An example of the expressive capabilities of this method can be seen in Figure 3.8. As with locations, hand configurations in SignWriting are very iconic, even capturing the position of the fingers in the configuration glyphs. Figure 3.9 shows some of the symbols used to describe hand configurations.

6. Images obtained from [Sutton 2009]. On the other hand, movement representation remains fairly similar to HamNoSys, using distinct types of arrows to differentiate between types of movement. Figure 3.10 show the difference between vertical and horizontal movements. The contact symbols indicate that hands "brush" the signer's body while executing the movement, and the double arrows indicate that the action is repeated twice.

Sign Language Synthesis

As previously introduced, SL synthesis deals with the artificial generation of language utterances by virtual signers (avatars) [START_REF] Michael Kipp | Sign Language Avatars: Animation and Comprehensibility[END_REF]]. One of the main interests in the area is to build avatars capable of mimicking the nuanced parametric changes made by signers during discourse [START_REF] Huenerfauth | [END_REF]]. This is because detailed parameters can be crucial for the unambiguous identification of phonemes, due to their combinatoric nature (see Chapter 2, Section 2.2.1, p. 25).

In an effort to confer a more expressive quality to avatars' gestures, research in synthesis has tended to move towards data-driven approaches [Rezzoug 2006]. For instance, the work presented by [Cox 2002] proposed the development of a SL translation system, aimed to improve interaction between Post Office clerks and Deaf users. Broadly, the authors describe the construction of an automatic translator, used to transform a clerk's speech into synthetic British Sign Language (BSL) (produced by an avatar). In order to enhance intelligibility, avatar's productions are animated as accurately as possible by way of detailed human movement data. To this end, the researchers assembled a custom-made motion capture rig from different body bound sensors, including a head-mounted camera to capture NMFs. The rig served to build a small corpus, compiling data from multiple human signers, which was then used to generate realistic signing from the avatar. The quality of the animation was tested by synthesizing a set of 115 BSL phrases, which were given to a group of native signers to decide whether they were comprehensible or not. In their experiments, the researchers found that the average comprehensibility was situated between 42% and 70%. However, most of the negatives were influenced by linguistic variation rather than technical issues: in some cases, signers didn't recognize phrases because they were signed differently to what they were used to -not because the animation was flawed -further underlining the importance of linguistic research in the development of synthesis technology.

On the same vein, works like [START_REF] Huenerfauth | [END_REF], Lu 2010] present similar corpus capture and evaluation methods, oriented towards the development a better suited corpora for both synthesis and machine learning tasks. However, similar observations to those of [Cox 2002], regarding comprehensibility and utility of the obtained data, are expressed by the authors, pointing towards the lack of sufficient linguistic knowledge as one of the main reasons behind poor results in these kind of systems.

In this sense, some synthesis research has centered around issues other than improving data capture. This efforts go from the development of tools for the edition of existing corpora [Lefebvre-Albaret 2013], to the development of new representation models [Losson 1998] intended to enrich corpus information. For example, [START_REF] Karpouzis | [END_REF] presents the creation of a synthesis system's architecture for Greek Sign Language (GSL), oriented towards education. For its development, a number of GSL resources were collected through various projects. This lead to the creation of a grammatical model of GSL, intended to be used in the production of phrases. Additionally, the project includes a lexical representation database encoding individual signs with HamNoSys. Despite their efforts, researchers point out that their approach is limited by both lack of enough standard linguistic resources for GSL, difficulties with the technicality of the chosen representation system, and problems linked to the production of co-articulations, which lead to unintelligibility.

Finally, works like [START_REF] Awad | [END_REF], Duarte 2010], propose the analysis of corpus annotations to improve the quality of virtual signer animations. In particular, the authors define a custom annotation schema for their project, taking in account elements such as grammatical markers from facial expressions; hand-movement descriptions; deictic uses of space and, notably, the occurrence of co-articulations.

The adoption of technology standards to encode their proposed schema -like the Extensible Markup Language (XML) [START_REF] Bray | [END_REF]] -enables great flexibility on studying which changes depicted in the video are relevant and when: each human-identified sign in corpora can be decomposed into the different aspects defined by the schema, making possible not only the generation of motion profiles from data, but also the development of rules to encode how signers synchronize their articulations depending on what's being signed. In this manner, synthesis can be greatly improved by linguistic knowledge of sign morphology, by showing how they effectively form depending on the context of communication. However, the disadvantage of this kind of studies, is that they are heavily dependent on the existence of quality linguistic annotations; as previously said, this is not necessarily a given for every corpus (see Chapter 1, Subsection 1.1.1, p. 3). In addition, this also points out the limitations that notations such like HamNoSys have in synthesis; they usually have to be modified into more technical representations capable of this kind of schematic decomposition, as it is presented in the next section.

Sign Language Representation in Synthesis

SL representation notations in synthesis are usually built depending on their purpose inside the system. In some instances, descriptions will serve as thoroughly geometrical recipes, detailing how a sign has to be animated [Elliott 2004]. In others, representation formalisms can serve as higher level models [Filhol 2012b], introducing linguistic information to the process [START_REF] Lejeune | [END_REF]]. In most cases, there will necessarily be an overlap between the two, due to the importance of linguistic data for synthesis.

An example of the combination between linguistic and geometrical descriptions is given by [START_REF] Karpouzis | [END_REF]]. In their system, lexical sign representations are written in HamNoSys, while avatar movement descriptions are defined in the Scripting Technology for Embodied Persona (STEP) language [START_REF] Huang | [END_REF]]. A STEP description is shown in Figure 3.12, where the recipe of how to build a hand configuration is presented.

In general, their system parses HamNoSys descriptions into STEP instructions: each

HamNoSys symbol corresponds to a set of STEP scripts, indicating the avatar how to render sequences of postures. In this manner, linguistic resources created with HamNoSys can be synthesized directly without having to give geometrical descriptions to the system; as there are already STEP-conversion rules in place to do it automatically. Despite this advantage, the authors mention that their method could prove troublesome to extend beyond manual parameters, as articulation from NMF tends to be more nuanced and, thus, less adapted for a straightforward conversion.

par ([ turn(humanoid,r_thumb1,rotation(1.9,1,1.4,0.6),very_fast), turn(humanoid,r_thumb2,rotation(1,0.4,2.2,0.8),very_fast), turn(humanoid,r_thumb3,rotation(1.4,0,0.2,0.4),very_fast), turn(humanoid,r_index1, rotation(0,0,0,0),very_fast), turn(humanoid,r_index2,rotation(0,0,0,0),very_fast), turn(humanoid,r_index3,rotation(0,0,0,0),very_fast), turn(humanoid,r_middle1,rotation(0,0,1,1.5999),very_fast), turn(humanoid,r_middle2,rotation(0,0,1,1.5999),very_fast), turn(humanoid,r_middle3,rotation(0,0,1,1.5999),very_fast), turn(humanoid,r_ring1,rotation(0,0,1,1.7999),very_fast), turn(humanoid,r_ring2,rotation(0,0,1,1.5999),very_fast), turn(humanoid,r_ring3,rotation(0,0,1,0.6000),very_fast), turn(humanoid,r_pinky1,rotation(0,0,1,1.9998),very_fast), turn(humanoid,r_pinky2,rotation(0,0,1,1.5999),very_fast), turn(humanoid,r_pinky3,rotation(0,0,1,0.7998),very_fast) ])

Figure 3.12: STEP code for a given hand configuration.

Signing Gesture Markup Language

A similar approach is followed by the Signing Gesture Markup Language (SiGML) [Elliott 2004], a representation formalism based on HamNoSys. The main difference between them, is that SiGML is designed to work as a XML standard on its own. An example of a SiGML description is shown on Figure 3.13.

As with previous representation efforts, SiGML is based on segmental phonology models, such as the one presented by [START_REF] Liddell | [END_REF]]. However, unlike other formalisms, with

SiGML the authors strive to combine sign parameters into morphological structures:

each parameter description can be either interpreted all by itself, as a phoneme of sorts, or it can be grouped with others to be identified together as a lexeme. In practice, this means that avatars may execute either an isolated parameter (single description file) or complete signs (group of description files), by controlling the groupings of individual parameters. Also, XML has the technical advantage of having a well-defined, nested, structure; this simplifies the addition of new elements to the schema if needed, which can further adapt the language to contain more information than HamNoSys.

This inherent adaptability has resulted into the creation of more flexible representations: it has enabled the combination of multi-dimensional HamNoSys strings, representing higher level linguistic functions [START_REF] Elliott | [END_REF]]. In turn, this has opened the door to the exploration of synthesis at higher levels where avatars may, for example, receive instructions in term of linguistic functions (e.g. "make reference to") rather than geometric instructions.

Nonetheless, some expressiveness problems may hamper efforts in this direction, due to the fact that HamNoSys was originally created for phonetic transcription; this is, by design it lacks the necessary structures for syntactic representation, and thus it may require multiple extensions to be able to support it.

Zebedee

A different approach to SL transcription for synthesis comes in the form of Zebedee [Filhol 2009]. This formalism, is based on the phonetic model presented by [START_REF][END_REF] (see Chapter 2, Subsection 2.2.1.4, p. 29).

For Zebedee, segment order comes above purely parametric descriptions, making special emphasis on time constraints such as duration. In addition, sign descriptions in Zebedee are dynamic: parameters don't remain fixed over time, but are dependent of internal changes that may change their values over time. By establishing dependency relations, experts describing signs may center around modeling sign structure, rather than having to thoroughly specify every possible parameter in the resulting synthesis; dependencies take care automatically, without further intervention. The same mechanism, enables a signing avatar deducing which movements perform, as dependencies make every one of them deducible from descriptions. Figure 3.14 shows an example of a Zebedee description.

As shown in the figure, Zebedee enables the inclusion of typed variables, which can provide specific information about independent articulators, places of articulation, and dependency relationships between them. In addition, Zebedee makes use of space by giving experts the possibility of mapping variables to spatial locations, which in turn permits the definition of inflections under the same formal language. In this manner, lexical signs given to the avatar may be directly modified during synthesis, incidentally simplifying the system's input. With this, and contrary to purely phonetic approaches, sign descriptions can remain very succinct, while still being able to generate very expressible output in practice.

Higher level representations

Most representation languages for synthesis have centered around phonetic transcriptions, however some work exists towards the representation of higher level structures.

For instance, [Lebourque 1999] presents the development of a high-level specification, permitting the representation of spatial locations and the avatar's relation towards them.

The proposed formalism is powerful enough to represent simple phrases, however the notation remains fairly low-level in terms of movement and synchronization.

SEQUENCE "ballon" <language=LSF> <numvidlimsi="1014_tout.mov"> <refdico="aucune"> <described_by="Flora, ">

DEP loc = @ABST + <FWD | medium> DEP size = medium Alias %p0 -> [loc] + <UP | [size]> KEY_POSTURE(0){ KEEP: For $h=s,w #all4_contact($h) Orient NRM!palm($h) along <@PA($h), [loc]> End HERE:
Place @PA(s) at %p0 Place @H_BACK(w) at @I_KNi(s,1) }

TRANSITION(10){ Accel 1 Arc @PA(s) : <LAT | [size]> Arc @PA(w) : -<LAT | [size]> } KEY_POSTURE(0){ HERE: Place @PA(s) at SYM %p0 wrt [loc]
Place @PA(w) at @L_KN(s,1) }

End "ballon" Works like the one presented by [START_REF] Lejeune | [END_REF]] go into more abstract representations, defining a set of linguistic operations and encoding contexts and verbs' meanings into formal structures. In this way, high-level linguistic phenomena such like iconicity could be represented easily in synthesis tasks. However, the disadvantage of working with such high-level representations is that it loses flexibility when confronted with existing synthesis engines, as they tend to need very verbose instructions to work with [START_REF] Huang | [END_REF]].

Finally, improvements on the original Zebedee language -previously introducedhave resulted in the development of AZee [Filhol 2012a], a higher level representation language intended better accommodate multimodality in synthesis transcriptions. AZee permits the definition of synchronization rules inside descriptions, inducing an ordering of the articulatory information on different channels (see Chapter 2, Subsection 2.2.1. 3, p. 28). This enables the system to synchronize multimodal information into single blocks containing more than one posture, therefore enabling representation of more complex linguistic phenomena such as spatialization, or the modeling of grammatical markers such like questions.

Sign Language Recognition

Due to the particularities of their linguistics (see Chapter 2 Section 2.2, p. 24), SL recognition tasks tend to be very complex to achieve; in order to recognize discourse, an automatic system needs to know how to make individual sense of both phonetic and morphologic SL characteristics, as well as more complex phenomena such as iconicity or the different uses of space [START_REF] Bauer | [END_REF]]. For this reason, most of the existing research in the area has centered around the first two levels of linguistic study, in an effort to approach the problem in a bottom-up fashion [START_REF] Ong | [END_REF]]. As such, researchers tend to subdivide their research efforts into hierarchical sub-disciplines, reflecting the different levels used in linguistic research:

Sub-lexical recognition Work in this level consists on recognizing articulation parameters of SL articulators. This involves finding articulators on corpora and determining their states; knowing where they are positioned, which configurations they hold or whether they are active in discourse.

Individual sign recognition Classification of individual signs, both on isolated and continuous recognition tasks. Research in this area also includes sign segmentation: finding time-intervals corresponding to meaningful productions on corpora, regardless of the specific signs depicted by the material.

-Isolated sign classification: Identification of single signs -mostly lexicalon idealized conditions.

-Continuous sign classification: Recognition of signs during discourse, where a lot of uncertainties and natural variations may present themselves during production.

As implied, sign recognition relies on the correct identification of measurable parameters, which can be a very specialized task. Because of this, emphasis is usually given to techniques centered around SL phonetics, expecting to be able to build from there, in an effort to search meaning from the bottom-up.

Sub-lexical recognition

Sub-lexical recognition is rich in methods to solve different kinds of problems, starting from the identification of individual articulators on corpora. As previously stated, each articulator has its own set of characteristics, and they can be very different from one another. Accordingly, they contribute their own particular kind of linguistic information, which can be different from the others both in terms of form and function. In addition to these differences, corpus media itself may come with their own recognition-related problematics; recall that corpora are compilations of video or motion capture information, which may have an assorted list of shortcomings such like occlusions, irregular forms, signal noise, etc. All these factors can impact on automatic articulation parameter analysis and, in most cases, they are challenging enough to claim the research focus themselves, individually [START_REF] Ding | [END_REF]]. As a result, it is not uncommon for each articulator to have its own set of specialized recognition techniques, without considering how these may communicate in higher levels to actually apply NLP algorithms.

Individual articulators and single parameter recognition

One of the first challenges of SL recognition, is to robustly follow articulators under changing conditions. An articulator tracker, is an algorithm that calculates the geometrical position of one or various articulators over a given time interval. A lot of the existing trackers are oriented towards the hands, in part because they are featured prominently in corpora; because of their fairly independent nature, hands can be very accurately tracked, as it's easier to differentiate them in video from more nuanced articulations [Vogler 2007]. In spite of this huge advantage, problems may arise on their tracking depending on the specific conditions in which the algorithm is executed, which are not always optimal [Gonzalez 2011].

High accuracy hand-tracking methods like [Gianni 2009, Gonzalez 2011], use particle filters [START_REF] Isard | [END_REF]] to classify signers' hands and head with minimal supervision. Their respective algorithms are designed to work over generic video sequences, acknowledging the that most existing resources are unannotated video corpora (see Chapter 1, Subsection 1.1.1, p. 3). In general, the authors use the skin tone to select the image regions (blobs)

that could most likely be the hands or head. Each blob is sampled into a "cloud" of particles, where each particle has an associated weight corresponding to the probability of it being part of the articulator of interest. The filter is dynamic; at each step, it takes in account the previous, current and next observations to recalculate particle weight. With enough executions, the algorithm will inductively converge towards the desired model's solution. This enables following hands and head with some robustness, although it might be costly in terms of calculation time. Finally, both methods apply different techniques to compensate occlusion with some success, one relying on using a probability exclusion principle [Gianni 2009] and the other by calculating differences in luminance [Gonzalez 2011]. Nevertheless, approaches relying on skin tone tend to fail under poor illumination conditions, skin-toned clothing, cluttered backgrounds or other sources of noise.

To avoid these potential pitfalls, some authors have approached the segmentation problem by constraining the initial setup of corpora [START_REF] Starner | [END_REF]]; that is, they force very controlled conditions to minimize tracking errors. Other alternatives showcase the use of special markers during the segmentation phase, in order to avoid the use of skin tone; for instance, authors [Dorner 1994, Starner 1995, Grobel 1997] use unambiguously colored gloves to improve results. Other popular techniques rely on the use of specialized equipment such as wired data-gloves and accelerometers [Kadous 1996[START_REF] Fang | [END_REF],

sometimes also paired with cameras [START_REF] Brashear | [END_REF]], which can obtain accurate tracking data by design. Works like the one presented by [Lu 2010] use state-of-the-art motion capture technology to obtain tracking information of hands, body, head and even eye motion. Finally, some corpora have been created with 3D motion sensing devices like the Kinect [START_REF] Zafrulla | [END_REF], Stefanov 2013], which can give enough information to find the hands and head without markings.

Novell unmarked methods like [START_REF] Buehler | [END_REF]], try to also avoid specialized equipment.

In their work, the authors use a geometrical model to determine where the hands and head should be, based on the form of the human body. Broadly, a geometrical model of the human body is overlaid into each frame. From there, an algorithm calculates the probability of blobs of similar color of being part of any of six body parts defined by the model (hand, arm, shoulder, etc.); blobs are determined by a measure of color proximity, not linked to any particular tone. Based on this process blobs obtain a label, which is checked dynamically against previous calculations to improve accuracy. A different proximity measure is obtained between images, in order to optimize comparisons; in very similar images, the algorithm will check only the subset of information that has changed. The continuous application of the algorithm, permits inferring position changes with high accuracy. The main advantage of this method with respect to others is its overall robustness, as it can be applied to treat videos created under very different conditions [START_REF] Buehler | [END_REF]].

Articulator classification and hand position tracking serve as the basis for more complex treatment. It is at this point that the difficulty of the task increases, as it is necessary to automatically find other less evident parameters. From these, the detection of handconfigurations has gained traction over the years; however, it has proven to be one of the most challenging. This is mostly due to the deformable nature of the hands [Vogler 2004],

which can complicate the task. In addition, variations between configurations can be minimal, to the point of being nearly indistinguishable: for example, the configurations shown in Figure 3.15 only differ on the flexion of the index finger and thumb, which is enough to mark a difference between the two. Authors like [START_REF] Erenshteyn | A Multi-Stage Approach To Fingerspelling And Gesture Recognition[END_REF]] have tried to address these problems by creating a classification hierarchy for SL video-frames, prioritizing some classificators with respect to the others. In this view, classes are subdivided into small groups of simple classificators.

Also, each classificator can be part of more than one classes. To determine its class, each sample is tested by each classificator, and the results are combined into a single score. Classificators are tested following their order of importance on the classification hierarchy. After each pass, the score is compared against an optimality criterion, to determine if further tests are required or if the sample can be classified within a certain confidence interval. In this manner, only a subset of the possible classificators is always tested, improving classification times overall.

10. Images obtained from [START_REF] Companys | LSF : Dictionnaire visuel bilingue[END_REF]].

On the same vein, efforts like the one presented by [START_REF] Munib | [END_REF]] use neural networks [START_REF] Hagan | [END_REF]] to achieve classification over unmarked images. This method is based on specializing sets of neurons to recognize minimal properties present on the parameters.

Thereafter, the topology of the network can be used to combine the results of individual neurons, essentially following the same strategy as the previous example. However, in both cases having reliable training data is essential, and the quality of the input images can always become an issue. For this reason, similar to what happens with position tracking, several research projects rely on sensors to improve the quality of data from capture [Takahashi 1991,Kadous 1996[START_REF] Liang | [END_REF]], which improves accuracy and reduces calculation times.

Segmental feature recognition

Some research projects avoid the recognition of isolated parameters altogether, and treat the problem from a morphologic perspective; this is, they classify entire postures, trying to identify sign components instead of individual parametric variations. One of the main advantages of these techniques, is that additional linguistic information can be used to improve recognition conditions; for instance, it may be easier to discard noisy video segments by catching meaningless postures [START_REF] Gonzalez | [END_REF]], or to isolate important gestures [START_REF] Nam | Recognition of Space-Time Hand-Gestures using Hidden Markov Model[END_REF]] such as pointing [START_REF] Nickel | Pointing Gesture Recognition Based on 3D-tracking of Face, Hands and Head Orientation[END_REF]]. It turn, this can also help to develop higher level recognition tasks, which could also benefit from SL sequential characteristics to improve accuracy [Vogler 1997].

A lot of the projects developed under these assumptions use Hidden Markov Models (HMMs) [START_REF] Stamp | A revealing introduction to hidden Markov models[END_REF]] for their machine learning tasks; roughly, a HMM represents a probability distribution over a sequence of independent observations of some process.

Usually, HMMs are represented as graphs, where each transition is labeled with the independent probability of changing from one state to another. The model is based on the assumption that there are states hidden from the observer, and these can be inferred from observations so as to predict the future of the represented process. Due to their flexibility, they are frequently used to model time series data such as video recognition, computational biology, data compression and others.

Works based on classic HMMs and the like usually avoid tracking, as they intend to work directly over unmarked corpus images. For example, the authors [START_REF] Cooper | [END_REF]] encode simultaneous parametric information into two independent classes: static features and movements. The system then analyzes raw video data, and classifies frame sequences into one of the two classes. Each found sequence is characterized by its own feature vector, regardless of the class it was classified into. To prove the utility of their approach, a lexical sign database was created describing each sign's formation; as with video sections, each of the sign's segments are characterized by a vector, enabling the development of distance measures to determine how close detected postures are from predefined ones.

Finally, these measures can be used as input for morphologic Markov chain, enabling sign recognition.

Despite its advantages, the usefulness of the aforementioned method is limited by the quantity of training samples available (see Chapter 1, Subsection 1.1.2.2, p. 9). In addition, linguistic variations and the need to introduce more or less parameters to the model forces the creation of several HMMs for the same segment, limiting scalability.

A similar technique was used by [START_REF] Brashear | [END_REF]], where the authors describe individual signs by way of HMMs. In general, each signs' internal structure is implicitly captured by its corresponding HMM. This implies that longer signs will thus induce larger models.

Similarly as what happens with previous efforts, the lack of learning data limits both the creation and evaluation of the resulting models, forcing researchers to test their results over rather small sets of signs.

Works like [START_REF] Vogler | [END_REF], Vogler 2004] have tried to improve scalability by considering modalities as independent channels, on their own variation of HMMs. As a result, the system can do dynamic addition and removal of parameters to the model during recognition, which both improves the framework's flexibility and performance. In some ways, their approach works as a mixture of posture-based and parameter-based recognition, as this makes possible the definition of single parameter lexemes, among others. The authors base their framework on the phonological model by [START_REF] Liddell | [END_REF]];

in this sense, the use of knowledge on sign structure helps them reduce computation times, by exploiting techniques reminiscent of hierarchical classification.

Approaches like the ones tried by [START_REF] Ma | [END_REF][START_REF] Liu | [END_REF]], attempt to integrate NMFs to the recognition process, as a way to make sense of data as a whole rather than concentrating on individual parameters.

Other projects generalize the same principle, in an effort to obtain more information about a posture's intention; for example, [Green 2004] present an architecture to track human body movements, for biometric analysis. In the article, the authors use both a particle filter and HMM to reduce computation times and improve accuracy. Articles like [Bauer 2002b], explore the idea considering variations on technology, and the general problem of subdividing SLs signs in segments. Finally, projects like [START_REF] Gonzalez | [END_REF] explore the use of low-level tracking-data to calculate automatically a proposed sign segmentation, in an effort to remove co-articulations from video data in annotation tasks.

Individual sign recognition

In this kind of recognition tasks, it is common to have two distinct classification phases:

1. sub-lexical recognition, either of individual parameters or segmental features;

2. sign classification.

Due to the bottom-up approach adopted by the domain, the hit and miss ratio of sub-lexical feature recognition from the first phase will necessarily impact the accuracy of sign classification as a whole [START_REF] Waldron | [END_REF][START_REF] Brashear | [END_REF][START_REF] Cooper | [END_REF].

The application of this type of hierarchical philosophy, inevitably limits the capabilities of recognition tasks from a technological point of view: each level could theoretically impose new restrictions on data, which in turn could reduce the amount of exploitable information.

For example, calculation-heavy parameter recognition based on particle filtering [START_REF] Lefebvre-Albaret | [END_REF],Gonzalez 2011], may not escalate well for real-time processing, which would immediately discard some of the existing data sources, developed to be treated under this technique. In addition, this approach is also prone to suffer from cascading failures, carrying erroneous data from lower to higher levels, and limiting usability. Both these technological limits, and the existence of different research objectives, has separated the field into two distinct areas: isolated and continuous sign recognition.

As its name implies, isolated sign recognition studies how to recognize individual apparition of signs [Grobel 1997]; in general, research in the area centers around the identification of single signs in very well-delimited contexts. This could be useful in different situations such as Deaf machine interaction [START_REF] Heloir | [END_REF]], the search of signs by signing on visual data repositories [Elliott 2012], the creation of software solutions for SL education [Stefanov 2013], and even to enable simple signing access to new technologies [START_REF] Fotinea | [END_REF]]. Most of the aforementioned projects, rely on the study of specific use-cases, where sign delimitation is almost always a given, and where the quantity of possible signs to recognize is limited.

On the other hand, continuous recognition tries to identify sign apparitions over unbounded contexts. This can be useful for projects related to the identification of phrases [START_REF] Chai | [END_REF]], discourse analysis [Bauer 2002a[START_REF] Nayak | [END_REF], or for the recognition of complex linguistic phenomena [Kelly 2009].

Contrary to what happens on isolation, continuous recognition has to work over very unstable environments, where the system is obliged to independently find cues leading to the segmental subdivision of the utterance [Bauer 2002b]. Notably, most of the existing projects on the area work by chaining HMMs; that is, they first create smaller HMMs for individual sign identification, and the result serves as input for a morpheme-level

HMMs [START_REF] Ong | [END_REF]]. However, these kind of approaches can be difficult to develop, because of the lack of both enough training data or linguistic knowledge to create the models.

These limitations, alongside the hierarchical structure, end up translating into very reduced sets of recognizable signs, as exemplified by Table 3.1.

Authors

Type of Recognition

Technique

Qty. of Signs For comparison, projects in continuous speech recognition are capable of recognizing sets of more than 1000 words using similar techniques [START_REF] Roth | [END_REF]], even in very limited conditions. This is of particular interest for the domain, as the existing data resources are not only limited but very heterogeneous, as it will be explained in the next section.

Notable Sign Language Research Resources

Various corpora for research have been developed over the years, with special emphasis on linguistics rather than computer-friendliness. One of the main characteristics of these corpora, is that they try to capture as many different variants of the language as possible. In general, this differs from the current approaches used by computerbased SL research, where ideal "standardized" language samples have been preferred [START_REF] Morrissey | [END_REF][START_REF] Forster | [END_REF]. This is because, as mentioned in previous sections, the existence of variation can affect evaluation results on both synthesis and recognition tasks.

As such, classic linguistic corpora pose different challenges to researchers who wish to use them as data sources, as they depict data in far from ideal conditions for automatic processing. Regardless, they remain prominent data sources for computer-based research, due to their relatively high availability.

For example, [Crasborn 2008c] present the authors' efforts to record a corpus for the Sign Language of the Netherlands (NGT). For their project, the research team collected samples from 100 native signers, coming from different backgrounds and regions. The participants were tasked with signing narratives, using popular culture bits as elicitation materials (cartoons, comic stories, TV videos, etc). Other tasks included discussions around SL issues and even free conversation. From a technological point of view, the corpus was captured using four High Definition cameras, located around the signers as shown on Figure 3.16. The project resulted in around 80 hours of video data, available for its consultation over the web. Some annotations and translations were made for some of the videos, however budget and time limitations didn't let researchers annotate everything nor give very detailed glosses. In any case, the work resulted in the development of new software for on-line collaboration [START_REF] Brugman | [END_REF]], and on the integration of new annotation capabilities to the ELAN platform [Crasborn 2008a].

It is common for long-term corpus projects to develop their own capture standards, which can vary depending on the size and scope of the project. Because of this, corpora has been built upon tools as diverse as professional video cameras [START_REF] Hanke | [END_REF][START_REF] Schembri | [END_REF], motion capture equipment [Cox 2002,Lu 2010], televised SL transmissions [START_REF] Buehler | [END_REF]],

or even with new emerging hardware technologies [Stefanov 2013]. Similarly, these projects frequently develop their own annotation tools, which usually implement their own standards. As such, big corpus projects have influenced the development of new annotation formats, as it is common for their auxiliary tools to become available to the research community. This availability has influenced the design principles of new, smaller corpora; for instance, authors [Karpouzis 2007, p. 6] express their choice of HamNoSys annotations, because of their compatibility with the ELAN platform.

One of the biggest SL linguistic data repositories to date is the DSG Corpus Project [START_REF] Hanke | [END_REF]]. For its creation, 300 signers from around 12 different regions were selected, in an effort to capture as much linguistic variations as possible. Being a long-term project, DSG managed to amass over 500 hours of video samples, showing approximately 3 million different signs. However, only a fraction of the materials are freely available [Nishio 2010], and not all videos are annotated; only 18 sessions out of 3 regions have annotations.

An specialized software platform called iLex [Hanke 2002] was used for its annotation.

In particular, this tool permits the expression of annotations as either glosses or as HamNoSys descriptions.

With respect to capture, the corpus was recorded by pairs of signers with the help of three HD cameras: two to capture each signers' frontal plane, and the last one recording the complete scene. Figure 3.17 shows a shot of the camera setup. This same setup was used for the Dicta-Sign corpus, presented by [START_REF] Matthes | [END_REF]]. This project consisted in creating a compilation of annotated corpora from four different European SLs (BSL, DSG, GSL and LSF). Data of the four languages was recorded in parallel, using the same elicitation materials and a lexicon of more than 1000 signs.

Despite of the corpora being elicited to reflect common use of SLs, Dicta-Sign was created with the intention of serving as input data to develop computer-based research. For this reason, special emphasis was put on creating computer readable annotations, that could be used to interpret data automatically.

Elicitation tasks for each corpus were performed by groups of 16 native signers, paired together into sessions of around two hours [START_REF] Hanke | [END_REF][START_REF] Fotinea | [END_REF][START_REF] Matthes | [END_REF].

From the resulting raw video, at least 5 hours of lexical gloss annotations were created, summing up to 25 hours of annotated corpus-data. Annotations were created with the help of the iLex platform, following the same guidelines across the four corpora. Some variations in annotation do exist, however, due to personal choices of the teams creating each corpus.

As with other projects of similar size, new software tools oriented towards annotation were created as part of the project. Contrary to previously existing software, the approach taken by Dicta-Sign relies on the integration of classic multimodal annotators with specialized SL software modules, following the guidelines introduced by [START_REF] Braffort | [END_REF]].

The main idea is that, by way of these modules, human annotators can collaborate remotely [Collet 2010[START_REF] Dubot | Improvements of the Distributed Architecture for Assisted Annotation of video corpora (poster)[END_REF], or can introduce recognition capabilities that could potentially simplify the annotation task [START_REF] Gonzalez | [END_REF]]. In a final note, smaller corpus projects are starting to take advantage of the byproducts of larger ventures; researchers in linguistics begin to acknowledge the importance of computer-based tools for corpus analysis, even in purely linguistic research [Leeson 2006].

Indeed, the literature shows that the vast majority of new linguistic SL corpora are systematically subject to some kind of automatic treatment. By the same token, corpora created exclusively for data-driven research have started delving deeper into linguistics [START_REF] Forster | [END_REF]], as linguistic knowledge is an important factor for the correctly interpretation of data. For these reasons, the development of new, more integrated, approaches towards corpus representation and annotation seem unavoidable, as it has become more evident than ever that neither purely mechanical nor purely linguistic aspects are sufficient on their own to understand SLs. Fortunately, computer science already fosters a set of procedures designed to treat similar issues, as they were created to match very technical problem descriptions with higher-level abstractions. In the literature, these techniques are usually referred as formal methods.

Formal Methods

The term formal methods, encompasses a group of mathematical techniques used to describe and test software or hardware systems, from conception to implementation [Wing 1990]. These are usually subdivided into two complementary areas:

Formal Specification Contains a series of formal notations used to characterize systems (specify), harnessing the power of several mathematical models.

Formal Verification It refers to the series of techniques that serve to test (verify)

formal specifications and their implementations, to assure that they conserve the desired properties.

Specification and verification are considered important tools to avoid pitfalls in the creation of complex systems; by introducing mathematical rigor, system designers can build coherent and unambiguous descriptions, which are both easier to understand and less likely to fail [START_REF] Bowen | [END_REF]]. However, despite their benefits, their penetration outside of the domain of critical systems remains lackluster at best, specially because of hurdles related to the both the usability of formal notations and other pragmatical issues [Knight 1997]. Regardless, some readily available solutions exists and have been central to the development of complex industrial processes in areas such like transportation [Hall 1996], micro-processor design [Bentley 2001] and energy production [Yoo 2008]. In the next sections, some of the existing work in the area will be presented, in an interest of showing the flexibility of formal notations and their applicability to various areas.

Formal Verification

The process of formal verification entails the analysis of a system's design, in order to determine if it satisfies certain properties [START_REF] Baier | [END_REF]]. This process can only take place if the system is defined formally; that is, if there is no ambiguity on its definition, and if there exist a well-defined set of consistent rules framing its inner workings. This makes the use of formal notations specially suitable for verification, which usually serves as a compelling argument to advocate for their use during system design [Holloway 1997].

There are two main techniques commonly used for verification: model-checking and automated theorem proving. The choice of one instead of the other depends largely on the specification formalism selected by the designer; however, mathematically speaking, both methods are equivalent [START_REF][END_REF]]. That said, model-checking is better adapted to verify systems represented as Labeled Transition Systems (LTSs) [Keller 1976, p. 372], whereas theorem proving methods tend to be favored for the verification of more symbolic representations [Chang 1997].

In general, model-checking algorithms are based on performing exhaustive searches for every possible state of a LTS, in an effort to find all possible errors on the system's specification [START_REF][END_REF]]. However, this methodology comes with the serious disadvantage that it has to deal with combinatorial explosion. Accordingly, model-checking algorithms are limited by tractability issues; this introduces the problem of determining if the verification of some description will be intractable, even before its creation. For this reason, research in model-checking has been focused on finding the limits of exhaustive verification [START_REF] Bauland | [END_REF]] and developing new stochastic methods to optimize performance even in the worst cases [START_REF] Kwiatkowska | [END_REF]].

On the other side of the spectrum, automated theorem provers try to tackle intractability by avoiding the systematic search of every possible state. To this end, these tools make use of different proof calculi to determine if a specification is valid, obtaining proofs by the strategic application of a finite set of inference rules [Chang 1997]. Specifications verified under this method, usually have to provide both a set of axioms modeling the system's invariants and a set of properties to prove; from there, the inference engine will try to find a formal proof asserting to show that the system fulfills each property, in order to determine the correctness of the specification.

Theorem proving is limited by decidability issues; for most formal systems, no algorithm exist to prove that some statement is true or false in the system [Davis 1958]. For this reason, some of the existent research on formal methods deals with proving the decidability of description formalisms; in practice, this results in the creation of less expressive descriptions, albeit automatically verifiable.

Formal Specification

A formal specification is a mathematical description created to capture, unambiguously, the inner workings of a system. They are written by way of very specialized notation languages, emanated from within various disciplines of mathematics.

Traditionally, formal notations have been inspired on logic, graph theory or algebra, depending on their intended use. In practice, the choice of one formalisms with respect to the others corresponds to the description needs of the system's designer; in this regard, the choice of which formalism to use and how, becomes part of the specifier's tasks, mostly depending on the problem and the purpose of the specification. For instance, in software development, designers can either use Z-notation [START_REF] Woodcock | [END_REF]] to characterize the interaction of an entire system, or they can go with Larch [Guttag 1993] to describe on an abstract level how the most basic components work. As such, it is not uncommon for specification languages to share similar expressive capabilities, since they have to show some degree of flexibility in order to adjust to the different possible use-cases.

Formal specification notations have been traditionally grouped into classes, semantically related to their underlying mathematical basis; the most relevant, for this scope of thesis, are listed below:

-model-based;

-algebraic; -process-oriented.

For the most part, this classification is fairly subjective, as some formalisms could fit in more than one category. In the next sections, some examples of each listed type will be analyzed, as well as their overall relevance in terms of this work.

Model-based specification

Model-based specifications are built upon concepts of set theory [Jones 1980]. As such, notations in this category will let designers describe information in terms of sets and relations between them; normally, operations are defined as mappings from one set into another. System invariants or semantic rules linked to set definitions, are usually described with predicates of first order logic. This enables the depiction of systems as complex mathematical structures, like LTSs. An example of this can be seen in figure Figure 3.19, built on Z-notation [START_REF] Woodcock | [END_REF]] and taken from [Jacky 1996]. This kind of description specifying system functions as maps between sets, can be useful to verify implementations, independently of the technical details behind each state or transition. A high level verification tool could, for example, check each operation by asserting that their results are members of the appropriate sets. In this way, it is possible to isolate the model from its implementations, enabling verification for all of them.

Other popular formalism relying on the same principles is the Vienna Development Method (VDM) [Jones 1990]. The VDM specification language uses types as primitives, which are none other than sets over specific domains. Both the Z-notation and VDM have been readily used in industrial applications with success [START_REF] Craigen | [END_REF]], and continue their evolution with respect to their use-cases in industry; however, other less industry-friendly theoretic formalisms are abound, exploring similar issues from a rather symbolic point of view. Such is the case of algebraic notations.

Algebraic specification

Algebraic specification notations represent systems in a more basic level than previously reviewed formalisms; they represent the inner workings of a system as algebraic structures.

This is done by way of abstractions like the ones used by VDM, where every piece of data has an associated Abstract Data Type (ADT), defined only over a specific set of values. However, unlike model-theoretic specification languages, algebraic notations are designed to express systems in more general terms, semantically closer to mathematics than to the actual implementation [START_REF] Guttag | [END_REF]].

ADTs are composed of two main parts:

-The signature of each one of its operations, defined recursively in terms of the given types.

-A set of axioms describing the semantics of these operators.

An example of an ADT is presented in Figures In general, just as with VDM, operators are defined in terms of maps between sets. 1. MEMBER OF? (EMPTY SET, i)=false 2. MEMBER OF? (INSERT(s, i), i ′ )=if ?=?(i, i ′ ) then true else MEMBER OF?(s, i ′ ) 3. DELETE (EMPTY SET, i)=EMPTY SET 4. DELETE (INSERT(s,i) The axiomatic specification serves as high level abstraction of what it means, in terms of set transformations, to insert, delete or be a member of Set.

, i ′ )=if ?=?(i, i ′ ) then DELETE(s, i) else INSERT(DELETE(s, i ′ ), i)
The flexibility of ADTs and their symbolic description approach, has permitted the creation of the Larch notation [Guttag 1993], which can be tailored to interface with different programming languages and to specify very specialized behaviors, such as the ones found in concurrent systems [Lamport 1989].

Process-oriented specification

Process-oriented specifications are mainly focused on how a system reacts. As such, these notations usually give the designers the means to create abstract descriptions of a system's evolution [START_REF] Winstanley | [END_REF]]. Notably, the interpretation of process-oriented descriptions is usually done over LTSs.

A lot of the process-oriented formalisms are used to specify concurrent systems; for this reason, most of the existing notations have evolved to be able to represent characteristics such as message-passing and parallelism [Pierce 1995]. It is also common for this kind of tools to formalize concepts such as channels, and to define groups of indivisible communication primitives that the processes can execute non-deterministically.

Notations like Calculus of Communicating Systems (CCS), developed by [Milner 1982],

captures the behavior of concurrent systems by combining processes recursively as defined by the Backus Normal Form (BNF) shown below:

Definition 3.1 (Process in CCS).

P ::= ∅ | a.P 1 | A | P 1 + P 2 | P 1 |P 2 | P 1 [b/a] | P 1 \a
where:

-∅ denotes the empty process.

a.P 1 indicates that a process executes action a and continues as P 1

-A is an identifier representing a primitive process.

-P 1 + P 2 means that either P 1 or P 2 continues.

-P 1 |P 2 indicates that processes P 1 and P 2 exist simultaneously.

-P 1 [b/a] denotes the process P 1 where all actions a are renamed as b.

-P 1 \a Represents the process P 1 without action a.

In this specification language, actions can represent any possible communication primitive needed by the designer to describe the system, and are defined depending on the specific use-case.

Communicating Sequential Processes (CSP) is another formalism working under similar assumptions. Originally presented by [Hoare 1985], CSP follows the same basic model than CCS: it describes primitive events and processes to represent the particulars of a system's functionalities. From there, the description of more complex functions is done recursively, by way of a the group of logic operators presented below. a → P is the process which, after event a, behaves as P .

-P Q denotes the process where either P or Q are executed.

-P ⊓ Q denotes the process where either P or Q are executed, non-deterministically.

-P |||Q is an interleaving process, where P and Q exist simultaneously.

-P ||{a}||Q is a synchronized interleaving, where a must occur in both P and Q before parallel execution.

-P \{a} is a process resulting of removing event a from P .

Finally, the Propositional Dynamic Logic (PDL) captures similar process-oriented properties, centering around sequentiality rather than concurrence. PDL is a multimodal 11 logic [Chellas 1980], first defined by [START_REF] Fischer | [END_REF]] to characterize computer programs.

Originally, it provided a formal framework for program description, allowing them to be interpreted as modal operators. The syntax of PDL is given below: Definition 3.3 (Syntax of PDL). Let α denote a program and ϕ a PDL formula.

α ::= π | α; α | α ∪ α | α * | ϕ? ϕ ::= ⊤ | p | ¬ϕ | ϕ ∧ ϕ | [α]ϕ
where:

π denotes an atomic program.

p denotes an atomic proposition.

α; α indicates the sequential execution of two programs.

α ∪ α is the non-deterministic choice between two programs.

α * means that program α is executed a finite, non-deterministic number of times.

ϕ? is the program that fails if ϕ is false.

-[α]ϕ indicates that, after executing program α, the system necessarily enters into a state where ϕ is true.

11. The term modality has different meanings in semiotics and formal logic. While in the former it has been previously defined as akin to a communication channel (see p. 28), in the latter it refers to the qualification of a statement in terms of "necessary" and "contingent" truths. In this regard, a logic is multimodal if more than one qualifiers are available.

In PDL, system properties are described as formulae and, as it's common with other modal logics, its semantics are interpreted by way of LTSs.

Several variations of the logic exist, with different repercussions over its decidability.

However, the basic version presented in Definition 3.3 features an optimal model-checking algorithm [Lange 2006], and it has been proved decidable [Danecki 1985].

Other process-oriented formalisms are explored in detail on the literature [Winskel 1995],

where different tools have been developed to enable specification and automatic verification of concurrent systems. In this regard, the area has provides a basis to attempt the formalization of SL production rules as transition systems: it has developed specification languages, capable of expressing simultaneous behaviors between independent agents and their temporal properties. These are desirable characteristics for the modeling of SL morphology, in particular when depicting how articulators act independently but, nevertheless, synchronize to generate meaning. In addition, these notations are designed around their expressiveness -their capacity to represent information -and, thus, are broad enough to describe SL utterances in different situations. In this way, they are capable of producing linguistic annotations which can be enhanced with technical information about any given corpus, something that can be useful in the automatic analysis of SL corpora, as presented in the next chapters.

Chapter conclusion

In this chapter, some of the most common SL representation formalisms were introduced, alongside some of their applications in research. In addition, a brief overview on SL synthesis and recognition was given, as well as a general introduction to formal methods.

As shown on the chapter, some of the most common problems in research and representation, come from SLs multimodal nature. This not only increases the complexity of synthesis and recognition tasks, but also affects the availability of copora due to the variety of technologies used to deal with multimodality. This prompts for the search of new representation methods that could help unify the current heterogeneous environment under a common meta-language, friendly not only for linguistics but also for very technical tasks.

It is on this context, that this thesis presents its main contributions. The idea, was to develop a flexible phonetic representation framework, capable of specifying articulation parameters in a way similar to what SiGML and the Stokoe notation do. Additionally, even though the proposed framework is strictly phonetic, it was built under the assumption that it would eventually be extended to represent morphological SL properties. With this in mind, the framework provides a broad set of tools intended to go beyond phonetic description in the future, akin to what Zebedee has done with AZee [Filhol 2012b]; the main assumption being that a flexible phonetic basis, can lead to higher level descriptions.

In the next chapter, a new SL phonetic representation method is presented, based on the principles of formal methods; even though specification notations have been heavily influenced by industrial applications, the same principles can be applied to academic research. For instance, linguistics have a rich history of developing formalisms for the study of natural language [START_REF] Chomsky | Noam Chomsky. Syntactic structures[END_REF][START_REF] Pullum | [END_REF][START_REF] Moss | [END_REF]], which has contributed on the theoretical development of the area. In particular, the proposed formalism is modeled on the PDL, also reviewed in the chapter, a logic created to represent change.

Chapter 4

Formal Specification of Sign

Language Utterances

The previous chapter presented a series of formal specification languages, striving to thoroughly describe complex systems (see Subsection 3.4,p. 67). By way of these notations, system designers can build abstract representations of a system's inner workings, so as to better understand and test its limits. Sign Languages (SLs) lend themselves to the same kind of formalization: they can be seen as complex transition-based systems (see Subsection 2.2.1.4, p. 29), able to produce phonetic change by applying per-articulator rules of change.

Recall from previous chapters that computer-based SL study is plagued by several problems deterring the development of the domain:

-the fact that SL corpora are collections of non-textual data, forcing Natural Language Processing (NLP) algorithms use uncommon data -such as video images -as input;

-the variability of corpus-data, impeding the creation of vast language information repositories such as the ones existing for the study of vocal languages; and, -the difficulty to annotate these corpora, taking into account both that annotation tasks are also very variable, and that there is a limited availability of SL experts able to create and correct annotations.

In this regard, using formal specification techniques to convert corpora into abstract representations may prove useful, as these abstractions may be used to tackle variability; in addition, they provide a more computer-friendly representation of raw data, which can contribute towards the development of automatic recognition and, crucially, annotation algorithms.

Previous formalization approaches to language study have been developed before [START_REF] Chomsky | Noam Chomsky. Syntactic structures[END_REF][START_REF] Pullum | [END_REF][START_REF] Moss | [END_REF]], a practice which has also extended to SLs (see Section 3.1, p. 42). However, these efforts continue to be limited by spatial and multimodal representation issues.

With this in mind, this chapter presents a formalism for SL utterance modeling inspired on the Propositional Dynamic Logic (PDL) (see Section 3.4.2.3,p. 74). PDL is a process oriented specification language, centered around sequential modalities. The idea was to extend on this notion to express SL phonetics in similar terms, by linking logical modalities to articulatory actions and depicting how these can foster change. This resulted in the creation of the Propositional Dynamic Logic for Sign Language (PDL SL ), which provides a flexible representation of SL multimodality (see Subsection 2.2.1.3, p. 28), paired with a formal notation to express properties over modeled utterances.

Together, these tools can help an automatic system to semi-automatically find phonetic properties in a visual corpus, just by ensuring a minimal description of each video by way of the formal structure provided by PDL SL . Globally, the quantity of information that needs to be described is largely decided by the human annotator, who ends up fulfilling the role akin to system designer in industrial applications.

The advantage of using PDL SL as a vehicle for the construction of an automatic system, is that it can serve as an intermediate language between computer science and linguistics, minimizing common pitfalls present in other representation languages which tend to favor either one side or the other. For the same reason, this formalism intents to be compatible with other SL phonological representation notations, in the sense that it aims to be capable of capturing at least the same information as the others.

Because of this, PDL SL is defined in somewhat broad terms; its objective is not to represent specific parametric configurations, but rather to give a flexible enough framework to represent as many phonetic combinations as possible, in an effort to remain language and corpus agnostic. Due to the combinatorial nature of SL phonemes, this has to be done by defining everything in terms of sets, akin to the definition of types in model-theoretic formalisms (see Subsection 3.4.2.1, p. 69). In particular, this can also help PDL SL to supersede existing transcription notations in automatic tasks, as they are capable of representing (at least) the same information. However, unlike model-theoretic tools, PDL SL types are predefined by the formalism itself, as presented in the following pages.

In the next section, some basic model-theoretic definitions are given to the reader, in order to establish the representation domain of the proposed formalism. Short after, in the following section, the logic's syntax is provided, mimicking the traditional logic-definition mechanism in the literature. Finally, the last section presents the language semantics; that is, how formulae built with this logic are to be interpreted, related to an abstract SL corpus representation.

Sign Language Primitives

Like previously mentioned, PDL SL enables the definition of type primitives in the same fashion as model-theoretic formalisms, which is helpful to establish limits on what information an annotator can specify; however, instead of forcing the experts to define these types, PDL SL simplifies the task by introducing a series of semantically-motivated set templates, which can be populated by the annotators with the information they deem relevant. The objective of these templates is to provide PDL SL with a powerful enough basis to be, at least, as expressive as other phonetic transcription notation (see Chapter 6, p. 129).

That being said, the set definitions introduced in the next paragraphs are based on existing parametric descriptions of SL phonemes (see Section 3.1, p. 42). In particular, the interest of PDL SL sets is to ascertain well defined concepts (like hand-shapes or locations), as classes containing concrete objects. For this reason, set members will correspond to observable characteristics; for example, the set of hand-shapes will contain every meaningful morphological configuration of a hand. When combined into more complex sets, these primitives serve to define atomic statements, which will in turn operate as seeds of phonetic formal descriptions.

First of all, PDL SL works under the assumption that each articulator is an independent agent, inducing individual information channels (see Subsection 2.2.1.3, p. 28) as the ones proposed by [START_REF] Vogler | [END_REF]]; for this reason, it is first necessary to define who these agents are, in terms of the relevant body parts used in SL communication. As with BODY, the articulator set is defined in very general terms, in order to adapt to any possible linguistic characterization that may affect the definition of articulators themselves. This is, ART will contain anything that annotators consider an articulator.

Regardless, more often than not the hands will be in ART , an thus PDL SL assigns specific symbols to denote them: R and L for the right and left hands, respectively.

In general, articulation is dependent on the morphological characteristics of articulators themselves (see Subsection 2.2.1.1, p. 26). For this reason, PDL SL defines places of articulation in terms of the individual articulators that can use them, as each will have their own articulation capabilities. To this end, it is also useful to have a characterization for the signing space, as sometimes space locations around the signer are used to articulate (see Subsection 2.2.1.1, p. 27). Let C : 2 ΨSL → N AMES be a function assigning labels to spatial coordinates, and Ψ a SL ⊂ Ψ SL be the set containing any spatial coordinate where a can articulate during signing. The set LOC a , denoting places of articulation for a, is defined as follows:

LOC a = {λ : λ ∈ (BODY a ∪ C(Ψ a SL ))}
Additionally, LOC is defined as the set containing all possible pairings of valid articulators and articulation places LOC = {(a, λ) : a ∈ ART and λ ∈ LOC a }.

In some cases, Non-Manual Features (NMFs) may change without referring to any external location (see Subsection 2.2.1.2, p. 28). To this end, the proposed formalism permits the definition of partial articulations in terms of configuration change. This is done simply by leaving the location set of the pertinent articulator empty, indicating that its changes will never refer to any location. So, for example, if a ∈ ART refers to the eyebrows, then it is most likely the case that LOC a = ∅, as there are almost no instances (if any) where the eyebrows refer to a place of articulation.

It is relevant to mention that these location-less partial articulations appear because of the channel separation, induced by the definitions. Intuitively, the formalism models an articulation as a composition of independent articulatory changes, each having the same "value" as a complete articulation. For this reason, to maintain consistency articulation places are described in terms of the articulators that may refer to them.

Similar to what happens with places of articulation, configurations will depend completely on the characteristics of their corresponding articulator: for instance, hand shapes will be exclusively held by the hands, while each NMF will have its own set of valid configurations Location and configuration traits alone are not enough to characterize SL utterances;

in order to give a more complete depiction of language, concepts linked to spatial relationships such as position, movement and distance have to be taken in account. This will be done mainly by way of direction vectors, which are defined below. By itself, the set ∆ holds no particular meaning whatsoever, as it is for the annotator to determine the relevance of directions himself. In general, this can be done by classifying vectors under more meaningful classes such like "LEFT" or "RIGHT". To this end, it is useful to introduce a labeling function taking groups of vectors to names, which will serve to characterize spatial concepts over the coordinate system induced by Ψ SL .

∆ SL = {v : v ∈ 2 ∆ and there is a name t ∈ L ∆ (v)}
Notably, v ∈ ∆ SL denotes a vector family identified by a name in DIRECT ION S.

Intuitively, the set in Definition 4.8 contains only the vector families defined over L ∆ , the labeling function from Definition 4.7; in this way, if definitions for LEFT, RIGHT ∈ DIRECT ION S exist in L ∆ , the group of vectors giving meaning to these names will be in ∆ SL . This enables annotators to separate geometric information from spatial concepts, thus permitting him to work with words like LEFT and RIGHT instead of defining groups of vectors.

These initial definitions are but the building blocks of representation; they are intended to be combined with each other, in order to describe more complex relationships. This combination is achieved by way of the PDL SL grammar, which is presented in the next section.

Syntax

The previously defined primitives, serve the purpose of providing some semantic information about posture parameters before characterizing postures themselves; to properly represent these, it is necessary to give statements, declare information about them that can be proven true or false. Roughly, the idea is that each statement will represent individual information pieces about articulators, and postures will be none other than the combination of several of these pieces. As such, it is useful to formally define these statements as atomic propositions, like shown in Definition 4.9.

Definition 4.9 (Atomic Propositions for SL Body Articulators). Let a ∈ ART be an articulator. The set Φ a , containing the atomic propositions for articulator a, is defined as follows:

Φ a = {p a : p a asserts information about the articulator named by a ∈ ART } Also, for every articulator a ∈ ART , there exists a proposition any a ∈ Φ a denoting that articulator a doesn't move.

The set of all possible atomic propositions is defined as follows:

Φ = a∈ART Φ a
The propositions defined in set Φ, are intended to characterize phonetic parameters; that is, they strive to assert propositional information about Holds in the Movement-Hold Model (MHM) phonological model (see Chapter 2, Subsection 2.2.1. 4,29). In a similar fashion, Movements will be characterized independently, by a set denoting actions.

Definition 4.10 (Atomic Actions for SL Body Articulators). Let a ∈ ART be an articulator. The set Π a of atomic actions for articulator a, is defined as:

Π a = {π a : π a asserts a change in articulator a ∈ ART }

In addition, for every articulator a ∈ ART , there exists an atomic action skip a ∈ Π a denoting that articulator a performs any action.

Finally, the set of all possible atomic actions is defined as follows:

Π = a∈ART Π a
It is important to underline that members of both sets, Φ and Π, are statements; that is, each member can be labeled as true or false, as specified by PDL SL semantics (see Section 4.3). This makes it possible to combine multiple statements into more complex phonological structures, starting with actions.

Definition 4.11 (Action Language for SL Body Articulators A SL ). The action language for SL body articulators (A SL ) is given by the following rule:

α ::= π a | α ∩ α | α ∪ α | α; α
where π a ∈ Π.

Intuitively:

-π a is an atomic action for some articulator a ∈ ART ;

-α ∩ α indicates the concurrent execution of two actions;

-α ∪ α is used to depict two non-deterministically occurring actions;

-α; α describes a sequence of two actions; and, Definition 4.11, presents the PDL SL action language as a Backus Normal Form (BNF) grammar; the operations depicted, intend to give the annotator the flexibility to combine various atomic actions into a single Movement, to describe complex phonological changes.

For instance, it permits describing situations where two hands move simultaneously, where a signer repeats an action an unbounded sequence of times or even if there might be more than one valid changes in the same interval. The resulting formulae can further be "glued" with Hold representations by way of the PDL SL language, defined below.

Definition 4.12 (Language PDL SL ). The language PDL SL is generated by the following rule:

ϕ ::= ⊤ | p a | ¬ϕ | ϕ ∧ ϕ | α ϕ | α ∧ ϕ ϕ | ϕ; α ϕ
where p a ∈ Φ, α ∈ A SL .

Intuitively:

-⊤ represents a logical true value;

-p a is an atomic proposition for articulator a ∈ ART ;

-¬ϕ represents the negation of formula ϕ;

-ϕ ∧ ϕ denotes conjunction;

-α ϕ describes that, after execution of action α, ϕ holds;

-α ∧ ϕ ϕ models situations where an action α and an static feature ϕ occur simultaneously until converging into some other static feature; and, -ϕ; α ϕ denotes that, if some ϕ holds, then a modal formula holds afterwards.

Just as A SL enables the construction of more complex Movements, the language PDL SL permits the integration of groups of atomic propositions into Holds. In addition, it provides operations like α ϕ to think in terms of sequences of Movements and Holds, giving way to the description of phonological structures. In this regard, PDL SL differs from PDL on the interpretation of modal operators, as PDL SL is essentially constrained by the possible phonetic sequences occurring in the studied SL. As a result, PDL SL formulae will be interpreted over a mathematical representation of SL utterances, designed to capture the effects of multimodal articulation; the interpretation rules, and the proposed utterance representation, are introduced in the next section.

Semantics

In the spirit of the possible worlds model introduced by [Hintikka 1962], formulae in the PDL SL language are interpreted mostly over Labeled Transition Systems (LTSs); however, concurrent operators will hold meaning only over more complex structures. In the case of SLs, this representation will reflect the possible morphological states signers can assume, depending on how they configure their articulation parameters during signing. But first, to know which state changes are valid in a determined SL, it is necessary to define an -S is a non-empty set of states -R is a transition relation R ⊆ S × S where, for every s ∈ S, there exists a state s ′ ∈ S such that (s, s ′ ) ∈ R. Furthermore, it can be the case that s = s ′ .

-• Φ a : S → 2 Φ a , denotes the function mapping states to a set of atomic propositions giving information about articulator a. Notably, for states s, s ′ ∈ S, if

s Φ a ≡ s ′ Φ a , then s ≡ s ′ . -• Π a : R → 2 Π a ,
denotes the function mapping binary relations to groups of atomic actions for articulator a.

It is implicit from the definition that each articulator has its own model, in order to reflect changes in individual articulators rather than on entire postures. Parametric information is provided by the labeling functions, • Φ a and • Π a , which are designed to restrain which information states and transitions may hold, respectively. It is by way of these labellings that the data structure gains meaning, as they serve to relate linguistic parameters to the model: states are labeled with information about Holds, while transitions are tagged with data pertaining to Movements. Thus, a path in the articulation model of a ∈ ART can be interpreted as a sequence of Holds and Movements containing only information about a. A formal characterization of such a path, is given by Definition 4.14. Definition 4.14 (Articulation Sequence). Let M a = (S, R, • Φ a , • Π a ) be an articulation model for articulator a ∈ ART . An articulation sequence of M a , is a finite ordered list of transitions S a = ((s 0 , s 1 ), (s 1 , s 2 ), . . . , (s n , s n+1 )), such that:

-if (s k , s k+1 ) ∈ S a , then (s k , s k+1 ) ∈ R; -if transitions (s i , s i+1 ) and (s j , s j+1 ) are adjacent in S a , then s i+1 Φ a ≡ s j Φ a .
It is said that M a induces sequence S a , or that the latter is induced by the former.

Roughly, S a describes a phoneme sequence where only a participates, expressed by way of state changes over a LTS. Even though time duration is not expressed by the sequence, there is a correspondence between phonemes as time-intervals and S a , as depicted on -for any pair of adjacent transitions (s k-1 , s k ), (s k , s k+1 ) ∈ S a , with allotted time-

intervals T a ((s k-1 , s k )) = [t i , t j ) and T a ((s k , s k+1 )) = [t m , t n ), it holds that 1 < t i < t j , t m < t n and t j < t m ;
-for each state s k common to each pair of adjacent transitions, the state's allotted

time duration is T a (s k ) = [t j , t m ). In addition, if (s k-1 , s k ) ∈ Ŝa is the first transition in the sequence, then state s k-1 has a duration of T a (s k-1 ) = [1, t i ).
For simplicity, in the rest of this document e i ∈ Ŝa will denote element e i from articulation sequence S a ∈ Ŝa , unless indicated otherwise.

It is brought into attention that, for the rest of this thesis, intervals are defined in terms of natural numbers (i.e. positive integers). This is, interval Proof. By induction. Let (s 0 , s 1 ) ∈ S a be the first transition in the sequence. By Definition 4.15, T a labels state s 0 and transition (s 0 , s 1 ) as T a (s 0 ) = [1, t) and T a ((s 0 , s 1 )) =

I = [m, n) is
[t, t ′ ), respectively. Therefore, it holds for T a (s 0 ) < T a ((s 0 , s 1 )). Assume it holds for the interval sequence T a (s 0 ) < T a ((s 0 , s 1 )) < T a (s 1 ) < . . . < T a ((s k-1 , s k )) < T a (s k ).

For T a (s k , s k+1 ), we know by Definition 4.15 that the state s k , common to two adjacent transitions, is labeled as follows: if

T a (s k-1 , s k ) = [t i , t j ) and T a (s k , s k+1 ) = [t m , t n ),
then T a (s k ) = [t j , t m ). Thus, interval T a (s k , s k+1 ) necessarily starts at time t m , where T a (s k ) < t m , which implies that T a (s k ) < T a (s k , s k+1 ). Then, for T a (s k , s k+1 ), it holds.

In some cases, the parameters given by a single timed articulation sequence are enough to model complete phonological sequences; for instance, when representing one handed signs, the information of a single hand may be all that's needed to characterize a sign. For this

M a , s k |= ⊤ always holds; M a , s k |= p a iff p a ∈ s k Φ a ; M a , s k |= ¬ϕ iff M a , s k |= ϕ; M a , s k |= ϕ ∧ ψ iff M a , s k |= ϕ and M a , s k |= ψ.
Let e ij = e i , e i+1 , . . . , e j ∈ Ŝa , i ≤ j be a chain of adjacent elements in the sequence Ŝa , and let s k denote any state in any transition e i ∈ Ŝa . Also, note that π a ∈ Π a and α, β ∈ A SL . Satisfaction over timed sequences is given as follows:

Ŝa , e ij |= ⊤ i = j, e i = (s k , s k+1 ), and

M a , s k |= ⊤; Ŝa , e ij |= p a iff i = j, e i = (s k , s k+1 ), and M a , s k |= p a ; Ŝa , e ij |= ¬ϕ iff i = j, e i = (s k , s k+1 ), and M a , s k |= ¬ϕ; Ŝa , e ij |= ϕ ∧ ψ iff i = j, e i = (s k , s k+1 ), and M a , s k |= ϕ ∧ ψ; Ŝa , e ij |= π a ϕ iff i = j, e i = (s k , s k+1 ), π a ∈ (s k , s k+1 ) Π a and M a , s k+1 |= ϕ; Ŝa , e ij |= α; β ϕ iff Ŝa , e ij |= α β ϕ;
Ŝa , e ij |= ψ; α ϕ iff Ŝa , e ik |= ψ and Ŝa , e kj |= α ϕ, where

i ≤ k ≤ j.
The missing PDL SL operators cannot be defined in terms of timed articulation sequences, as their meaning is related to the interaction between two or more articulators, whereas each Ŝa holds information about a single articulator. To address this situation, Definition 4.17 introduces a new data structure built upon sets of timed articulation sequences, enabling the synchronization of multiple channels into phoneme chains.

Definition 4.17 (SL Utterance). A SL utterance is a tuple U = (P, T U , • U , SEQ)

where:

-P is an arbitrarily long list of ordered phonemes p 0 , p 1 , . . . , p n ;

-T U : P → N × N is a time-labeling function for phonemes; -• U : P → 2 Φ∪Π labels phonemes to a set of atomic propositions and actions (a more thorough description is given in Definition 4.19);

-SEQ is a group of timed articulation sequences such that, for each a ∈ ART , there is exactly one sequence Ŝa = (S a , T a ) ∈ SEQ.

The list P is time-labeled recursively as follows:

1. For p 0 , let e 0 , e 1 , . . . , e n = Ŝ• ∈ SEQ be the timed articulation sequence holding the earliest occurring transition of all; this is, T • (e 0 ) = [t, t ′ ) has the smallest t of every sequence in SEQ. The phoneme p 0 represents the first occurring phoneme in the utterance, and is time-labeled as T U (p 0 ) = [1, t), 1 < t.

2. For any other p N , N > 0, such that T U (p N -1 ) = [t i , t j ), p N is time-labeled as

T U (p N ) = [t j , t k )
, where t k is either the first instant after some transition ends, or the first instance where a new transition starts, and t i < t j < t k .

In general, utterances synchronize information with respect to global articulatory changes;

intuitively, utterances strive to maintain a strict ordering across all sequences in SEQ, dividing each sequence if necessary when concurrent articulations show changes. In this sense, phonemes can be seen as "cuts" of time where articulation parameters remain essentially static. Utterances make possible the combination of propositional information from different channels, regardless of whether it corresponds to static or change parameters. For this reason, it is important to ensure that articulators will retain consistent properties when the information is combined into phonemes; notably, it is important to be certain that a phoneme will not hold contradicting information about each articulator. In this respect, utterances guarantee that articulation changes won't occur inside phonemes, but rather than they will be generated around them, as shown by the following lemmas.

T a ((s k-1 , s k )) < T a (s k ) < T a ((s k , s k+1 )), with respective values T a ((s k-1 , s k )) = [t v , t w ), T a (s k ) = [t w , t x ) and T a ((s k , s k+1 )) = [t x ,
T a ((s k-1 , s k )) < T a (s k ) < T a ((s k , s k+1 )) < . . . < T a ((s n , s n+1 )),
Lemma 4.2 implies that t ′ < t w and, since Ŝa is strictly ordered, it is not possible that T U (p N ) and T a ((s n , s n+1 )) overlap. Once proven that information won't change inside phonemes, it is safe to define phonetic parameters in terms of utterances; as presented in Definition 4.17, phonemes are labeled by way of a mapping • U , the details of which are explained by the next two Definitions.

Definition 4.18 (Phoneme to sequence mapping). Let U = (P, T U , • U , SEQ) be an utterance and p N ∈ P be a phoneme labeled with time interval T U (p N ). Let Ŝa ∈ SEQ be the timed articulation sequence in U corresponding to articulator a ∈ ART , while

M a = (S, R, • Φ a , • Π a
) denotes the articulation model inducing Ŝa . Also, let T a be the time-labeling function associated to Ŝa . Function V a : P → S ∪ R, mapping phonemes to transitions or states of the articulation model M a , is defined as follows:

V a (p N ) =                e k if T U (p N ) overlaps with T a (e k )
, where e k ∈ Ŝa ;

s k if T U (p N ) overlaps with T a (s k ),
M a = (S, R, • Φ a , • Π a
) denotes the articulation model inducing Ŝa . The mapping

• a U : P → 2 Φ a ∪Π a , denoting the parametric information of articulator a ∈ ART at interval T U (p N ), is defined as follows:

p N a U =            V a (p N ) Π a if V a (p N ) ∈ R; V a (p N ) Φ a if V a (p N ) ∈ S;
where V a is the mapping given on Definition 4.18.

The function giving the set of phonetic parameters of p N ∈ P is then defined as:

p N U = a∈ART p N a U
Finally, Theorem 4.4 shows that utterances take in account every articulatory change; this is, that if some transition occurs between two parametric states, then it will be contained in an utterance's phoneme. Proof. By contradiction. Suppose that there exist a timed articulation sequence Ŝa where some transition (s k , s k+1 ) ∈ Ŝa is not represented in P. If this is the case, we know (s k , s k+1 ) was not the first transition in SEQ, or it would have been added as per Definition 4.17.

Since (s k , s k+1 ), time-stamped as T a ((s k , s k+1 )) = [t i , t j ), is not represented in the sequence, it means that there is a phoneme p N which was time-stamped as T U (p N ) = [t h , t i ) and a phoneme p N +1 which was time-stamped as T U (p N +1 ) = [t j , t k ). However, if T U (p N ) = [t h , t i ) then, by the definition of U it is the case that T U (p N +1 ) must have started at time t i , because we know that t i it is the beginning of transition (s k , s k+1 )! Also, note that if phoneme p N +1 starts at time t i , it will either end at time t j-1 or before. With these results, it becomes apparent that there will always be a consistent phoneme in U for transition in SEQ; that is, phonemes will neither omit information nor contain contradicting propositions, as long as articulation sequences themselves remain consistent.

Thus (s k , s k+1 ) Φ a ⊆ p N +1 U .
Finally, Lemma 4.5 provides an idea of how many phonemes are needed to build U. Proof. Theorem 4.4 implies that, if transitions don't overlap, each of them will induce the time-stamping of, at least, one phoneme. Recall by Definition 4.17 that phonemes, except from the first one, will always be time-stamped either when a transition's interval begins or ends. In addition, from the definition, if the start of a transition's interval induces the time-stamping of a phoneme, then said phoneme will have, at most, the same length than the interval, at which moment a new phoneme will be issued. This implies that every non-overlapping transition will necessarily induce the time-stamping 2 phonemes. Also, note that if k transitions overlap, k ≥ 2, then it can be the case that:

-they perfectly overlap, in which case a single phoneme contains the information of all the transitions; -they don't perfectly overlap, in which case at most 2k phonemes will be created, if none of their starting or ending points are aligned.

Finally, note by Corollary 4.3 that transitions are totally ordered, implying that they will only be tagged once by U. Thus, in the worst case, U will time-stamp 2n phonemes, two for each transition, plus the phoneme in the beginning, giving 2n + 1.

Overall, these properties permit defining the semantics of concurrent PDL SL formulae over utterances, in terms of phonological change; the proposed satisfaction rules are presented in Definition 4.20. Definition 4.20 (PDL SL formulae satisfaction over utterances). Let U = (P, T U , • U , SEQ) be an utterance and p N ∈ P be a phoneme labeled with time interval T U (p N ). Let Ŝa ∈ SEQ be the timed articulation sequence in U corresponding to articulator a ∈ ART , while M a = (S, R, • Φ a , • Π a ) denotes the articulation model inducing Ŝa . Also, let ϕ and ψ be PDL SL formulae and p a ∈ Φ a . Let p ij = p i , p i+1 , . . . , p j ∈ P, i ≤ j be a segment of phoneme list P starting in p i .

Similarly, let e ij = e i , e i+1 , . . . , e j ∈ Ŝa , i ≤ j be a chain of adjacent transitions in the sequence Ŝa . For simplicity, if i = j then p ij ≡ p i and e ij ≡ e i . Satisfaction over utterance phonemes is given as follows:

U, p ij |= ⊤ iff i = j, always holds; U, p ij |= p a iff i = j, s k = V a (p i ) ∈ S
U, p ij |= ϕ ∧ ψ iff i = j, where U, p i |= ϕ and U, p i |= ψ; U, p ij |= π a ϕ iff e m = V a (p i+1 ) ∈ Ŝa where e m = (s k , s k+1 ) such that Ŝa , e m |= π a ⊤, and for V a (p N ) ≡ s k+1 , where i < N ≤ j, it holds U, p N j |= ϕ; U, p ij |= α; β ϕ iff U, p ij |= α β ϕ; U, p ij |= α ∪ β ϕ iff U, p ij |= α ϕ or U, p ij |= β ϕ; U, p ij |= α ∩ β ϕ iff U, p iN |= α ⊤, where i < N ≤ j and U, p iM |= β ⊤, where i < M ≤ j such that, -if N < M then U, p N +1M |= ¬ α ⊤ and U, p M j |= ϕ; -if M < N then U, p M +1N |= ¬ β ⊤ and U, p N j |= ϕ; -if M = N then U, p N j |= ϕ; U, p ij |= α ∧ ψ ϕ iff U, p iN |= α ⊤, where i < N ≤ j such that U, p iN -1 |= ψ, and U, p N j |= ϕ; U, p ij |= ψ; α ϕ iff U, p iN |= ψ, where i ≤ N < j and U, p N j |= α ϕ.
where π a ∈ Π and α, β ∈ A SL .

With these semantic rules, annotators can use formulae to determine if a property holds over a sequence of phonemes or not. Furthermore, they permit to alter their phonological interpretation, depending on how the formula is build. For instance in the case where articulator a moves and articulator b remains static, and formula ϕ a , giving information about articulator a exclusively, will see at least one Movement, whereas ϕ b will see a single Hold. This is because the semantic rules rely on the individual articulation sequences to implicitly discard unused information; in this case, as formula ϕ b only needed information from b, the channel of articulator a was ignored and the formula was satisfied directly on the individual articulation sequence Ŝb . This provides a mechanism to verify both individual and concurrent properties over the same structure.

Chapter conclusion

This chapter presented the main theoretical notions of this work. In the first part, a series of primitive sets where introduced, which serve as basis for the representation of SL phonetic parameters as logical statements (see Table 4.1). Additionally, a group of time-ordered data-structures was defined, in an effort to have a formal representation of temporal change. Both primitive sets and data-structures where connected with each other by way of a formal framework, based on the PDL, which was developed with the intention of being inherently multimodal, to cope with the notion of parallel articulatory changes.

Generally speaking, the main interest of the presented definitions is to establish a correspondence between very abstract notions and real world data. It is for this reason that primitive sets are introduced as templates to be filled by an expert, depicting fairly broad descriptions. The same holds true for the data-structures themselves, as they can correspond to different use cases depending on expert observations: for instance, the utterance objects from Definition 4.17 can serve to represent one-handed signs, two-handed signs, changes in NMFs and others.

The relationship between real-world observations and the formalism becomes clearer if we consider that a video from a corpus, for example, can be represented as an utterance object during an automatic recognition task; assuming that the proper technical tools are available, it is possible to follow changes on individual articulators and combine them on-the-fly, just as utterance objects do with timed articulation sequences. Furthermore, the flexibility of this particular data structure permits the addition or removal of channels as needed. In the real world, this can be useful for situations where a tracking system can only follow changes over a limited number of articulators, thus not needing to model any of the non-tracked information channels while still being interested on combining those which are.

Primitive Set Description

N AMES

The set containing every chain of characters.

BODY

Contains any body part visible during signing, BODY ⊂ N AMES.

ART

Refers to all body parts capable of articulation, ART ⊆ BODY.

Ψ SL

Establishes a three-dimensional coordinate system originating on the signer's center of mass, where

Ψ SL ⊂ R × R × R.

LOC

Holds pairs of articulators with their respective places of articulation, denoted as (a, λ), where a ∈ ART and λ ⊂ N AMES (λ is the name of a location).

CF G

Holds pairs of articulators with their possible configurations, denoted as (a, c), where a ∈ ART and c ⊂ N AMES (c is the name of a configuration).

∆ Contains pairs of coordinates describing a vector in Ψ SL , ∆ ⊆ Ψ SL × Ψ SL .

L ∆

Refers to a function assigning names to vectors in ∆, permitting more abstract definitions such as "Up" or "Down".

DIRECT ION S

It is the set of names that can be used by L ∆ to label some vector, DIRECT ION S ⊂ N AMES.

∆ SL

Contains sets of vectors identified by a individual direction names in DIRECT ION S: for instance, it contains every individual vector that can be labeled as going "Up".

Π Contains every atomic action related to every individual articulator in ART .

Φ

Contains every atomic proposition related to every individual articulator in ART . Something similar occurs with PDL SL formulae: since they are intended to be interpreted over an utterance, they can be used to analyze SL videos once they have been turned into abstract representations. In particular, formulae can be used to ask question about the video, for instance, so as to determine whether a sign appears or not over a determined segment of video-frames. In this regard, the language is designed to be flexible enough to add or discard information depending on the available data, therefore adaptable to different types of corpora.

In order to give a better picture of how everything works in practice, the next chapter provides a concrete example. On Chapter 5, the formal structures defined on this chapter are used on a real-world recognition task, oriented towards the semi-automatic annotation of a corpus. Essentially, the idea is to show, step by step, how humans and an automatic system can interact to fill up the primitive sets (see Table 4.1), leading to the automatic specification of a corpus and its partial annotation by way of PDL SL formulae.

Chapter 5

Semi-automatic annotation using logic

The previous chapter introduced the Propositional Dynamic Logic for Sign Language (PDL SL ), a formalism intended to represent Sign Language (SL) corpora in Natural Language Processing (NLP) tasks. Overall, the PDL SL provides a set of basic rules to capture different corpus features under the same formal language, regardless of the technical characteristics of said corpus. For this reason, when confronted with real-world data, it is the task of the annotator to narrow down or extend the language as required, in order to suit his or her specific needs.

In this chapter, an example of the representation process is introduced with the implementation of a modular, PDL SL -based, semi-automatic annotation framework. In particular, the system was designed to work over the Dicta-Sign corpus (see Chapter 3,Subsection 3.3.3,p. 65), a French Sign Language (LSF) corpus. Broadly, the system core consists on both an implementation of utterances (see Definition 4.17, p. 89), and a PDL SL interpreter. A series of processing modules were built around these basic components, in order to automatically transform each corpus video into an instance of a utterance.

Utterances are none other than directed acyclic graphs, linked to per-articulator Labeled Transition Systems (LTSs). In the final step, a series of PDL SL -described properties are searched automatically in the graph, and the results are returned to the user as an ELAN annotation file.

In the following section, a brief description of the framework's architecture is presented, including a bird's-eye view of the overall process as intended in practice. Likewise, this portion contains a module-by-module description, demystifying the procedure on a step-by-step basis. Finally, the last couple of pages present the implementation of a semi-annotation system, created by following the described framework's guidelines.

Framework Architecture

As already stated, the main objective of the framework is to be able to receive an untreated SL video input, and return a set of possible annotations, calculated by way of formal verification. Figure 5.1 shows a diagram describing the data workflow. In the Figure 5.1, circles represent information whereas squares depict individual processing modules; each module receives a particular input and their results are sent to other modules for further processing. Each module has its own specialized role, and together they take untreated corpus data and calculate an annotation file that can be used for linguistic research. In general, modules tasks can be broken as follows:

-Division Module Divides input data into time intervals.

-Modeling Module Encodes the information from time intervals into a graph.

-Logic Verification Module Uses the graph to verify a database of PDL SL formulae, and generate an annotation.

-Annotation Tool Enables human experts to correct the results.

In the next sections, each of the modules depicted in the figure will be individually described, explaining in detail how each of them contributes to the generation of an automatic annotation.

Division Module

The Division Module, highlighted in Figure 5.2 is in charge of processing the raw corpus data and transform it into an interval segmentation. On the figure, the points over the signer's hands and head represent the calculated positions for each. In addition, the colored line represents the path that the left hand followed when moving from one position to the other; the point where the line changes color, represents the instant where the hand achieved maximum speed.

Interval segmentation based upon this tracking tool, rely on defining articulation changes in terms of speed. In particular, the Division Module follows the observations made by [START_REF] Gonzalez | [END_REF]], and selects segments by looking at speed variations. For the module, a frame is static if the speed of the observed articulator is below the noise threshold of the tracker (approx. 1.08 pixels/frame). Moreover, a frame is considered a change if its speed is above the threshold. On a similar note, static intervals are defined as sequences containing only static frames, while change intervals are sequences containing only change frames.

Since the tracking tool is limited to detect only hands and head, it is not possible to create a segmentation for any other articulators outside of these three. In addition, for Dicta-Sign in particular, the average speed of the head during movement held approximately the same value as the calculated noise threshold for the tested videos. A graphic showing how speed measures compare, for the three articulators, is presented in Figure 5.7. In the graph, speed changes below the noise threshold were set to zero, for clarity. both hands are moving). Under these conditions, the individual segmentation of the head is unreliable, hence forcing the module to only generate interval sequences for the hands.

In addition, the detection of other change-inducing features, such as hand-configuration, isn't readily available. For this reason, segmentation has to be achieved by means of speed change alone, as presented by the Algorithm 1 below.

Recall from Subsection 4.3 (see p. 87) that intervals in this document are defined over the positive integers. Also, note that frames are enumerated over the same domain, thus starting in 1. Procedure Segmentation receives the tracker's noise threshold T ǫ and a total number of frames N . By definition, any speed lower than or equal to T ǫ is assumed to be static. Also, the speed of any of the hands in the first frame (v 1 ) is 0, meaning that Algorithm 1 Interval segmentation for a single hand in one video

1: procedure Segmentation(T ǫ ≥ 0, N > 0) 2: v 1 ← 0 3: I ← {1} 4:
L ← empty set of intervals 5:

for each frame i ∈ {2, . . . , N + 1} do 6:

v i ← instantaneous hand speed at frame i 7: if (v i > T ǫ & v i-1 ≤ T ǫ ) or (v i ≤ T ǫ & v i-1 > T ǫ ) then 8:
L.add(I) end for 14:

L.add(I)

15:

return L 16: end procedure the first frame is static by default. From there, for the hand of interest, at each frame i > 1, the algorithm reads the hand's speed v i and uses it to decide whether i is part of an interval I or not; roughly, if i and i -1 are both of the same type and i -1 ∈ I, then i ∈ I. Finally, the procedure stops in N + 1, to ensure that the sequence will always end on a static interval (we assume that v N +1 = 0). Proof. By induction over the length of L. Let I 0 be the first interval in L. Let i be the first frame where the hand changes, hence v i > T ǫ holds. If such i doesn't exist, every frame necessarily falls on the case of line 10, thus ensuring that they will all be added to interval I, defined in line 3. Since no change frame exist, I is static. Furthermore, because line 14 is always executed before returning, then I will be added to L, thus ensuring that I = I 0 and L = ∅.

If a change frame i does exist, we know from line 2 that i = 1. Also, note that for every frame f ∈ [1, i -1] it holds that v f ≤ T ǫ , warranting that each will enter the case in line 10 and thus

I = [1, . . . , i -1]. Since v i > T ǫ and v i-1 ≤ T ǫ , then i enters in the case of line 7, thus it holds that L = [[1, . . . , i -1]] and I ← [i].
In this scenario, it is always the case that I = I 1 , since either it gets overridden again in line 9, after being added to L, or I is never overridden again and is added by line 14. Thus, for I 0 it holds.

For I k , assume that L = [I 0 , . . . , I k-1 ] is correct. Let I k-1 = [m -M, . . . , m -2, m -1];
interval I k-1 could have only been added to L by line 8, meaning that for frame m it was the case that either

(v m > T ǫ & v m-1 ≤ T ǫ ) or (v m ≤ T ǫ & v m-1 > T ǫ ).
This situation renders frames m -1 and m of different types. In addition, we know that, by entering the case of line 7, frame m became the first frame in I, after adding I k-1 to L.

Finally, from here, it will always be the case that I = I k since, once again, either I gets overridden in line 9 after being added to L, or I is never overridden again and is added by line 14. Thus, for I k it holds.

Algorithm 1 generates a valid sequence of interleaved change and static intervals; however, the changes inside the sequence aren't completely accurate in terms of what movement they are capturing. As observed by [START_REF] Gonzalez | [END_REF]], it is often the case that signers chain hand movements without passing through a static interval, as they conserve momentum.

An example can be seen in Figure 5.7 above: in frame 2926, the right hand ended some movement without attaining speed 0 and, immediately after, started a new one. This can be observed on the sudden drop of speed experienced by the hand, which is rapidly gained on the next instant. However, these changes remain largely invisible for Algorithm 1, which would consider [2923,2930] is a single change. To avoid this situation, change intervals are further subdivided with respect to speed minimums, by the procedure presented in Algorithm 2.

Algorithm 2 Change interval sub-segmentation for a single hand in one video for each frame i ∈ {m + 1, . . . , n -1} do 8:

v i-1 ← instantaneous hand speed at frame i -1 9: v i ← instantaneous hand speed at frame i 10: v i+1 ← instantaneous hand speed at frame i + 1 11: if (v i-1 > v i & v i < v i+1 ) then
k ; v i-1 , v i and v i+1 . If v i-1 > v i < v i+1 ,
then, by lines 12-14, we know that L c = ({i -1}, {i}) and I = ∅.

With |I k | = 3, the for is executed only once, thus, the algorithm executes lines 19 and 20, resulting in L c = ({i -1}, {i}, {i + 1}), which is returned immediately after. Note that, by the sake of the comparison in line 11, {i} denotes a minimum. Then, for

|I k | = 3, L c holds. On the other hand, if v i-1 > v i < v i+1 is false, then I doesn't change, thus I = {i -1}.
By line 16, I = {i -1, i}. Once again, the for is executed only once, thus, the algorithm executes lines 19 and 20, giving I = {i -1, i, i + 1}, L c = (I) and returning L c . Since

I ≡ I k , it holds.
For |I k | = N > 3. Assume without loss of generality that I k = {0, 1, . . . , N }. Also, assume that, until N -1, L c is a correct interleaving. Recall that the for ranges from 1, . . . , N -1. In the last execution, it must have compared speeds v N -2 , v N -1 and v N .

If v N -2 > v N -1 < v N , then L c = (. . . {. . . N -2}, {N -1}) where {. . . N -2} is a change
and {N -1} is a minimum. Note that the comparison ensures that I = {. . . N -2} will always be a change, as in the previous for execution, line 11 tested v N -2 > v N -1 and added N -2 to I. Now, as {N -1} was the last interval added to L c , then I = {}. Also, since N -1 corresponds to the last test of the for, the algorithm executes lines 19 and The previous theorem, shows that Algorithm 2 uses speed minimums to produce an interleaving, depicting similar characteristics to those resulting from the first algorithm. In turn, this similarity can be exploited to combined both results into a single interval chain: the idea is to substitute all changes in the first sequence with their sub-segmentation, if any. In general, this corresponds to forcing local minimums into static intervals, a process presented in Algorithm 3. return L s 17: end procedure Theorem 5.3 (Change interval substitution). In the resulting interval list L s , produced by Algorithm 3, every "true" change interval will be surrounded by either two static intervals, two minimum speed intervals or one of each.

20 giving I = {N } and L c = (. . . , {. . . N -2}, {N -1}, {N }) is returned. Since we know that, v N -1 < v N , then N is not a minimum, therefore L c holds. If not v N -2 > v N -1 < v N ,

Algorithm 3 Substitution of change intervals

1: procedure SegmentSubstitution(L = interval sequence) 2: if |L| == 1 then 3: L s ← L 4:
Proof. Assuming that L is a correct interleaving, if |L| = 1 then there are no change intervals, so it holds by vacuity. For |L| > 1, we know by Theorem 5.1 that every change interval in L is surrounded by two static intervals; recall that L always ends on a static interval. By Theorem 5.2 we know that SubSegmentation(I) in line 10 is an interleaving of change and minimum speed intervals, where the first and last I s ∈ Sub-Segmentation(I) are always "true" changes. Thus, for |SubSegmentation(I)| ≤ 3 it holds: the first and last change intervals will be surrounded by one minimum speed and one static interval, while any other will be surrounded by minimum speed intervals.

Even though, by definition, minimum speed intervals are not truly static, the system makes no difference between the two; to avoid any potential pitfalls in this regard (at least from the implementation point of view), each time a minimum frame is found the module sets its speed to zero, so as to maintain consistency. An example of the entire process, for the right hand, is given on Figure 5.8. In Figure 5.8, a speed graph for the right hand is presented, with its corresponding interval segmentation; there, intervals are depicted as either boxes (static) or arrows (change), depending on how they are interpreted by the module. Broadly, the first segmentation presents the resulting sequence after executing Algorithm 1. The second, presents how changes are affected when passed through Algorithm 2. Finally, the last sequence presents the result of combining the two previous ones, by way of Algorithm 3;

this is the one that will be passed over to the next module, for further processing. Also, note that the depicted sequences are just segments of a larger sequence, produced for the entire video. It is for this reason that the first sequence ends on a change interval and not on a static one (more intervals follow).

The choice of introducing artificial static intervals, was made to capture instants within long movement chains where it is clear that more than one change occurred. Further down the line, these reduced states serve as points of reference for the verification module, to detect smaller changes within these movement chains. Also, note that these points contain exactly one frame, as the comparisons in line 11 of Algorithm 2 are strict. This is to avoid, in the measure of possibility, breaking up changes that may be intentionally slower.

The module executes Algorithm 3 for each hand and passes both results to the next module, where they will be formally represented as explained in the next section.

Modeling Module

The Modeling Module, shown in Figure 5.9, is the one in charge of transforming the raw video information into a formal data structure. More precisely, the module receives an interval segmentation for every articulator, like the one shown in Figure 5.5, and uses the available information to determine the truth value of a series of statements about articulators. More specifically, this module implements the utterance objects presented in Definition 4.17, and executes an algorithm to tag utterances with information, depending on what it can automatically infer from video images. For this reason, in order to generate the graph, the module has to know how to make sense of visual information, and convert it into a more abstract representation. This is achieved by giving concrete domains to the PDL SL primitive sets of Section 4.1 (p. 79); once this information is in place, the module becomes knowledgeable enough to determine which articulators are being described, which statements are true on a given video-frame and, overall, the kind of data that has to be modeled.

In the next section, primitive information is defined for the case of Dicta-Sign corpus, when paired with the tracker presented by [Gonzalez 2011].

Primitives for a 2D corpus

Recall from last chapter (see Chapter 4, Section 4.1 p. 79) that PDL SL defines a series of set templates, intended to be used in the creation of atomic propositions and actions;

originally, these sets where defined very broadly, as they have to be general enough to cover a vast number of use cases. In the case of the study of a specific corpus, as is the case with Dicta-Sign, it is not necessary to have such broad definitions. In fact, confronted with data, the opposite becomes true: it is necessary to have a very detailed With respect to space, it has already been mentioned that Dicta-Sign is a 2D corpus;

for this reason, the coordinate system established by Ψ SL is limited to two dimensions, simply giving: Definition 5.3 (Space coordinates for 2D corpora).

Ψ SL = R × R × {0}
In general, Ψ SL doesn't change with respect to Definition 4.3; it is a given that the only possible value in the third dimension in Dicta-Sign, reachable by any articulator, is zero.

Hence, the original definition is valid and compatible with Definition 5.3.

Once articulators and their spatial frame of reference is determined, it is possible to define their places of articulation. From Definition 4.4, recall that each articulator a ∈ ART will have its own set of places LOC a . In the case of the hands, both sets will almost be identical, with the exception that they won't contain themselves as locations. The visual depiction of the defined places of articulation is shown in Figure 5.11; each region can be as small or as large as desired, depending on the definition of C -1 . Note that the defined regions may overlap. Because of this, in some video corpora there might be ambiguity in region definitions, due to the lack of a third dimension: in Figure 5.11, the neutral space should denote the 3D spatial coordinates around the signer, which is not possible to model in a 2D corpus. In this context, UPPERBODY and LOWERBODY are inaccurately defined as sub-planes of NEUTRAL, because of this technical limitation.

Nevertheless, the advantage of holding the meaning of spatial locations into an external function, in this case C -1 , is that it can be easily adapted for the 3D case by changing the function itself, while leaving the region names intact.

Definition 5.4 is largely based on function C; from the implementation point of view, this corresponds to a data structure, mapping 2D image subsections to strings. For Dicta-Sign, the human annotator can define regions as rectangles on the image's coordinate system, thus permitting to easily add or remove articulation places as needed; in this sense, it is the internal representation itself who provides C rather than the user.

The last set defined on a per-articulator basis, is the one containing the possible configurations an articulator can assume. In this case, as the only articulators in ART are the hands, the configuration set CF G will contain only hand-configurations. However, as previously explained, the used tracking tool is unable to detect complex features such as configuration change; because of this, the module isn't capable of using CF G. Regardless, it is useful to provide these definitions anyway, at least to exemplify how they fit in the overall process. The proposed CF G is presented on Definition 5.5 below. DIRECT ION S = {↑, ր, →, ց, ↓, ւ, ←, տ}

The set of relevant directions is defined as follows:

∆ SL = t∈DIRECT ION S L -1 ∆ (t)
where L -1 ∆ (t) is defined for every t ∈ DIRECT ION S.

Similar to what happens with the places of articulation, ∆ SL is completely based on how the function L ∆ was defined. For its implementation, the definition comes rather straightforward: for example, ← are all vectors with starting and ending coordinates (start 0 , start 1 ) and (end 0 , end 1 ), respectively, such that start 1 ≡ end 1 and start 0 < end 0 . This is, they only change horizontally, towards the left side of the coordinate system. For With this last definition, the contents of the primitive sets (see Chapter 4, Section 4.1, p.

79) have been completely specified for the case of a 2D corpus. From here, it becomes possible to define the sets of atomic propositions and actions, by using the members of the sets above to give statements about video segments. This process is presented in the next section.

Atomic propositions and actions for a 2D corpus

As presented in Chapter Remember from the previous section that, for the time being, only the hands are considered articulators. The atomic propositions for hand a ∈ ART are defined below. Intuitively:

-δ a .-Indicates that hand a moves in direction δ (i.e. → a asserts that hand moves to the signer's left).

a .-Asserts that a executes a single clockwise-motion.

a .-Similarly, asserts that a executes a single counterclockwise-motion.

a .-The hand a does a trill motion: it moves rapidly and continuously without changing its articulation place.

The set Π is the same as in Definition 4.10.

Actions assert information about change. An example of this is presented in Figure 5.15, where atoms ← R and → L capture the changes occurring in the right and left hand, respectively, during some interval of time. In contrast to the members of set ∆ SL , the movements a , a and a in Definition 5.8 are not thoroughly defined. This is because it is assumed that they can be approximated by combining small chains of movements in ∆ SL : for example, a could be seen as a sequence (ր, →, ց, ↓, . . .). In this regard, it is important to underline that atomic actions happen over a single change interval: they are swift, uncut movements.

Finally, it is important to underline that the definitions of Φ and Π remain unchanged.

With this, the Modeling module can directly create and label utterance objects, by way of a single algorithm. The details of this process are presented in the next section.

Transforming interval segments into utterance objects

Recall that the Division Module results into a segmentation of change and static intervals, as depicted in Figure 5.16. Intuitively, the articulation model of articulator a, encodes all possible significant postures of a as a LTS. For instance, the articulation model of the right hand M R (in LSF), has some state s 0 where cfg(R, INDEX) is true (the right hand has the index finger extended).

If there are n possible configurations in CF G a , then there are at least n -1 transitions starting in s 0 , taking the hand from INDEX to any other valid configuration.

However, articulation models are not a given for the module; each interval in the input segmentation is interpreted a valid state of some unknown model. Thus, the system is incapable of asserting information about the validity of each M a , but may infer its states, induced by static intervals, and how they connect with each other. To this end, the system needs a way to assert the propositional information on each state; a method to find • Φ a and • Π a . This is done by way of modeling rules, as defined below. From the implementation point of view, modeling rules are functions that indicate whether an atom holds over some video segment. Intuitively, they are the rules used to determine the meaning of atomic actions and propositions with respect to real-world data.

As with the labelings for regions, configurations and directions, these functions are not directly implemented by the module, but are provided externally. For this particular case, the existing rules are able to determine the truth values of simple statements over 2D images, using only hand tracking; this is, whether a hand is inside some region (for pos), if it is located in certain position with respect to the other (for touch), if there is a clear direction of movement (for δ a ), etc. In turn, these rules enable the construction of model M a , sequence Ŝa and, ultimately, utterance object U (see Definition 4.17 let Ŝa = (S a , T a ) be an empty timed articulation sequence of a. Algorithm 4, receives a set of interval sequences for n articulators, and a modeling rule R.

For each interval in each sequence, it infers the information on the model by using R to test, one by one, each of the defined atoms. Simultaneously it builds the set SEQ, which can be used to generate utterance U in line 28. Also, note that U is well-defined; from Definition 4.17, it is clear that the set SEQ is the only external requirement to build U, thus no further procedures are needed. Figure 5.17 shows a visual representation of the results. Once the utterance construction is complete, the resulting graph is passed to the next module, which will be in charge of analyzing the result by way of formal verification.

The process is explained in the next section. The input of the module is the utterance graph, generated during the modeling phase, and a database of PDL SL formulae, which is introduced in the next section.

Formulae database

The formulae database consists on a list of all the properties that an annotator wants to find on the video, encoded in PDL SL . From the implementation point of view, the database is a simple text file, which is interpreted on-the-fly by an internal PDL SL parser.

As such, no specialized tools are needed for its creation, as a simple text editor is sufficient to generate the file.

Formulae in the database are assumed to be based on the same formalization primitives used by the Modeling module (see Subsection 5.1.2.1,p. 110). However, it is noteworthy to mention that this doesn't impede the database to contain formulae built upon other, undefined, primitives; this is a desirable characteristic in situations where future improvement is expected from the point of view of signal processing. For example, annotators may add formulae expressing changes in the Non-Manual Features (NMFs), expecting that in the future there might be a reliable way to recognize these changes automatically.

By relying on these modular phonetic descriptions, PDL SL can be used to design formulae representing structures closer to the morphological level. For instance, consider the iconic production shown in Figure 5.20. The formula in Example 5.1, called ICONIC for simplicity, was built using the atoms presented by Definitions 5.7 and 5.8. In the top part, the formula establishes the information contained in the first H: the hands hold a certain configuration, they are positioned in front of the head and they are touching. The second line starts with an action denoting that both hands move, simultaneously, in opposite directions. The final section of the second line, introduces the result of the aforementioned movement over the first H: the hands remain in the same relative position, with the same configuration, but this time they are not touching. With respect to the latter, it is worth to mention that the atom ¬touch(R, L) was explicitly asserted to avoid implementation ambiguities.

Strictly speaking, the formula could have omitted the aforementioned atom and it would still be equivalent to the one presented.

The explicit declaration of the hands not touching, arises a peculiar characteristic of ICONIC: even though it is clear for a human, that separating both hands in opposite directions implies that they are no longer in contact, an automatic system will not necessarily have the ability to infer the same information. From here, it is easy to see that PDL SL is capable of expressing inconsistencies -e.g. the hands separate and then touch -however this is not an issue, since it is not its role to avoid them. Rather, formulae consistency must be checked by the human designer upon creation or, ideally, tested automatically during verification.

Note that the presented formula is not unique: ICONIC could have been described

differently, with different propositions. Also, observe that atoms of different articulators mix seamlessly within the formula, which is accepted by PDL SL satisfaction rules (see Definition 4.20,p. 94).

Finally, formulae in the database may also correspond to either lexical signs or other simpler structures, as long as they are representable in PDL SL . The idea is that, once the module knows about their existence, it can execute its verification algorithm regardless of the type of structure the formulae intend to describe. This results in a very flexible annotation creation process, since it is only necessary to adapt the database, and not the module itself, to produce different kinds of annotation. A more detailed description of the final verification process is explained in the next section.

Verification Algorithm

The principle of the verification algorithm, is based on the correspondence between formulae and utterance objects. For instance, let the formula from Example 5.1 be represented by ICONIC. It is the case that, in utterance object U from Figure 5.20, the following equation holds:

U, p 02 |= ICONIC (5.1) where p 02 = p 0 , p 1 , p 2 ∈ U.

Therefore, by observing in which phoneme sequences each formula holds, it may be possible to determine whether the described property exists over a video segment or not.

The complete verification algorithm is presented below.

Algorithm 5

Verifying PDL SL formulae in utterances 1: procedure UtteranceVerification(U, DB)

2:

Gloss ← {} 3:

for phoneme p i ∈ U do 4:

for formula ϕ ∈ DB do 5:

find the largest j such that i ≤ j and where DB denotes the PDL SL database. For each p i , it tries to find the longest sequence p ij such that U, p ij |= ϕ; this is, the longest video segment where a formula is satisfied (line 6). If such a sequence exists, it adds it to the proposed gloss, regardless if any other formula holds in the same sequence; the final proposal is not a unique annotation track, but rather a series of individual tracks (one for each formula). The module generates an editable file, that the user can modify directly by way of an annotation tool.

Annotation Tool

By thoroughly checking every state, the previously presented verification algorithm tries to maximize the number of possible hits; however, this process is usually prone to error, as several factors may mislead the module.

First of all, some of the existing phonemes may be co-articulations (see Chapter 2, Section 2.2.1.5, p. 31), which are indistinguishable from the others in the system. Since the algorithm is thorough, it will try to find hits in co-articulation phonemes, which may produce erroneous results. In addition, the noise introduced by tracking or segmentation errors may also induce the creation of incorrect phonemes, further complicating the problem. For this reason the final step of the process, shown by Figure 5.22, is simply the interaction with a human expert, who can modify the generated multi-track file by way of an annotation tool.

Dynamic Architecture Details

The framework introduced in Figure 5.1 (see p. 100), establishes the main development guidelines for any PDL SL -based semi-automatic annotation system: one interval segmentation phase, one modeling phase and one verification phase. Furthermore, even though the modules presented in the last section were developed to work over a specific corpus, the underlying system architecture was designed to be a dynamic framework; this is, a system able to adapt on-the-fly to different corpora and analysis tools. As such, the system considers the situations where the modules implementing each phase need to be swapped: for example, when the tracking technology changes, or if new segmentation parameters are added. To this end, the system core implements the observer architecture shown in Figure 5.24. The main idea behind this design, is for the framework to be able to:

-use several tracking tools, depending on the characteristics of the input corpus;

-generate consistent utterance models from any combination of different trackers.

This task is not as direct as it may seem; recall that the Division and Modeling modules, presented earlier, are heavily dependent on the available tracking information. This implies that different combinations of tools may result in differing interval segmentations and, ultimately, utterance models. In addition, not every corpus can be analyzed with the same automatic tools. As such, the framework has to coordinate the different possible inputs, in order to ensure that every SL resource will be paired with compatible signal processing software. This process is entirely done by way of event-triggering: each time some significant action happens, in any part of the system, a system-wide announce is sent. This mechanism enables communication between modules, allowing them to act appropriately depending on what events they receive. Furthermore, the architecture provides basic software interfaces for each of the framework's phases: roughly, it supplies implementation templates, detailing the inputs and outputs of each phase. With this, new modules developed to fulfill the tasks of any of the phases are forced to implement an interface, guaranteeing their compatibility. In turn, this promotes the creation of self-contained, interchangeable, modules, adapted to different research situations. For example, during the development phase, a preliminary Kinect-based Division Module was successfully hooked-up into the system, seamlessly introducing 3D movement information.

No further development of this, or other 3D modules, was pursued; however, the successful substitution of one of the modules without breaking compatibility, goes on to show the advantages of adopting this kind of architecture.

The execution process of the architecture is fairly straightforward. At the beginning, a

Start event is fired-up, prompting to load both a corpus resource and a processing tool.

This task corresponds to the Division Module of the framework (see Subsection Finally, even though the implementation details of the phases may change, the internal PDL SL representation remains unchanged, as it is part of the system's core. In this regard, the verification process remains largely unchanged, as it is rather the contents of utterance objects themselves that may affected by the module swapping, and not the formalism's rules.

Chapter conclusions

In this chapter, a PDL SL -based semi-automatic annotation framework was presented.

Broadly, the framework's architecture is divided into three processing modules: the Division Module, the Modeling Module, and the Logic Verification Module. Together, they change a corpus resource into an abstract representation which can be semi-automatically annotated. More specifically, this chapter presented a concrete implementation of the system's modules, designed to analyze the Dicta-Sign corpus with a 2D head-hands position tracker.

Briefly, the process works as follows: the Division Module receives an untreated video from the corpus and obtains the hand tracking information. Afterwards, the module uses the obtained data to separate each articulation channel into an interleaving chain of static and change intervals, reflecting video segments where the articulator of interest either changes or not. To this end, the module analyses the dynamic characteristics of the hands. The resulting interval chains are passed to the Modeling Module, who uses a series of predefined modeling rules to transform the chains into a utterance object (roughly, a directed acyclic graph). Finally, the Logic Verification Module takes the generated utterance and uses it to search properties in it; each property corresponds to a PDL SL formula, built by a human annotator. The final result can be edited by humans to correct the process as needed.

Even though the presented case is specific to Dicta-Sign, the underlying architecture is designed to enable the implementation of different versions of each of the modules, adapted to various types of corpora and tracking tools. This also helps to showcase the power of the formalism behind the implementation, as the chapter presented in detail how PDL SL primitive sets were restrained to adapt to a real world scenario. In this regard, some insight was given into how the theoretical specification may differ from practical application, as purely mechanical problems (mostly related to the quality and format of the inputs) can easily affect the final results, depending on how each problem is solved.

The next chapter continues to delve into the contrast between theory and practice, by presenting some of the results obtained from using this implementation to search for PDL SL -defined properties in video. In parallel, some of the formal language expressiveness issues will be addressed, alongside some discussion about how this can affect future computer-aided SL linguistic research.

provides no method to represent modularity. As a result, each time a PDL SL formula is defined it has to be completely rewritten, even in cases when it shares multiple sub-formulae with other database members. Additionally, there are instances where it is useful to have the capacity of predetermining the truth value of a formula, by modifying atoms' valuation. This is useful in situations when an annotator is testing different hypotheses on a corpus, as it enables him or her to assume something is either true or false, and observe its effects; for instance, he or she may want to know what happens when every hand configuration atom is valuated as true, in systems where hand configurations are not recognizable. Regardless of the application, both cases can be solved by adding an assignment operator to the language (=), that can be used to name formulae and assign truth values. The extended syntax is presented in Definition 6.1. Definition 6.1 (Extended PDL SL ). Let Λ : E ϕ → PDL SL be a map taking E ϕ to PDL SL formulae.

E ϕ ::= ϕ | ¬E ϕ | E ϕ ∧ E ϕ | E ϕ = ⊤ | E ϕ = ⊥ | η = E ϕ | η | λ η.(E ϕ )
where ϕ ∈ PDL SL and η ∈ N AMES.

In addition to assignments, Definition 6.1 introduces lambda expressions [Barendsen 1994],

to enable variable binding of atomic proposition and action parameters; as such, lambdas enable the description of groups of very similar formulae, for verification purposes.

Note that the satisfaction rules for E ϕ remain essentially unchanged: assignments are interpreted as PDL SL formulae, as shown by Definition 6.2. Definition 6.2 (Extended PDL SL semantics). Recall the mapping Λ from Definition 6.1.

The extended PDL SL formulae are defined recursively by Λ as follows:

-Λ(ϕ) ≡ ϕ.

- Finally, for some utterance U = (P, T U , • U , SEQ) satisfaction is given below:

Λ(¬E ϕ ) ≡ ¬Λ(E ϕ ). -Λ(E ϕ ∧ E ϕ ) ≡ Λ(E ϕ ) ∧ Λ(E ϕ ). -Λ(E ϕ = ⊤) ≡ Λ(E ϕ ) ⊤ , denoting that every atom in Λ(E ϕ ) is substituted by ⊤. -Λ(E ϕ = ⊥) ≡ Λ(E ϕ ) ⊥ , denoting that every atom in Λ(E ϕ ) is substituted by ⊥. -for η E ϕ , if Λ(E ϕ ) is defined, then Λ(η = E ϕ ) ≡ Λ(E ϕ ). -if Λ(η = E ϕ ) is defined, then Λ(η) ≡ Λ(η = E ϕ ). -For Λ(λ η.(E ϕ )), if Λ(E ϕ ) ∈PDL SL is
U, p ij |= E ϕ ⇐⇒ Λ(E ϕ ) is defined, and U, p ij |= Λ(E ϕ )
The presented extensions, improve the annotators' capacity to express succinct properties. where the domain of c is CF G R ∩ CFG L .

The formula can be modularized by way of the assignment operator, which enable the separation of opposition as depicted in Example 6.2.

Example 6.2 (modular opposition lambda expression)

.

hands conf ig(c) = cfg(R, c) ∧ cfg(L, c) (6.1) opposition = λc.(pos(R, ←, L) ∧ hands conf ig(c)) (6.2)
where the domain of c is CF G R ∩ CFG L .

In Example 6.2, pos(R, ←, L) indicates that R lies in direction ← with respect to L.

Also, note that cfg(R, c) and cfg(L, c) denote that articulators R and L, respectively, hold some configuration c; however, observe that, if they appear by themselves, these atoms are only defined if there exists a unique c ∈ CFG R ∩ CF G L . By way of the lambda operator, c gains a different meaning; in formula 6.2, the expression implies that c ≡ CFG R ∩ CFG L , thus indicating that opposition contains a sub-formula for every possible configuration common to both hands.

From the implementation point of view, lambdas can provide "syntactic sugar" to simplify formulae definitions. For example, by using opposition it may be possible to define signs SCREEN LSF and DRIVE LSF like shown in Example 6.3. Finally, assignments can help the system to better cope with situations where not every atom is present on an automatically generated utterance. Observe the formulae in Example 6.4, for the case where hand configurations are not recognizable.

Example 6.4 (opposition expression with a predefined valuation).

hands conf ig(c) = λc.(cfg(R, c) ∧ cfg(L, c)) = ⊤ (6.3) opposition = λc.(pos(R, ←, L) ∧ hands conf ig(c)) (6.4)
where the domain of c is CF G R ∩ CFG L .

Since the value of hand configuration atoms is not calculated during the creation of the utterance object, it is implicit by PDL SL satisfaction rules that, regardless the value of pos(R, ←, L), opposition will always be false, since hands conf ig(c) is falsified by default. However, if the value of hands conf ig(c) is overridden to become true (formula 6.3), then satisfaction of opposition will depend on the value of pos(R, ←, L), an outcome better adapted to the given situation. What's more, the definition of opposition itself didn't changed, as the override was done in one if the sub-formulae.

Experimental Results

By adapting the semi-automatic annotation framework (see Chapter 3,p. 41) to interpret the extended PDL SL , it was possible to obtain some results over a set of simple PDL SL formulae. In particular, two specific cases were tested:

-Verification over purely static, or "True", Hold intervals: in which utterance segments are a strict interleaving of Holds and Movements (static and change phonemes).

-Verification over non-purely static Hold intervals: in which every utterance segment can either be interpreted as a Hold or as a Movement, depending on which articulators the formula refers to (static and change information is mixed in each phoneme).

The idea of this separation, was to observe how different interpretations of a utterance affected the final gloss. For example, consider the first case, where Holds are purely static phonemes. In this scenario, each "True" Hold corresponds to time intervals where no change was detected in any of the articulation channels. An example is shown in Figure 6.2.

In the figure, the only time intervals considered "True" Holds were the ones where no articulator was moving or changing in any way; intervals where one of the hands show simultaneous speed minimums, creating a static interval on every channel at that specific moment and, thus, being considered as a Hold globally. Nonetheless, even in this case, a strict interleaving of Holds and Movements is always respected, as implied by Theorems 5.2 and 5.3.

Contrary to the first testing case, the second doesn't display a strict interleaving of Holds and Movements: it considers that a Hold from the right hand can occur simultaneously with a Movement of the left, thus assuming that every phoneme can be of either type or a mixture of both. In this sense, even phonemes where all articulators change simultaneously -which in the first case would have been necessarily Movements -are considered as potential Holds and, as such, may be used to check satisfaction of static

formulae. An example is shown in Figure 6.3.

In the figure, each utterance phoneme is considered as possibly having mixed information:

this is, there is no global Hold-Movement sequence, just a chain of intervals where changes could exist or not. In this manner, every phoneme can be tested equally, and no information whatsoever should be lost by the verification algorithm. Strictly speaking, individual articulation sequences remain the same as in the first case, the only difference being that the system avoids deciding globally whether an interval is of one type or other.

As a result, the verification algorithm can decide on the fly if it considers a phoneme as a Movement or a Hold, depending on the formula being tested.

One way to think about the difference between the two cases, is that the first case is very coarse-grained, as it decides if a utterance phoneme is either a Hold or a Movement by looking at the state of every articulator, globally, during its associated time-interval; in contrast, the second case is more fine-grained, as it considers phonemes to be the aggregation of varying quantities of individual articulatory information, which can be used to change their type depending on formulae.

Either way, both cases were tested with the same set of formulae; a small PDL SL description database, consisting of the three descriptions presented below: head anchor. λs.(loc(s, HEAD); moves (head active)). Either of the hands is in the head region when some change occurs and, in the end, the head location remains active. Note that skip a denotes any action in Π a , as indicated by Definition 4.10 (p. 83). The sub-formulae are defined below:

moves = skip R ∪ skip L head active = loc(R, HEAD) ∨ loc(L, HEAD) tap. λs. (λw.(no touch(s, w); moves (touch(s, w); moves (no touch(s, w)))). Either of the hands moves until they touch and, from there, either of them moves until they are not touching anymore. The no touch sub-formula is defined as follows:

no touch(s, w) = ¬touch(s, w) opposition. λc. (λs.(λw.(opposed hands(s, w) ∧ no touch(s, w) ∧ hands conf ig(c)))).

Hands are opposite to each other, holding the same configuration. Note that hands conf ig(c) is the one defined in equation 6.3 and:

opposed hands(s, w) = pos(s, ←, w)

The formulae use lambda expressions to denote all possible combinations of hand-related atomic propositions. For instance, the formula for tap considers cases where either of the hands articulated the contact or separation.

The tests where performed over a single Dicta-Sign video with the following characteristics:

-the video had a duration of 11409 frames at 25 fps (7 minutes 36 seconds);

it was manually annotated with 244 lexical glosses, where 12 were marked as "indecipherable" by the annotator;

the task consisted of performing a LSF narration of a situation contrasting "Expectation vs. Reality".

To measure the hit ratio of the system, a human counted the number of apparitions in the video of the properties described above. The quantities of Table 6.1 were contrasted with the output of the Logic Verification Module (see Chapter 5,Subsection 5.1.3,p. 120) for each verification case. The results are analyzed in the next sections.

Verification over purely static Hold phonemes

For the case where only completely static time intervals are considered Holds, the execution of the verification algorithm reported the results shown in Broadly, the results show a high recognition rate for opposition and tap (few instances were missed), but also a high quantity of false positives. Some of the erroneous opposition false positives were found in parts of the video where the signer had his arms either crossed, or resting over his knees; this is, even though the hands were correctly positioned to satisfy the formula, the video segment didn't depict signing. In other instances, it was observed that some of the false positives were due to tracking error or erroneous interval separation: for instance, in some cases Movements were the product of tracking noise which, when subdivided into minimums (see Algorithm 2, p. 105), induced the creation of "empty" segments (meaningless utterance states). This situation produced sequences of valid Holds, separated by sub-sequences of empty Holds and Movements; corresponding to changes induced by tracking noise.

Verification over non-purely static Hold phonemes

The verification results for the case where any phoneme in the utterance can be considered a Hold, are reported in The most salient characteristic of these results with respect to the previous case, comes from the quantity of glosses that the algorithm produced. The quantities in Table 6.4

show that, as the volume of possible Holds increased, the number of reported hits for opposition exploded. This was to be expected, since opposition is verified in Holds alone: in this case, as any phoneme can be considered a Hold, the quantity of testable phonemes increased, explaining the larger number false positives. On the other hand, for modal formulae, the overall number of reported positives decreased. In either case, the overall quantity of good hits remained stable, as shown by Table 6.5.

The drastic reduction of false positives in formulae with modal properties may seem counter-intuitive at first glance. However, a deeper analysis revealed that the algorithm effectively managed to discriminate and ignore some of the empty Holds during the verification process, something that was not possible on the first verification case. For example, suppose that there are two Holds h 0 , h 1 , connected by a movement m 0 , such that: U, h 0 , m 0 , h 1 |= head anchor. More precisely, suppose that U, h 0 |= loc(R, HEAD)

and that U, h 0 , m 0 , h 1 |= skip R (loc(R, HEAD)), meaning that the right hand was in the head, moved, and ended up in the head again. If the left hand introduces tracking noise (n 0 ) between the two Holds then the sequence gets subdivided either as h 0 , n 0 , h ′ 0 , m 0 , h 1 or h 0 , m 0 , h ′ 0 , n 0 , h 1 . For the first articulation case, h ′ 0 is an empty state where U, h ′ 0 |= loc(R, HEAD), thus either U, h ′ 0 , m 0 , h 1 |= head anchor or U, h 0 , n 0 , h ′ 0 |= head anchor are valid. If more noise is introduced between Holds, more false positives are detected.

However, on the second case, the same scenario would render a single result: by the PDL SL semantics, the formulae would be verified over the articulation sequence of the right hand, where no noise was introduced. Moreover, all h 0 , n 0 , m 1 and h 1 are mapped to a single transition in the articulation sequence of R (see Definition 4.18,p. 4.18), thus guaranteeing that every gloss produced from any of those phonemes is the same; hence, the quantity of false positives is reduced. The comparison of the results from both cases, is summarized in Table 6 The table shows that, in terms of overall hits, there is no real advantage from one case to the other; in fact, it suggests that some formulae could benefit from being verified over purely static Hold sequences, whereas some others would be better off in non-purely static sequences. However, due to the small size of the testing samples, it is not possible to provide strong claims on the issue without further testing both over larger corpora and with more pertinent databases. Regarding the latter, in the next section some final reflections are given about PDL SL expressiveness, and on how property databases can be created automatically from existing SL resources.

PDL SL and other SL notations

The simple database presented in the previous section, the one used to test the semiautomatic verification framework, was created manually; a human directly wrote PDL SL formulae from corpus observations. However, for the most part, this is not a straightforward task. For users unfamiliar with formal logics, building formulae like the ones proposed can be an issue, as they require a certain level of familiarity and experience.

In addition, as presented in previous chapters, several SL representation projects have been developed over the years, permitting the creation of several annotation resources that are still available to this day. For these reason, it might be important to establish a correspondence between PDL SL and other existing representation formalisms as this could:

-enable familiarization of the users towards PDL SL ; and, -provide information on how to convert one formalism into the others, permitting the automatic creation of PDL SL databases from existing resources.

To this end, in this the next paragraphs some comparisons between existing representation languages are given, providing a little insight on how they relate to PDL SL . However, the reader should know that the information provided by this section is by no means thorough; it is not intended to give construction recipes, but rather to measure informally how such a recipe may be created for different formalisms.

Synthesis languages

As reviewed in Chapter 3, the domain of SL synthesis usually requires sign representation formalisms (see Subsection 3.2.1,p. 51), in order to indicate their systems how to execute a sign. As mentioned in the aforementioned Chapter, these notations tend to be very geometric-oriented, as they have to be fairly specific about movement and articulator positioning. Because of this, some especial considerations have to be taken in account if one is to transform such descriptions into PDL SL formulae. In this subsection, some of these considerations are addressed by analyzing one of these notations in particular: ZeBeDee.

ZeBeDee

ZeBeDee is a SL representation notation, oriented towards language synthesis (see Chapter 3,Subsection 3.2.1.2,p. 54). It was developed to describe SL lexical units by way of geometric constraints and contextual dependencies: roughly, the language permits the representation of spatiotemporal relationships -between articulators or with space locations -instead of parametric characterizations, resulting in highly reusable descriptions that are neither over-specified nor under-specified. The temporal context is established by way of time-interval sequences, inspired by the phonetic model by [START_REF][END_REF]]. It is usually used in conjunction with AZee, which provides stronger expressive capabilities to the language, enabling higher level descriptions (see Chapter 3,Subsection 3.2.1.3,p. 54).

Space in ZeBeDee is of the utmost importance. As such, the formalism defines a three dimensional space around the signer, where geometrical descriptions can be provided in terms of points and vectors. As such, it is by way of spatial locations that an annotator can specify articulation places, not only on the space around the signer but also to name corporal regions; for this, ZeBeDee provides the operation Place @P at K, which assigns a name of articulation @P to a geometrical object K.

In contrast, PDL SL defines space coordinates implicitly, as they are never specifically named in the language, but rather by the defined primitives. PDL SL also establishes a three dimensional coordinate space (Ψ SL ), but it makes a clear separation between its members and their meaning, limiting the introduction of the latter to formulae. As an example, consider the set LOC a , which identifies locations for an articulator a as members of N AMES and not coordinates; from Definition 4.4, the link between names and location coordinates is given by the function C : 2 ΨSL → N AMES, which is defined for a name in N AMES only if there is a coordinate associated to it. With this in mind, PDL SL can interpret Place @P at K as "define @P in C such that C(@P) = K and

K ∈ Ψ SL ".
With respect to the name of corporal places, ZeBeDee takes as main reference both body sites and parts of the signer's skeleton. The first ones, surface body locations that the signer can touch, are denoted by the symbol @, and provide regions such as the sternum (@ST) and the like. In PDL SL , this abstraction corresponds directly to the members of the set BODY, and thus @St can be read as "ST ∈ BODY".

For the skeleton, ZeBeDee names every relevant bone (segment) individually, from the points of the fingers to the torso. In addition, the language provides a nomenclature for the right (r), left (r), dominant (s) and non-dominant (w) sides: for example, the dominant arm can be denoted as !arm(s), where the character "!" indicates that arm is part of the skeleton. Note that !arm(s) can be the same segment as !arm(r), depending how the signer is considered. In addition, ZeBeDee links body sites with skeleton segments; roughly, sites correspond to the surface of some segment.

To sum things up, a ZeBeDee description can be converted into a PDL SL formula by following the pattern presented below:

1. for each Keyposture, transform the contained information into a non-modal PDL SL formula;

2. for each Transition, transform the contained information into a A SL action formula (see Definition 4.11,p,84);

3. combine the results of this transformations into a modal PDL SL formula, respecting the sequence defined by the ZeBeDee description.

From the previous paragraphs, it has been argued that there is a straightforward correspondence between PDL SL terms, and the information described by Keypostures and Transitions. In addition, ZeBeDee is already well adapted to be parsed by way of a computer system: accordingly, the entire transformation process roughly consists of "unfolding" ZeBeDee descriptions into PDL SL formulae, which can be done automatically.

The situation is slightly different of what would happen with SL transcription notations, as these are less computer-friendly than ZeBeDee, and define parameters in a more abstract manner, as explained in the next section.

Transcription languages

More directly related to linguistic research, other representation notations are less concerned on geometrical accuracy, but rather on how to avoid information loss in SL transcription (see Chapter 3,Section 3.1,p. 42). As such, these transcription-oriented notations tend to be very symbolic, and rely on human interpretation to decode their information. Here, one notation in particular is compared to PDL SL : the Hamburg Notation System (HamNoSys).

HamNoSys

HamNoSys is a transcription notation developed to represent SL resources in written With respect to the remaining symbols, the transformation is pretty straightforward. As with ZeBeDee, HamNoSys defines a coordinate system akin to Ψ SL in PDL SL . From here, the interpretation of language statements such as orientation or location, can be defined by way of the PDL SL primitive mappings and model rules. Finally, the definition of the members of sets BODY, ART and CF G is less strict than with ZeBeDee, permitting the use of broader labels for their definition; as a matter of fact, the contents of these sets could even be denoted directly by HamNoSys symbols, as they are considered in N AMES by definition. In this regard, the only real issue comes from calculating the expected effects of actions which, as indicated, is usually a task performed by humans.

Chapter conclusion

In this chapter, an extension to the PDL SL was presented, providing a way to work with modular formulae during semi-automatic annotation tasks. The extension was used to build a simple PDL SL database which, in turn, was used to generate some practical results over the annotation framework from Chapter 5 (p. 99). In the final section, a brief analysis comparing the expressiveness of PDL SL against two different SL written notations is given; the main objective, is to show how existing SL resources could be turned into PDL SL representations, simplifying the work of building formulae databases.

Broadly, the results presented in this chapter highlight the possible pitfalls that PDL SL may encounter when applied to semi-automatic annotation. First of all, the formal language had to be extended for it to adapt to the chaotic conditions that formulae might find in practice (namely, lack of data). This was paired with a comparison of how two varying interpretations of formulae can render different results in practice, as

showcased by the two verification cases in Section 6.2. The insights gained from the examples, have helped shaping the semantics of the formal language, and opened future research possibilities based on the obtained results.

Chapter 7

Conclusions and Perspectives

This present work has introduced a formal representation for Sign Language (SL) phonology, oriented towards the development of semi-automatic annotation tasks. In particular, the proposed formalism was developed to help solving some of the common problems existing in computer-based SL research, notably:

the lack of a standard written representation for SL corpora, which forces automatic systems to work directly with raw data (such as video images);

the heterogeneity of corpus-data, which impedes the creation of large, uniform, language information repositories, thus curbing the effectiveness of machinelearning algorithms and the like; and, -the difficulty to systematically annotate video information, taking into account the variability of annotation tasks and the limited availability of SL experts to perform and correct them.

In the next paragraphs, a brief analysis is given on how the Propositional Dynamic Logic for Sign Language (PDL SL ), the proposed representation formalism, contributes to solve the above issues, alongside some perspectives of future work.

On SL corpus representation

Regarding SL representation, PDL SL provides two basic abstractions to encode SL information: logic formulae (to represent SL phonetic-phonological interactions) and graph-based utterances (to symbolize corpora). Both of them are closely related to previously existing transcription efforts, with the difference that they center on flexibility: they permit the creation of new symbols as a core feature of the language, so as to adapt to any use case in research.

With respect to corpus representation, PDL SL contributes to reduce heterogeneity by permitting the transformation of SL corpora into a well-defined graph utterances, as shown in Chapter 5 (see p. 109). Once the aforementioned transformation is done, further analysis can be executed directly over the resulting graph, without resorting to further processing over the original data; this means that if several corpora, with different technologies, are represented under the same PDL SL primitives, then any algorithm designed to analyze one of them will also work on the others. As a result, the process can potentially increase the quantity of exploitable data, regardless of the origin of each corpus.

However, there are heterogeneity-related limitations to this process. For instance, the process presented in Chapter 5, showcasing the formalization of a 2D corpus, still relies on specialized tools to generate the graph (in this case, a two-dimensional hand position tracker). If the corpus would have had motion capture data, the same process would have been performed by a different algorithm, adapted to interpret information as needed.

Despite this, when applied to recognition tasks, PDL SL presents an advantage with respect to other methods: heterogeneity is only an issue before any linguistic analysis takes place. In contrast, existing sign recognition efforts have to deal with the problem during the analysis (see Chapter 3,p. 56), limiting the application of their methods to the specific corpus for which they were created.

The same situation goes to shows how PDL SL contributes to avoid a common problem, linked to the lack of a standard written representation: recognition algorithms don't need to work on raw data, since utterance objects already represent the information contained in the video. In addition, these graphs are more expressive than transcription languages (see 6 p. 140), as they are unbounded on the quantity of information they contain.

On the other hand, unbounded information may also prove to be a disadvantage in some cases; as explained in 6, the granularity of information may affect the results of verification in recognition tasks, resulting in either too many false positives or no hits at all. These problems, called underspecification and overspecification in classical formal methods [START_REF] Bergstra | [END_REF]], oblige annotators to develop adequate rules for their use case, which is not always evident and may be subject to trial and error.

Perspectives

From a theoretical standpoint, the most natural path for future PDL SL research leads towards the analysis of articulation models; this is, the underlying structures used to produce SL utterances, as defined in Chapter 4 (see Definition 4.13 p. 85). Contrary to utterance objects, which represent only specific instances of language use, articulation models hold generalizations about the SL of interest, which makes them useful in contexts beyond annotation.

Broadly, articulation models are interesting in the sense that they may contain the basic generation rules for any SL production. Recall from Chapter 2 that SLs from different regions tend to be unique; this implies that each SL has different sets of valid parametric postures, arranged by distinct combination patterns. This would indicate that, together, all the articulation models of a single SL should be characteristic of said language or, at least, of its linguistic family; however, PDL SL doesn't yet define a way to unify these models consistently. For this reason, it may be worthy to explore how various articulation models fit together into a single structure, as it has potential applications in areas such as SL synthesis or SL recognition. For example, it may provide more accurate generation models (useful in synthesis), establish proximity measures between different SLs (useful for low-resource Natural Language Processing (NLP)) and help in the identification of patterns pertaining to linguistic phenomena (useful for recognition). They may also help to develop a formal calculus for PDL SL , grounded on the specific properties derived from a global articulation model.

Additionally, the current state of PDL SL provides a better starting point than before for the exploration of articulation models: the implementation of the semi-automatic annotation framework, has shown the potential that PDL SL -based systems have to infer articulation models from data (see Figure 6.4,p. 138), opening the door to new measures akin to those used to calculate phoneme frequencies in vocal languages.

On PDL SL -based semi-automatic annotation

From the point of view of corpus annotation, Chapter 5 presented the implementation of a semi-automatic annotation framework, based on the principles introduced by the PDL SL . The proposed system, provides a general architecture, representing the entire process from transforming a raw corpus video into an abstract representation, to the generation of a gloss proposal that can be edited by a human expert. In particular, the described system was developed to annotate Dicta-Sign corpus, using not only video data but also the results of a 2D head-hand tracker.

Notably, the annotation process is based on a database of PDL SL formulae, describing which properties are to be searched for in the graph representation of each corpus video.

The proposed algorithm, enables the automation of the annotation process, since the same database can be used seamlessly to treat different corpus videos, as long as their graph representation remains consistent. In this way, annotators can simplify the overall process by defining a single database that they can use repeatedly for each new video.

Still, this process also shows some limitations.

The principal limitation, comes from the formulae contained in the database: they are affected by similar overspecification issues like the ones mentioned in the previous section. Recall from Chapter 4 that PDL SL formulae are designed to be broad; as a result, PDL SL establishes no standards for annotation, leaving the work in the hands of human annotators. The complication comes from the fact that each expert has the liberty to describe properties following his or her own standards, which may greatly differ from any others. This means that, theoretically, there could be at least as many individual annotation templates as there are SL experts. In turn, this situation could end up mimicking the already existing problematics in annotation, since the resulting databases would only be usable on their original context, making difficult their reutilization over different corpora.

Also, even if annotation formulae were uniform across corpora, this wouldn't necessarily guarantee that a database would always be reusable without hiccups; recall that the modeling rules used to create graph representations from videos (see Chapter 5, Subsection 5.1.2, p. 109), depend on having the necessary tracking or recognition tools to determine the truth values of atoms in a corpus resource. This means that not necessarily every atom used in a formula will be detectable in every corpus, nor that they will always be correctly valued (tracking tools are prone to error, video conditions could be suboptimal, etc); both situations could influence the accuracy of the resulting annotation, regardless of the quality of the database.

Finally, the given implementation displays less-than-optimal algorithmic complexity; for the time being this is barely an issue, as the number of articulators is small enough to not represent a serious performance hit. However, the obtained values show that combinatorial explosion could rapidly become unmanageable without much effort, which could hinder the system's scalability.

Perspectives

The most pressing issue regarding the semi-automatic annotation system, is for broader capabilities to be developed into each of the existing modules, so as to try the process in other corpora. Crucially, the integration of modeling rules for the three-dimensional case is becoming a necessity, in order to widen the scope of the system; as presented in Chapter 3, various corpora are recorded with the help of motion capture devices or 3D equipment. However, this poses a number of challenges to automatic corpus analysis, starting with the interval segmentation from the Division Module. Similarly, adapting the framework to new corpora entails a reworking of the modeling and verification algorithms, in terms of optimization; remember that the calculated complexity in the Modeling (see 5.4, p. 118) and Verification (see Theorem 5.5,p. 123) modules, is by no measure small. As such, the addition of new information prone to introduce change intervals, can rapidly become unsustainable without any optimization.

On a final note, a better integration of the framework with some manual annotation mechanism is desired, as it may improve the process robustness; that is, instead of providing an output file to be edited elsewhere, it would be better for users to have direct access to the annotation in real time, to enhance the verification process as it happens. This may also help reduce the verification algorithm's complexity, which could benefit from external data to avoid systematically testing every possible state. Likewise, introducing on-the-fly corrections may also enable the use of machine learning algorithms to learn from these, dynamically improving both the modeling and verification processes.

On the empirical application of PDL SL in linguistics

Finally, something has to be said with respect to the multidisciplinary nature of this work. The presented formalism is, first and foremost, a tool. As such, the context of its intended use is to be taken in account for its development. Recall from Chapter 3, that annotation tasks in linguistics are very variable, that they respond to different research needs and they are, ideally, in constant iteration. In this regard, PDL SL formulae have properties that can enrich the corpus annotation process, such as modularity; this is, the ability to define formulas as groups of reusable blocks, as presented in Chapter 6.

In practice, modularity enables the rapid development of annotation iterations; by changing the definition of a single module, an annotator may also change every formula built with the same module, thus potentially accelerating the subsequent production of new annotation batches. This also enables the constant testing of linguistic hypotheses by way of PDL SL databases, as it becomes relatively simple to override large groups of formulae, execute the verification algorithm and compare results between executions.

Despite these advantages, cases like the ones mentioned above assume familiarity with formal tools, a domain which is not necessarily well-known in linguistics. Moreover, the complexity of specification formalisms in the spirit of PDL SL could be harrowing for the non-initiated user, which could deter researchers from their adoption. Besides, differences between research methodologies in linguistics and computer science, could give way to confusion on the use of the formal language from either domain. For these reasons, the burden of reconciling both lies on PDL SL itself, which is why special emphasis was given on developing a flexible representation language. With this, resources already in use for linguistic research (like previous annotations) can be represented as PDL SL formulae, and used by the annotation framework as reference. This is in an effort to provide SL experts with a transparent transition between their linguistic descriptions and the annotation framework, instead of trying to force them into selecting a new contender to the SL transcription arena. However, more work has to be done to achieve this goal.

Perspectives

Future work, from the point of view of multidisciplinary collaboration, is centered in the development of the necessary tools for the automatic conversion of ZeBeDee or HamNoSys descriptions, for example, into PDL SL formulae. Furthermore, it may also be useful to conduct usability tests over the annotation framework, to detect potential pitfalls induced by the system's design and not necessarily by the formalism itself.

Likewise, the development of interactive tools for the creation of PDL SL formulae could prove to be a viable alternative to the transformation from other descriptions. In this way, users could define themselves the contents of the primitive sets by way of a visual interface, and an automatic algorithm could use these definitions to calculate the appropriate modeling rules. Similarly, such a system could be fitted with a SL synthesis engine, in order to guide users into the edition of formulae: each formula could be transformed into an utterance representation -following PDL SL semantic rules -the could, in turn, be used to animate a signing avatar. With this, the expert could see in real-time how the system interprets a given formula, without having to dwell on the details of the formalism.

Finally, more collaboration with SL experts could lead to improvements to the PDL SL syntax and semantics, so as to represent properties beyond the phonetic-phonological level; however, as for now, it might be more important to evaluate which features of the formalism, as-is, are truly useful for linguistic research and which could be simplified to better suit the work in the area.

  logique formelle pour la représentation phonetique de la Langue de Signes dans des taches d'annotation semi-automatiques par Arturo Tlacaélel Curiel Díaz Cet thèse présente le développement d'un framework formel pour la représentation des Langues de Signes (LS), les langages des communautés Sourdes, dans le cadre de la construction d'un système de reconnaissance automatique. Les LS sont de langues naturelles, qui utilisent des gestes et l'espace autour du signeur pour transmettre de l'information. Cela veut dire que, à différence des langues vocales, les morphèmes en LS ne correspondent pas aux séquences de sons ; ils correspondent aux séquences de postures corporelles très spécifiques, séparés par des changements tels que de mouvements. De plus, lors du discours les signeurs utilisent plusieurs parties de leurs corps (articulateurs) simultanément, ce qui est difficile à capturer avec un système de notation écrite. Cette situation difficulté leur représentation dans de taches de Traitement Automatique du Langage Naturel (TALN).

1. 1

 1 Time-aligned lexical gloss of FSL on ELAN annotation software. Gloss is written in French. 1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.2 Example of an avatar used in SL synthesis. 2 . . . . . . . . . . . . . . . . . 1.3 Diagram depicting the proposed intermediate layer between corpora and learning tasks. Each corpus can be specified into an homogeneous representation, that can then be used to verify the existence of the required annotations. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.4 Block diagram of a semi-automatic SL annotator based on PDL SL . . . . 1.5 The resulting annotation of property BOTH on ELAN annotation tool. The intervals where BOTH was found, are shown on the third annotation track from up to bottom. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.1 In sign DATE LSF the right hand affects the left hand. 3 . . . . . . . . . . . . 2.2 Common body articulation places. 4 . . . . . . . . . . . . . . . . . . . . . 2.3 Signer articulating single-handed signs over head-located places of articulation. 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.4 Signer articulating the sign SLEEP LSF with his head, using the palm of the dominant hand as place of articulation. . . . . . . . . . . . . . . . . . . 2.5 Representation of a H-M-H sequence in the Movement-Hold Model (MHM).

  . . . 3.16 Recording setup for the Sign Language of the Netherlands (NGT) corpus [Crasborn 2008c]. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.17 Example of German Sign Language (DSG) and Dicta-Sign setup [Hanke 2010]. 65 3.18 Example of the different angles captured for the National Center for Sign Language and Gesture Resources (NCSLGR) corpus [Neidle 2000]. . . . 3.19 An schema in Z-notation representing a system for patient control in a hospital. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.20 Labeled Transition System (LTS) representing a therapy control system. 3.21 Type definitions in Vienna Development Method (VDM) specification language for a colored world map. . . . . . . . . . . . . . . . . . . . . . . 3.22 Function definitions in VDM specification language. . . . . . . . . . . . . 3.23 Definition of a Set of integers as abstract data types. . . . . . . . . . . . 3.24 Axioms for the definition of the Set of integers. . . . . . . . . . . . . . . 4.1 Spatial region contained by the set Ψ SL . 18 . . . . . . . . . . . . . . . . . 4.2 Representation of articulation sequence S a for changes in articulator a ∈ ART . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.3 Representation of a case where a utterance object synchronizes three articulation sequences. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.1 Block diagram of a generic PDL SL -based SL lexical structure recognition system . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.2 Block diagram of a generic PDL SL -based SL lexical structure recognition system . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.3 Example of a Dicta-Sign raw video sequence. . . . . . . . . . . . . . . . . 5.4 Example of an interval segmentation for the right hand; the intervals below the image denote which frames are contained in the segment. . . . . 5.5 Example of two parallel per-articulator segmentations. . . . . . . . . . . 5.6 Calculated path of hands and head on a corpus video. . . . . . . . . . . 5.7 Example of an interval segmentation for the right hand; the intervals below the image denote which frames are contained in the segment. . . . 5.8 Example of an interval segmentation for the right hand. The intervals sequences below the graph denote the results produced by each algorithm. The graph depicts the speed changes of the right hand, over a video segment.108 xv 5.9 Block diagram of a generic PDL SL -based SL lexical structure recognition system . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.10 Primitive set templates in PDL SL . . . . . . . . . . . . . . . . . . . . . . 5.11 Possible places of articulation in LOC common to both hands. . . . . . 5.12 Some LSF hand configurations. . . . . . . . . . . . . . . . . . . . . . . . 5.13 The signer's point of view, used to define Ψ SL . . . . . . . . . . . . . . . . 5.14 The information about the signer's posture above is captured by the following atomic propositions, which are true for this image: pos(R, ←, L), pos(L, →, R), loc(R, HEAD), loc(L, HEAD), cfg(R, CLAMP), cfg(L, CLAMP), touch(R, L). . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.15 Atomic actions ← R and → L are true in the above image. . . . . . . . . 5.16 Articulator segmentations for the right and left hands. . . . . . . . . . . . 5.17 Transformation of interval segments into utterance phonemes. . . . . . . 5.18 Example of the different layers processed by an automatic annotation system120 5.19 Block diagram of a generic PDL SL -based SL lexical structure recognition system . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.20 An iconic depiction of a thin and long object, and its corresponding utterance representation. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.21 Example of a resulting gloss. . . . . . . . . . . . . . . . . . . . . . . . . 5.22 Block diagram of a generic PDL SL -based SL lexical structure recognition system . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.23 Example of a resulting gloss. . . . . . . . . . . . . . . . . . . . . . . . . 5.24 Information and control flow in the SL annotation framework . . . . . . 6.1 Comparison of signs SCREEN LSF and DRIVE LSF sharing the same underlying structure. 19 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6.2 First Case: Considering only "True" Holds. . . . . . . . . . . . . . . . . 6.3 Second Case: Considering Holds and Movements simultaneously. . . . . 6.4 Depiction of the inferred articulation model from one video. . . . . . . . Chapter 1

  (e.g. position and size classifiers), spatialization cues (e.g. pointing signs) and culturally influenced gestures (e.g. proper names) [Chen Pichler 2010, Johnston 2010]. Glosses can also be created individually for hands and NMF. Nowadays, researchers use specialized multimodal annotation software like ELAN [Wittenburg 2006]. These tools permit the creation of time-aligned glosses, over corpora with more than one communication modalities such as speech, facial expression, hand configuration and others. They let users select a relevant time-interval, for example when a sign occurs, and mark it with a gloss note. Notes can be arranged into tracks, each track representing a different gloss type. Figure 1.1 shows an snapshot of ELAN during the creation process of a lexical gloss for a French Sign Language (LSF) corpus.

Figure 1

 1 Figure 1.1: Time-aligned lexical gloss of FSL on ELAN annotation software. Gloss is written in French. 1

Figure 1 . 2 :

 12 Figure 1.2: Example of an avatar used in SL synthesis.2

Figure 1 . 3 :

 13 Figure 1.3: Diagram depicting the proposed intermediate layer between corpora and learning tasks. Each corpus can be specified into an homogeneous representation, that can then be used to verify the existence of the required annotations.

Figure 1 . 4 :

 14 Figure 1.4: Block diagram of a semi-automatic SL annotator based on PDL SL .

Figure 1 . 5 :

 15 Figure 1.5: The resulting annotation of property BOTH on ELAN annotation tool. The intervals where BOTH was found, are shown on the third annotation track from up to bottom.

Figure 2 . 1 :

 21 Figure 2.1: In sign DATE LSF the right hand affects the left hand.4

4

 4 Figure 2.1: In sign DATE LSF the right hand affects the left hand.4

Figure 2 . 2 :

 22 Figure 2.2: Common body articulation places.5

4 .

 4 Images obtained from [Sématos 2013]. 5. Corpus image obtained from Dicta-Sign project [Matthes 2012].

Figure 2 . 3 :

 23 Figure 2.3: Signer articulating single-handed signs over head-located places of articulation. 6

Figure

  Figure 2.4.

6 .Figure 2 . 4 :

 624 Figure 2.4: Signer articulating the sign SLEEP LSF with his head, using the palm of the dominant hand as place of articulation.

Figure 2 . 5 :Figure 2 . 6 :

 2526 Figure 2.5: Representation of a H-M-H sequence in the MHM. Holds H A and H B are characterized by postures A and B, respectively. The movement between holds is a transition from postures A to B.

Figure 2 . 9 :

 29 Figure 2.9: Spatialization of FRIEND LSF to the right of the signer.

  Figure 2.11: TREE LSF is an example of an iconic sign.

  Figure 2.13 shows an example of role shifting, where the signer narrates a story about a fire and takes the role of a firefighter breaking a door.

Figure 2 . 13 :

 213 Figure 2.13: The signer shifts roles to narrate his story from the point of view of a firefighter.

Figure 2 . 14 :

 214 Figure 2.14: Hand configurations used in ASL. 11

Figure 2 . 15 : 3 .

 2153 Figure 2.15: Hand orientation vector with respect to the palm.

4 .

 4 Hand movement.-Indicates the characteristics of hand motion. These can be as simple as straight movements like the ones shown in Figure2.16, or as complex as irregular trajectories describing the physical form of an object. This parameter also takes in account salient movement characteristics such as speed or acceleration.

Figure 2 . 16 :

 216 Figure 2.16: Subset of the possible movements a hand can execute during signing. 12

  are recurrent issues in the area, showing that the domain is still finding its footing. Thus, a lot of effort has been put into studying SL representation across different domains, since it has become apparent that it may be a crucial part of corpus-based SL research. This chapter presents the existing state of the art for computer-based SL processing. The first half introduces the current research efforts related to the domain, seen from the point of view of SL research; the second half, presents some of the computer science tools on which the contributions of this dissertation are based. With this in mind, the next sections introduce some of the most common SL transcription systems used in linguistic research. Moreover, Sections 3.2 and 3.3 give a brief introduction to SL synthesis and SL recognition, respectively, showing how representation needs may change between different research efforts. Finally, Section 3.4 gives a brief introduction to formal methods, presenting how systems engineering deals with representation issues in the development of industrial applications, always following well-established patterns despite the fact that application domains may differ from one another.

  SL representation research, consist in the development of formal notation systems for the transcription of SL utterances. These notations can range from written SL systems, to phonetic transcription languages. Currently, several representation notations exists for different objectives, but neither of them can be considered as standard in their respective domains of application. Nonetheless -and regardless of their intended use -most of the existing SL representations share various common characteristics, reflecting the importance of capturing the underlying articulation parameters (see Chapter 2, section 2.2, p. 24) as accurately as possible.

Figure 3 . 1 :

 31 Figure 3.1: Subset of Stokoe Notation symbols. 1

Figure 3 .

 3 Figure 3.2: SNAKE ASL in Stokoe Notation.

  200 characters, intended to represent a wide range of parametric postures in several SL. The symbols defined by HamNoSys are more iconic than those by Stokoe. For instance, the representation of hand configurations and places of articulation retain a visual relation with the actual morphological characteristics of the human body. Figure 3.3 shows some of the characters used by HamNoSys to represent common places of articulation and hand configurations.

Figure 3 . 3 :

 33 Figure 3.3: Iconic places of articulation and hand configurations in HamNoSys.2

Figure 3 . 4 :

 34 Figure 3.4: HAMBURG DSG in HamNoSys.3

Figure 3 . 5 :

 35 Figure 3.5: Movement and direction symbols in HamNoSys.4

4

 4 Figure 3.5: Movement and direction symbols in HamNoSys.4

Figure 3 . 6 :

 36 Figure 3.6: A SignWriting glyph describing a posture where the signer's dominant hand touches ( * ) the head (•), while holding a POINTING configuration. 5

Figure 3 . 8 :

 38 Figure 3.8: SignWriting places of articulation and their possible modificators.6

Figure 3 . 9 :

 39 Figure 3.9: SignWriting hand configurations.7

Figure 3 .

 3 Figure 3.10: SignWriting vertical and horizontal movements.8

Figure 3 .

 3 Figure 3.11: Sign ADDRESS LSF represented in SignWriting. 9

  9. Signer image obtained from [Sématos 2013] and SignWriting description obtained from[Sutton 2010].

Figure 3 .

 3 Figure 3.14: Zebedee description for BALLOON LSF .

Figure 3 .

 3 Figure 3.15: Two very close LSF hand configurations. 10

Figure 3 .

 3 Figure 3.16: Recording setup for the NGT corpus [Crasborn 2008c].

Figure 3 .

 3 Figure 3.17: Example of DSG and Dicta-Sign setup [Hanke 2010].

Finally

  , the Dicta-Sign project resulted in the development of new corpus-based research, showcased by the production of several proofs-of-concept in the areas of web communication for the Deaf [Efthimiou 2012b], SL synthesis applied to human-computer interfaces [Efthimiou 2012a] and isolated sign recognition on lexical databases [Elliott 2012]. Similar long-term non-European efforts are represented by projects like the National Center for Sign Language and Gesture Resources (NCSLGR) corpus of ASL [Neidle 2000]. For their work, the researchers captured a database of 1866 distinct signs, performed by four native signers, summing up to 11,854 total sign occurrences on video. Capture was achieved by way of four standard definition cameras (no HD), positioned to capture orthogonal planes of the participants. An example is shown in figure 3.18.

Figure 3 .

 3 Figure 3.18: Example of the different angles captured for the NCSLGR corpus [Neidle 2000].

Figure 3 . 19 :

 319 Figure 3.19: An schema in Z-notation representing a system for patient control in a hospital.

Figure 3 .

 3 Figure 3.20: LTS representing a therapy control system.

Figure 3

 3

Figure 3 .

 3 Figure 3.21: Type definitions in VDM specification language for a colored world map.

Figure 3 .

 3 Figure 3.22: Function definitions in VDM specification language.

Figure 3 .

 3 Figure 3.23: Definition of a Set of integers as abstract data types.

Figure 3 .

 3 Figure 3.23 gives the signatures of an empty set (mapping {ǫ} to a Set), operators closed under Set for insertions and deletions, and the signature of an operator which determines if an integer is member of a Set. The axioms defining the semantics are given in Figure3.24.

Figure 3 . 24 :

 324 Figure 3.24: Axioms for the definition of the Set of integers.

Definition 3 . 2 (

 32 Algebraic operators of CSP). P ::= a → P | P Q | P ⊓ Q | P |||Q | P ||{a}||Q | P \{a} where:

Definition 4 . 1 (

 41 Relevant body parts for SL). Let N AMES be the set containing all possible chains of characters. The set of relevant body parts is defined as BODY = {b : b denotes a body part visible during signing; b ∈ N AMES}. Intentionally, the set BODY has a very broad definition; the relative importance of different body parts may change between SLs, for which it becomes useful to have a very general characterization. As a result, annotators have enough liberty to specify whatever they need, depending on the language properties they are describing. The same can be done for SL articulators, as shown in definition 4.2. Definition 4.2 (Articulators). Let ART denote the set of SL articulators, where ART = {a : a ∈ BODY and a is capable of articulation}.

Definition 4 . 3 (

 43 Space coordinates). Let the set Ψ SL ⊂ R × R × R contain all possible three-dimensional euclidean coordinates taking the signer's center of mass as origin, such that for every p ∈ Ψ SL :-a signer can physically reach point p with any articulator a ∈ ART ; the space on p can become empty at any given time; that is, that no body part named by b ∈ BODY locates in p.Roughly, the set Ψ SL contains the spatial region depicted on Figure4.1, which can be activated by signers on discourse. However, this definition is too general, as it also contains regions lacking of linguistic meaning, not used on signing. Definition 4.4 solves this issue, by defining places of articulation under articulatory restrictions.

Figure 4 . 1 :Definition 4 . 4 (

 4144 Figure 4.1: Spatial region contained by the set Ψ SL . 1

Definition 4 . 5 (

 45 (i.e. raised/lowered eyebrows, open/closed eyes, etc). The definition of configurations under this principle, is given below. Articulator configurations). Let CF G a be the set naming every possible morphological configuration that the articulator denoted by a ∈ ART can hold. Notably CF G a ⊂ N AMES and CF G a ∩ BODY = ∅. Finally, the set CF G contains all valid pairings of articulators and configurations, such that CF G = {(a, c) : a ∈ ART and c ∈ CFG a }.

Definition 4 . 6 (

 46 Set of directions). Let ∆ ⊆ Ψ SL × Ψ SL be the set containing every pair of coordinates in Ψ SL ; for each pair (A, B) ∈ ∆, where A, B ∈ Ψ SL , the symbol # » AB will denote the vector going from coordinate A to B.

Definition 4 . 7 (

 47 Labeling function for ∆). Let DIRECT ION S ⊂ N AMES be the set of direction names, such that DIRECT ION S ∩ BODY = ∅ and, for any a ∈ ART , DIRECT ION S ∩ CFG a = ∅. The mapping L ∆ : 2 ∆ → DIRECT ION S denotes the labeling function taking groups of vectors in ∆ to a name in DIRECT ION S; that is, L ∆ assigns a single name to a set of vectors defining a direction. The labeling function of Definition 4.7 can be used to populate yet another set, containing information of linguistic interest for sets of vectors. Definition 4.8 (Set of relevant directions for SL). The set of relevant directions for SL is defined as follows:

  articulation model, corresponding to a LTS of Holds connected by possible Movements with their outcomes. The formal definition is presented below. Definition 4.13 (Sign Language Articulation Model ). Let a ∈ ART be an articulator, the articulation model of a (M a ) is a tuple M a = (S, R, • Φ a , • Π a ) where:

Figure 4

 4 Figure 4.2.

Figure 4 . 2 :

 42 Figure 4.2: Representation of articulation sequence S a for changes in articulator a ∈ ART .

  to be interpreted as the set {m, m + 1, m + 2, . . . , n -1}, m, n ∈ N and m < n where the square bracket next to the m indicates that m ∈ I, while the parenthesis next to the n indicates that n ∈ I. Similarly, two intervals overlap if the sets have numbers in common. For example, intervals [m, k) and [k, n) don't overlap, whereas intervals [1, k] and [k, n) do (they have k in common). Finally, interval [m, m] is defined, whereas [m, m) and (m, m] are not. Intuitively, timed articulation sequences induce a chain of strictly ordered intervals, which is proven below.Lemma 4.1. Let Ŝa = (S a , T a ) be a timed articulation sequence; T a induces a strict interval order over states and transitions represented by S a .

Figure 4 . 3 ,

 43 shows the visual representation of a utterance U, for three articulators.In the figure, the bottom part shows the chain of states representing utterance phonemes, aligned with the interval segments to which they correspond. Just above, a representation of the individual sequences contained in SEQ is given for three articulators a 1 , a 2 , a 3 ∈ ART ; furthermore, each state and transition represented in SEQ has marked the phonemes in P to which they correspond.

Figure 4 . 3 :

 43 Figure 4.3: Representation of a case where a utterance object synchronizes three articulation sequences.

Corollary 4 . 1 .

 41 For utterance U = (P, T U , • U , SEQ), each phoneme p N ∈ P overlaps with a single interval of the chain induced by T a , where Ŝa = (S a , T a ) ∈ SEQ.

Theorem 4 . 4 (

 44 Utterance phoneme to transition correspondence). Let U = (P, T U , • U , SEQ) be an utterance and Ŝa denote a timed articulation sequence of a ∈ ART . For every Ŝa = (S a , T a ) ∈ SEQ and for each transition (s k , s k+1 ) ∈ Ŝa , there exist a p N ∈ P in the phoneme sequence such that (s k , s k+1 ) Π a ⊆ p N U .

Corollary 4 . 2 .Corollary 4 . 3 .

 4243 For every Ŝa = (S a , T a ) ∈ SEQ and for each transition (s k , s k+1 ) ∈ Ŝa , there exist a p N ∈ P in the phoneme sequence such that s k+1 Φ a ⊆ p N U . Phonemes in U induce a total order over transitions in SEQ.

Lemma 4 . 5 (

 45 Number of states in U). Let n denote the total number of transitions in all sequences of SEQ. Utterance U assigns, at most, 2n + 1 phonemes to represent all the information in SEQ.

Figure 5 . 1 :

 51 Figure 5.1: Block diagram of a generic PDL SL -based SL lexical structure recognition system

Figure 5 . 2 :

 52 Figure 5.2: Block diagram of a generic PDL SL -based SL lexical structure recognition system

Figure 5 . 3 :

 53 Figure 5.3: Example of a Dicta-Sign raw video sequence.

Figure 5 .

 5 4 shows an interval segmentation for the raw video.

Figure 5 . 4 :

 54 Figure 5.4: Example of an interval segmentation for the right hand; the intervals below the image denote which frames are contained in the segment.

Figure 5 . 5 :

 55 Figure 5.5: Example of two parallel per-articulator segmentations.

Figure 5 . 6 :

 56 Figure 5.6: Calculated path of hands and head on a corpus video.

Figure 5 . 7 :

 57 Figure 5.7: Example of an interval segmentation for the right hand; the intervals below the image denote which frames are contained in the segment.

Figure 5 .

 5 Figure 5.7, shows a plot of per-articulator speed changes, occurring from frame 2916 to frame 2930 on a Dicta-Sign video. Observe that not only does the speed of the head remains fairly unchanged, but is always below the noise threshold (even in frames where

Theorem 5 . 1 (

 51 Interleaved segmentation). The result of the execution of Algorithm 1,for any of the hands, is a list L either containing a series of interleaved static and change intervals or a single static interval.

1:

  procedure SubSegmentation(I k = a change interval [m, n]) 2: if m = n or |I k | < 3 then

  Change interval subdivision). Executing Algorithm 2 over a change interval I k , produces an interval chain L c where, either |L c | = 1 and I k ∈ L c or |L c | ≥ 3 and L c is an interleaving sequence of minimum speed intervals and change intervals. Proof. By induction, over the length if I k . If |I k | < 3 then, by line 2 in the algorithm, it holds. For |I k | = 3, where I k = [i -1, i, i + 1]. By line 5, there is a variable I such that I = {i -1}. The for of line 7 centers in i and compares the speeds of each frame denoted by I

  then by line 16 we have that I = {. . . , N -1}. Since this is the last execution of the for, the algorithm executes lines 19 and 20 giving I = {. . . , N -1, N } and L c = (. . . , {. . . N -1, N }) is returned. Note that, in this case, neither N -1 nor N can be minimums, since frame N + 1 is static and, hence, v N > v N +1 = 0. Thus L c holds.

  each subinterval I s ∈ SubSegmentation(I) do 11: L s .add(I s )

Figure 5 . 8 :

 58 Figure 5.8: Example of an interval segmentation for the right hand. The intervals sequences below the graph denote the results produced by each algorithm. The graph depicts the speed changes of the right hand, over a video segment.

Figure 5 . 9 :

 59 Figure 5.9: Block diagram of a generic PDL SL -based SL lexical structure recognition system

Figure 5 . 10 :

 510 Figure 5.10: Primitive set templates in PDL SL

Definition 5 . 4 (

 54 Places of articulation for 2D corpora). Recall that BODY a denotes the containing body-bound locations where a can articulate. For articulators R, L ∈ ART , it is the case that:BODY L = BODY/{L} BODY R = BODY/{R}Recall the labeling C : 2 ΨSL → N AMES, mapping space regions to names, from Definition 4.4. The inverse function, C -1 : N AMES → 2 ΨSL , takes members of N AMES to space regions. Let the set REGION S = {C -1 (NEUTRAL), C -1 (RIGHT HEADSIDE), C -1 (LEFT HEADSIDE)} denote a group of spatial regions. Articulation places are given as follows: LOC L = {λ : λ ∈ (BODY L ∪ r∈REGION S C(r))} LOC R = {λ : λ ∈ (BODY R ∪ r∈REGION S C(r))} LOC remains the same as in Definition 4.4.

Figure 5 .

 5 Figure 5.11: Possible places of articulation in LOC common to both hands.

Definition 5 . 5 (

 55 Articulator configurations for 2D corpora). For R, L ∈ ART , configurations are given as follows:CF G R = CF G L = {INDEX,PINCE, FIST, PALM, . . .} CF G remains the same as in Definition 4.5. In general, the names included in CF G correspond each to a possible hand-configurations in LSF, some of which are depicted in Figure 5.12. LSF hand-configurations where chosen because the tests were based on the LSF portion of Dicta-Sign. Nevertheless, just as with the other sets, the contents of the set largely depend on the annotator, and are by no means limited by what is shown on the figure.

Figure 5 .Definition 5 . 6 (

 556 Figure 5.12: Some LSF hand configurations.

  the rest of the names in DIRECT ION S, similar definitions were made in ∆ SL . Note that, by convention, directions are interpreted from the signer's point of view; also, Ψ SL is centered on the signer's body. An diagram exemplifying the selected point of view is shown on Figure 5.13.

Figure 5 .

 5 Figure 5.13: The signer's point of view, used to define Ψ SL .

Definition 5 . 7 (

 57 Atomic propositions for 2D corpora). The set Φ a of atomic propositions for articulator a ∈ ART is defined as: Φ a = {pos(a, δ, b), loc(a, λ), touch(a, b), cfg(a, c)} where a, b ∈ ART , δ ∈ DIRECT ION S, λ ∈ LOC a and c ∈ CFG a . Intuitively: pos(a, δ, b).-Recall the function L ∆ from Definition 4.7. This atom asserts that hand a is located on position δ with respect to b; this is, there exist a vector # » BA ∈ L -1 ∆ (δ) such that a is positioned in coordinate A and b is positioned in coordinate B. loc(a, λ).-Indicates that hand a articulated in location λ. touch(a, b).-Is the same as loc(a, b), where b is a hand such that b ∈ LOC a and b ∈ ART . cfg(a, c).-Hand a holds configuration c.The set Φ is the same as in Definition 4.9.An example of how atomic propositions assert information about a video segment, is presented in Figure5.14.

Figure 5 .

 5 Figure 5.14: The information about the signer's posture above is captured by the following atomic propositions, which are true for this image: pos(R, ←, L), pos(L, → , R), loc(R, HEAD), loc(L, HEAD), cfg(R, CLAMP), cfg(L, CLAMP), touch(R, L). . .

Figure 5 .

 5 Figure 5.15: Atomic actions ← R and → L are true in the above image.

Figure 5 .

 5 Figure 5.16: Articulator segmentations for the right and left hands.

Definition 5 . 9 (

 59 Modeling rule). Let Φ and Π be the sets of atomic propositions and actions. A modeling rule is a function R : (Φ ∪ Π) × (N × N) → {⊤, ⊥}, taking proposition and time intervals to truth values.

Algorithm 4

 4 Transformation of interval segments into utterance objects 1: procedure UtteranceConstruction(L 0 , . . . , L n , R) for each segmentation list L a ∈ (L 0 , . . . , L n ) do 4: let M a = (S, R, • Φ a , • Π a ) be an empty articulation model of a.

6 : 4 (

 64 for each change interval I i ∈ L do 7:let I i-1 and I i+1 be the static intervals before and after I i 8: create two states s i-1 and s i+1 in M a 9:assert (s i-1 , s i+1 ) ∈ R in M a 10: for each atom proposition p a ∈ Φ a do 11: if R(p a , I i-1 ) then 12: assert p a ∈ s i-1 Φ a action π a ∈ Π a do 19: if R(π a , I i ) then 20: assert π a ∈ (s i-1 , s i+1 ) i-1 , s i+1 ) to Ŝa 24: assert I i ∈ T a ((s i-1 , s i+1 ))in Ŝa 25: Modeling Complexity). Creation of the U object takes O(n) time. Proof. For the n detected change interval, from every articulator, the algorithm: -adds two vertex to the graph M a in O(1) time; -adds an edge to the graph M a in O(1) time; -performs a constant number of comparisons, for the members of Π and Φ in O(1) time; -performs one insertion to a list Ŝa in O(1) time; -performs one insertion to a lookup table T a in O(1) time; thus the complexity is roughly O(n).

Finally

  , from Lemma 4.5, utterance labeling takes up to O(2n + 1) time, thus the overall complexity remains bounded by O(n).

Figure 5 .

 5 Figure 5.17: Transformation of interval segments into utterance phonemes.

Figure 5 .

 5 Figure 5.17 presents the induced utterance object for two interval segmentations. In the two sequences, each of the intervals is marked with the propositional information inferred by the given modeling rules. The end result, the utterance object U above, is time-aligned with interval changes, as it was created from two timed articulation sequences based on the given segmentation; in essence, the depicted graph corresponds to the abstract representation of a video-segment, as shown on the bottom of the image. A simplified representation of the results of both the Division and Modeling modules together is shown in Figure 5.18.

Figure 5 .

 5 Figure 5.18: Example of the different layers processed by an automatic annotation system

Figure 5 .

 5 Figure 5.19: Block diagram of a generic PDL SL -based SL lexical structure recognition system

Figure 5 .

 5 Figure 5.20: An iconic depiction of a thin and long object, and its corresponding utterance representation.

6 : 5 (

 65 if U, p ij |= ϕ then 7:Gloss.add((ϕ, p ij )) Verification Complexity). For n interval changes and m formulae in DB, the algorithm takes O(m • n 2 ) time.Proof. Assuming line 7 takes O(1) time; the algorithm tests m formulae, in every phoneme of the U. From Lemma 4.5, we know that 2n + 1 phonemes are enough to capture all information in SEQ, thus we have at most O(m•2n+1). However, by line 5 we know that the algorithm tries to obtain the largest j such that i ≤ j at every state. Since utterances are capped to 2n + 1 phonemes, it is safe to assume that the longest possible j decreases in 1 on each iteration. Thus, the total number of comparisons can be O(m • (2n+1)(2n+2) 2 ) on the worst case. Simplified, this formula gives us O(m • (2n 2 + 3n + 1)), which is bounded by O(m • n 2 ). Algorithm 5 takes each phoneme p i ∈ U and tests it against each formulae ϕ ∈ DB,

Figure 5 .

 5 21 shows an example.

Figure 5 .

 5 Figure 5.21: Example of a resulting gloss.

Figure 5 .

 5 Figure 5.22: Block diagram of a generic PDL SL -based SL lexical structure recognition system

Figure 5 .

 5 Figure 5.23: Example of a resulting gloss.

Figure 5 .

 5 Figure 5.24: Information and control flow in the SL annotation framework

For a simpleFigure 6 . 1 :

 61 Figure 6.1: Comparison of signs SCREEN LSF and DRIVE LSF sharing the same underlying structure. 1

Figure 6 .

 6 Figure 6.1 shows two French Sign Language (LSF) signs: SCREEN LSF and DRIVE LSF . Both signs share the same underlying structure, characterized by both hands holding the same morphological configuration, while being spatially positioned opposite from one another.An annotator searching for every sign with the same underlying structure, where only hand configurations differ, can use a lambda expression to build a formula like the one presented in Example 6.1.1. Corpus images obtained from Dicta-Sign project[START_REF] Matthes | [END_REF]].

Example 6 .

 6 1 (opposition lambda expression). opposition = λc.(pos(R, ←, L) ∧ cfg(R, c) ∧ cfg(L, c))

Example 6 . 3

 63 (opposition-derived signs).SCREEN LSF = opposition(L FORM) DRIVE LSF = opposition(FIST FORM) where L FORM, FIST FORM ∈ CFG R ∩ CFG L .In the example, L FORM denotes the morphological configuration of the hand where the thumb and the index fingers are held orthogonally (see Figure6.1). Similarly, FIST FORM denotes the configuration where the hand forms a fist. In general, opposition(L FORM) and opposition(FIST FORM) are two new formulae, interpreted by the system as being sub-formulae in opposition corresponding to configurations L FORM and FIST FORM, respectively.

Figure 6 . 2 :

 62 Figure 6.2: First Case: Considering only "True" Holds.

Figure 6 . 3 :

 63 Figure 6.3: Second Case: Considering Holds and Movements simultaneously.

Finally, during the

  algorithm's execution, a global articulation model (see Definition 4.13, p. 85) was inferred from the detected Holds and Movements. The result is shown in Figure 6.4.The graph in Figure6.4 displays a total amount of 205 states, representing all the static phonemes that were calculated during utterance creation. Overall, each state corresponds to a Hold phoneme that the signer depicted throughout the video sequence. Holds are connected between each other by 739 edges, representing all detected Movements in the video, produced by any of the articulators. From the annotation results, it is safe to assume that some of the depicted Movements were induced by tracking noise. Similarly, some of the Holds necessarily correspond to meaningless postures (like when the signer crossed his arms), or may be the product of small changes induced either by noise or by the choice of segmentation thresholds. All the same, the diagram goes on to show that, globally, the number of complex interactions is very high, thus producing a large number of empty Holds. In this view, verification based on non-purely static Hold phonemes may represent an advantage; in theory, it may provide a way to avoid verification over the empty Holds, based on ignoring information that could had been induced by tracking or thresholding noise.

Figure 6 . 4 :

 64 Figure 6.4: Depiction of the inferred articulation model from one video.

form (see Chapter 3 ,

 3 Subsection 3.1.2 p. 44). In general, HamNoSys captures signs' features by providing an initial parametric posture and a sequence of actions affecting said posture. To this end, the language provides a series of symbols representing places of articulation, hand configurations, orientation and Non-Manual Features (NMFs).PDL SL and HamNoSys share the same basic principle; just as HamNoSys, the logic permits establishing a departure posture and denoting modifications over it. However, unlike HamNoSys, modal PDL SL formulae explicitly express how the resulting posture should look (posture; [action](result)), whereas HamNoSys actions' results are left implicit. Mainly, this is because the semantics of HamNoSys symbols are broader than those defined in PDL SL : they contain more information than a PDL SL atom.For example, observe the action ↓ R ∈ Π R , defined for the study of 2D corpora. The meaning of the action is linked to a phoneme in a utterance graph (see Definition 4.17), where the y position of the right hand decreases monotonically while the x position remains unchanged. Further information about the right hand has to be asserted elsewhere, with other atoms. In contrast, the HamNoSys symbol implicitly accounts for the hand's location, position and, if a concatenation of symbols exist, even the path it follows.As a result, in order to be able to transform HamNoSys strings into PDL SL formulae, a mechanism to calculate postures by the successive application of actions is required.This hints to the development of a PDL SL calculus, based on morphological rules about the movement of the human body. Otherwise, the alternative is to delve into the creation of thorough articulation models in the spirit of the one presented on Figure6.4; in this case, the idea would be to interpret the initial HamNoSys posture, find it in a graph representing an articulation model and, from there, determine the resulting state by the application of the specified actions. Once the end state is found, the resulting posture can be encoded as a PDL SL formula.

  Recall fromChapter 5 (p. 104), that the Division Module selects video sequences based solely on tracking information. Thus, it is safe to assume that the introduction of an additional spatial dimension would, for better or worse, modify the results calculated by the module. The same case can be made for any additional tracking or recognition information like hand-configuration, Non-Manual Features (NMFs) or body posture: the basis of the segmentation is the identification of changes, and new data may affect what the module considers a change. In brief, this means that any segmentation based in raw data requires a careful examination of the possible outcomes, suggesting the need for new linguistic research regarding phoneme identification under varying conditions.

  . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.13 The signer shifts roles to narrate his story from the point of view of a firefighter. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.14 Hand configurations used in American Sign Language (ASL). 6 . . . . . 2.15 Hand orientation vector with respect to the palm. . . . . . . . . . . . . 2.16 Subset of the possible movements a hand can execute during signing. 7 . 3.1 Subset of Stokoe Notation symbols. 8 . . . . . . . . . . . . . . . . . . . . 3.2 SNAKE ASL in Stokoe Notation. . . . . . . . . . . . . . . . . . . . . . . . . 3.3 Iconic places of articulation and hand configurations in Hamburg Notation System (HamNoSys). HAMBURG DSG in HamNoSys. 10 . . . . . . . . . . . . . . . . . . . . . . . . 3.5 Movement and direction symbols in HamNoSys. 11 . . . . . . . . . . . . 3.6 A SignWriting glyph describing a posture where the signer's dominant hand touches ( * ) the head (•

	List of Figures	xiv
	3.4
	xiii

9 . . . . . . . . . . . . . . . . . . . . . . . . . . . .

  . . . . . . . . . . . . . . . . . . . . . 3.10 SignWriting vertical and horizontal movements. 15 . . . . . . . . . . . . . 3.11 Sign ADDRESS LSF represented in SignWriting. 16 . . . . . . . . . . . . . . 3.12 STEP code for a given hand configuration. . . . . . . . . . . . . . . . . 3.13 SiGML description of the sign SCOTLAND BSL in British Sign Language (BSL). 3.14 Zebedee description for BALLOON LSF . . . . . . . . . . . . . . . . . . . . . 3.15 Two very close French Sign Language (LSF) hand configurations. 17

Table 3 . 1 :

 31 Quantity of recognizable signs by research project.

  reason, it is useful to give semantics of PDL SL formulae in terms of timed articulation sequences, as shown in Definition 4.16.

Definition 4.16 (PDL SL formulae satisfaction over timed articulation sequences). Let Ŝa be a timed articulation sequence and let M a = (S, R, • Φ a , • Π a ) be the articulation model inducing S a ∈ Ŝa . Also, let ϕ and ψ be PDL SL formulae and p a ∈ Φ a . The semantics of the non-modal PDL SL operators on Definition 4.12, are given as follows:

  By contradiction. Suppose that T U (p N ) = [t i , t j ) overlaps with two adjacent intervals T a (s k ) and T a (s k+1 ). By Lemma 4.1, it is safe to assume that T a (s k ) = [t x , t y ) and T a ((s k , s k+1 )) = [t y , t z ). An overlapping exists if and only if t i ∈ [t x , t y ) and there exist some t ′ ∈ [t i , t j ), such that t i < t y ≤ t ′ ≤ t z-1 . Note that t y is the starting time ′ will be delimited by t i < t ′ < t y , thus implying that T U (p N ) doesn't overlap with T a ((s k , s k+1 )) = [t y , t z )! Lemma 4.3. Let U = (P, T U , • U , SEQ) be an utterance. For each phoneme p N ∈ P, and any sequence Ŝa = (S a , T a ) ∈ SEQ, utterance interval T U (p N ) won't overlap with two non-adjacent intervals in the chain induced by T a . Proof. By contradiction, suppose that T U (p N ) = [t i , t j ) overlaps with two non-adjacent intervals T a ((s k-1 , s k )) and T a (s k , s k+1 ), separated by interval T a (s k ). Note that

Lemma 4.2. Let U = (P, T U , • U , SEQ) be an utterance. For each phoneme p N ∈ P, and any sequence Ŝa = (S a , T a ) ∈ SEQ, utterance interval T U (p N ) won't overlap with two adjacent intervals in the chain induced by T a . Proof.

of a new transition in SEQ; by Definition 4.17, interval T U (p N ) can be only as long as T U (p N ) = [t i , t y ), which occurs when t y is the first transition change after t i . Implicitly, this means that every t

  where s k is a state common to two adjacent transitions (s k-1 , s k ), (s k , s k+1 ) ∈ Ŝa . Utterance phonetic parameters). Let U = (P, T U , • U , SEQ) be an utterance and p N ∈ P be a phoneme labeled with time interval T U (p N ). Let Ŝa ∈ SEQ be the timed articulation sequence in U corresponding to articulator a ∈ ART , while

	Note that Corollary 4.1 guarantees that T U (p N ) overlaps with either a single transition,
	or a single state.
	Definition 4.19 (

Table 4 .

 4

1: Summary of SL primitives and atoms for PDL SL

  4 (see Section 4.2 p. 83), atomic actions and propositions are the basis of what is representable with PDL SL . In general, they correspond to statements asserting information about the state of a signer during signing. However, even though the Modeling Module knows how atoms combine, it can't determine by itself which assertions are meaningful for the studied corpus. For this reason, it corresponds to the annotator to determine what should be claimed, depending on the available tools.

  a formula where at least one of the atoms receives η as a parameter, denoted as Λ(E ϕ ) η , and every η parameter in Λ(E ϕ ) where Λ(E ϕ ) d is the formula Λ(E ϕ ) η , with every occurrence of η substituted by a member of the parameter's domain. If a Λ(E ϕ ) η doesn't exist but Λ(E ϕ ) is defined, then Λ(λ η.(E ϕ )) ≡ Λ(E ϕ ). Otherwise, it is not defined.

η is defined over the same domain D, then Λ(λ η.(E ϕ )) is equivalent to d∈D Λ(E ϕ ) d ,

Table 6

 6 .1 shows the observed quantities.

	ϕ	oppos. tap h. anch.
	Total	76	33	74

Table 6 .

 6 1: Manually annotated apparitions of property formulae on one video.

Table 6

 6

	.2.

Table 6 .

 6 2: Total reported hits over purely static phonemes on one video.The table above, shows the total number of times each of the formulae were satisfied on the utterance representing the video. When manually comparing these results, with the human observations counted in Table6.1, it was possible to generate the table presented

	in Figure 6.3.
	In Figure 6.3, in order to determine the quantity of hits and misses, each reported gloss
	interval was compared with the human observations: if an overlap existed, it was counted

as a hit. The human observations that weren't hit by the automatic gloss, were counted as misses. Finally, the last column of the table corresponds to false positives, i.e reported detections that didn't overlap with any human observation.

Table 6 . 3 :

 63 Per-formula summary of the total number of observations found, missed and false positives for the first verification case.

Table 6

 6

	.4.
	ϕ	oppos. tap h. anch.
	Total	390	48	84

Table 6 . 4 :

 64 Total reported hits over mixed phonemes on one video.

Table 6 . 5 :

 65 Per-formula summary of the total number of observations found, missed and false positives for the second verification case.

	ϕ	Human Obs. False+ Hit Miss
	opposition 71	5	314
	tap	31	2	15
	h. anchor	38	36	10

Table 6 . 6 :

 66 .6. Global per-formula summary of the total number of the obtained results.

	ϕ	Human Obs.	1st Case Hit Miss False+ Hit Miss False+ 2nd Case
	opposition	76	67	9	97	71	5	314
	tap	33	25	8	54	31	2	15
	h. anchor	74	44	30	94	38	36	10

Images obtained from[Prillwitz 1989].

Images obtained from[Prillwitz 1989].

Images obtained from[Prillwitz 1989].

Images obtained from[Sutton 2009].

Images obtained from[Sutton 2009].

Images obtained from[Sutton 2009].

Image obtained from[START_REF] Venkatagiri | Lecture Notes on American Sign Language[END_REF]].

Acknowledgements

Before I forget, I want to express my gratitude to all of those who, directly or indirectly,

Chapter 6 PDL SL in Sign Language

Research

This chapter presents some experimental results, obtained with the semi-automatic Sign Language (SL) annotation framework introduced in the previous chapter. During the experimentation phase, some technical adaptations to the original Propositional Dynamic Logic for Sign Language (PDL SL ) language were required, in order to ensure the modularity of formulae; this is, the formalism was extended to provide each formula with the capacity of being reused as part of some other formula. Also, some changes were required to account for undefined atoms: this is, propositions and actions used in the formulae database but not in the represented by the graph model. Finally, the chapter closes with some discussion about the expressiveness of PDL SL , compared to existing transcription languages.

Broadly, the next section presents some technical modifications to the PDL SL language, in an effort to simplify its use in linguistic research; although these are effectively theoretical, they result on, arguably, more comprehensible, reusable description formulae. Afterwards, the following section presents some experiments performed with the modified logic, as well as the obtained results. Finally, the chapter ends with a brief comparison between PDL SL and other description formalisms, intended to provide an empirical insight on representativity issues, without lingering on stronger properties such as logic decidability.

Extending PDL SL definitions

The original PDL SL language, as presented in Chapter 4 (see Section 4.2, p. 83), enables experts to codify SL phoneme sequences by way of logic formulae; however, PDL SL PDL SL do not give a direct representation for ZeBeDee's skeleton as is, specially because ZeBeDee does a semantic separation between the skeleton and the surface; however, it does provide the basic notion, by way of the set ART . Recall from Definition 4.4 that the set LOC is created by pairing articulators in ART to both named geometrical locations and members of BODY (even though ART ⊂ BODY). Then again, these pairings are not defined by the language but by the designer, therefore as long as the skeleton parts are in ART , the semantic separation can be implicitly established by

LOC.

ZeBeDee uses the previously explained definitions to create Holds and Movements (for the authors key postures and transitions). In particular, Holds differentiate from Movements by the nature of their respective parametric informations. For PDL SL , this corresponds to the members of the sets Π and Φ; recall that Π contains information about change (Movements) and Φ about static postures (Holds). In this regard, for both formalisms would seem to be compatible, since both treat statements as predicates; Chapter 5 provides more information about PDL SL in this regard. Nonetheless, as what happens with locations, PDL SL separates the semantics of the predicate from itself, and thus relies on the implementation of modeling rules (see Definition 5.9, p. 117) to provide meaning. For this reason, ultimately any symbol in either atom set can represent any ZeBeDee statement, as long as there exist a modeling rule defined in terms of ART , BODY, LOC over the coordinate space Ψ SL .

Regarding temporal structure, by design ZeBeDee can express sequences of Holds and Movements by grouping parameters into two structures: Keypostures and Transitions, respectively. These are built upon temporal notions such as time duration, which is not directly built into PDL SL ; the language is capable of expressing sequences (see Definition 4.12, p. 84), but it doesn't consider duration. Recall that, to model corpora, it was required to define time-stamping functions for articulation sequences (see Definition 4.15,p. 87). Because of this, in order to introduce time to a formula, it is necessary to define duration as a statement, expressible in terms of atoms: an atom duration can be added to the sets Φ and Π, so as to assert inside formulae how much time a phoneme lasts.

However, the reader should be aware that this entails the creation of modeling rules to define the meaning of time, just as it was done with space (see Definition 4.3,p. 80).

Finally, ZeBeDee provides a series of auxiliary tools like macros and loops, geared towards improving the experience of using the language rather than SL itself. There is no clear way to establish correspondence between these additional structures and PDL SL ; nonetheless, as long as their final results are expressible in ZeBeDee's primitive types, it should be possible to encode the same information as PDL SL formulae.