Combining Near-Field and Far-Field Microscopy: A new method for nanoscale super-resolution imaging

<b>Lähikenttä- ja kaukokenttämikroskopian yhdistäminen: Uusi korkearesoluutioinen menetelmä nanokuvantamiseen.b> Osteoporoosi on sairaus, jossa luun uudistumisprosessi ei ole enää tasapainossa. Uuden luun muodostuminen on hitaampaa johtuen osteoblastien laskeneesta aktiivisuudesta. Yksi keino estää osteoporoosin syntyä on estää osteoklastien sitoutuminen luun pinnalle, jolloin ne eivät aloita luun syömisprosessia. Tämän Pro gradu -tutkielman tarkoituksena on luoda uusi työkalu osteoklastien sitoutumisen tutkimiseen samanaikaisesti fluoresenssi- ja atomivoimamikroskoopilla. Tätä tarkoitusta varten yhdistettiin atomivoimamikroskooppi sekä STED mikroskooppi. Kirjallisuuskatsauksessa käydään läpi yksityiskohtaisesti molempien mikroskooppitekniikoiden teoriat. Kokeellisessa osiossa esitetään käytetyt metodit ja alustavat tulokset uudella systeemillä. Lisäksi keskustellaan lyhyesti kuvan analysoinnista ImageJohjelmalla. Konfokaalisen fluoresenssimikroskoopin ja atomivoimamikroskoopin yhdistelmä on keksitty jo aikaisemmin, mutta tavallisen konfokaalimikroskoopin erottelukyvyn raja on noin 200 nanometriä johtuen valon diffraktioluonteesta. Yksityiskohdat eivät erotu, jos ne ovat pienempiä kuin puolet käytettävästä aallonpituudesta. STED mikroskooppi mahdollistaa fluoresenssikuvien taltioimisen solunsisäisistä prosesseista 50 nanometrin lateraalisella erotuskyvyllä ja atomivoimamikroskooppi antaa topografista tietoa näytteestä nanometrien erotuskyvyllä. Biologisia näytteitä kuvannettaessa atomivoimamikroskoopin erotuskyky kuitenkin huononee ja yleensä saavutetaan 30-50 nanometrin erotuskyky. Kuvien kerrostaminen vaatii vertauspisteitä ja tätä varten käytettiin atomivoimamikroskoopin kärjen tunnistamista ja referenssipartikkeleita. Kuva-analysointi suoritettiin ImageJ-kuvankäsittelyohjelmalla. Tuloksista nähdään, että referenssipartikkelit ovat hyviä, mutta niiden sijoittaminen tarkasti tietylle kohdealueelle on hankalaa nanoskaalassa. Tästä johtuen kärjen havaitseminen fluoresenssikuvassa on parempi metodi. Atomivoimamikroskoopin kärki voidaan päällystää fluoresoivalla aineella, mutta tämä lisää kärjen aiheuttamaa konvoluutiota mittausdataan. Myös valon takaisinsirontaa kärjestä voidaan tutkia, jolloin konvoluutio ei lisäänny. Ensimmäisten kuvien kerrostamisessa käytettiin hyväksi fluoresoivalla aineella päällystettyä kärkeä ja lopputuloksessa oli vain 50 nanometrin yhteensopimattomuus fluoresenssi- ja topografiakuvan kanssa. STED mikroskoopin avulla nähdään leimattujen proteiinien tarkat sijainnit tiettynä ajankohtana elävän solun sisällä. Samaan aikaan pystytään kuvantamaan solun fyysisiä muotoja tai mitata adheesiovoimia atomivoimamikroskoopilla. Lisäksi voidaan käyttää funktinalisoitua kärkeä, jolla voidaan laukaista signalointitapahtumia solun ja soluväliaineen välillä. Sitoutuminen soluväliaineeseen voidaan rekisteröidä samoin kuin adheesiomediaattorien sijainnit sitoutumisalueella. Nämä dynaamiset havainnot tuottavat uutta informaatiota solun signaloinnista, kun osteoklasti kiinnittyy luun pintaan. Tämä teknologia tarjoaa uuden näkökulman monimutkaisiin signalointiprosesseihin nanoskaalassa ja tulee ratkaisemaan lukemattoman määrän biologisia ongelmia.

St. Petersburg Court Chant and the Tradition of Eastern Slavic Church Singing

The present study examines the repertory of liturgical chant known as St. Petersburg Court Chant which emerged within the Imperial Court of St. Petersburg, Russia, and appeared in print in a number of revisions during the course of the 19th century, eventually to spread throughout the Russian Empire and even abroad. The study seeks answers to questions on the essence and composition of Court Chant, its history and liturgical background, and most importantly, its musical relationship to other repertories of Eastern Slavic chant. The research questions emerge from previous literary accounts of Court Chant (summarized in the Introduction), which have tended to be inaccurate and generally not based on critical research. The study is divided into eight main chapters. Chapter 1 provides a survey of the history of Eastern Slavic chant and the Imperial Court Chapel of St. Petersburg until 1917, with special emphasis on the history of singing traditional chant in polyphony, the status of the Court Chapel as a government authority, and its endeavours in publishing church music. Chapter 2 deals with the liturgical background of Eastern chant, the chant genres, and main repertories of Eastern Slavic chant. Chapter 3 concentrates on chant sources: it introduces the musical notations utilised, after which a typology of chant books is presented. The discussion continues with a survey of the sources of Court Chant and their content, the specimens selected for closer analysis, the comparative materials from other repertories, and ends with a commentary on some chant sources that have been excluded. The comparative sources include a specimen from around the beginning of the 12th century, a few manuscripts from the 17th century, and printed and manuscript chant books from the early 18th to early 20th century, covering the geographical area that delimits to the western Ukraine, Astrakhan, Nizhny Novgorod, and the Solovetsky Monastery. Chapter 4 presents the approach and methods used in the subsequent analytical comparisons. After a survey of the pitch organization of Eastern Slavic chant, the customary harmonization strategy of traditional chant polyphony is examined, according to which a method for meaningful analysis of the harmony is proposed. The method is based on the observation that the harmonic framework of chant polyphony derives from the standard pitch collection of monodic chant known as the Church Gamut, specific pitches of which form eight harmonic regions that behave like the usual tonalities of major and harmonic minor. Because of the considerable quantity of comparative chant forms, computer-assisted statistical methods are applied to the analysis of chant melodies. The primary chant forms and their respective comparative forms have been pre-processed into reduced chant prototypes and divided into redactions. The analyses are carried out by measuring the formal dissimilarities of the primary chant forms of the Court Chant repertory against each comparative form, and also by measuring the reciprocal dissimilarities of all chant versions in a redaction, the results of which are subjected to agglomerative hierarchical clustering in order to find out how the chant forms relate to each other. The dissimilarities are determined by applying a metric dissimilarity function that is based on the Levenshtein Distance. Chapter 5 provides the melodic and harmonic analyses of generic chants (chants used for multiple texts of different lengths), i.e., chants for stichera samoglasny and troparia, Chapter 6 of pseudo-generic chants (chants that are used for multiple texts but with certain restrictions), i.e., chants for heirmoi, prokeimena, and three other hymns, and Chapter 7 of non-generic chants, covering nine chants that in the Court repertory are not shared by multiple texts. The results are summarized and evaluated in Chapter 8. Accordingly, it can be established that, contrary to previous conceptions, melodically, Court Chant is in effect a full part of the wider Eastern Slavic chant tradition. Even if it is somewhat detached from the chant versions of the Synodal square-note chant books and the local tradition of Moscow, it is particularly close to chant forms of East Ukraine and some vernacular repertories from Russia. Respectively, the harmonization strategies of Court Chant do not show significant individuality in comparison with those of the available polyphonic comparative sources, the main difference being the part-writing, which generally conforms to western common practice standard, whereas the deviations from this tend to be more significant in other analysed repertories of polyphonic chant. Thus, insofar as the subsequent prevalence of Court Chant is not based on its forceful dissemination by authorities (as suggested in previous literature but for which little tangible evidence could be found in Chapter 1), in the present author’s interpretation, Court Chant attained its dominance principally because musically it was considered sufficiently traditional, and as a chant body supported by the government, was conveniently available in print in serviceable harmonizations.

The Finnish Paper Workers' Union at a crossroads: Labor union representativeness in a changing environment, 1980-2008

This thesis consists of four articles and an introductory section. The main research questions in all the articles refer to the changes in the representativeness of the Finnish Paper Workers' Union. Representativeness stands for the entire entity of external, internal, legal and reputational factors that enable the labor union to represent its members and achieve its goals. This concept is based on an extensive reading of quantitative and qualitative industrial relations literature, which includes works based on Marxist labor-capital relations (such as Hyman's industrial relations studies), and more recent union density studies as well as gender- and ethnic diversity-based 'union revitalization' studies. Müller-Jentsch's German studies of industrial relations have been of particular importance as well as Streeck's industrial unionism and technology studies. The concept of representativeness is an attempt to combine the insights of these diverse strands of literature and bring the scientific discussion of labor unions back to the core of a union's function: representing its members. As such, it can be seen as a theoretical innovation. The concept helps to acknowledge both the heterogeneity of the membership and the totality of a labor union organization. The concept of representativeness aims to move beyond notions of 'power'. External representativeness can be expressed through the position of the labor union in the industrial relations system and the economy. Internal representativeness focuses on the aspects of labor unions that relate to the function of the union as an association with members, such as internal democracy. Legal representativeness lies in the formal legal position of the union – its rights and instruments. This includes collective bargaining legislation, co-decision rules and industrial conflict legislation. Reputational representativeness is related to how the union is seen by other actors and the general public, and can be approximated using data on strike activity. All these aspects of representativeness are path-dependent, and show the results of previous struggles over issues. The concept of representativeness goes beyond notions of labor union power and symbolizes an attempt to bring back the focus of industrial relations studies to the union's basic function of representing its members. The first article shows in detail the industrial conflict of the Finnish paper industry in 2005. The intended focus was the issue of gender in the negotiations over a new collective agreement, but the focal point of the industrial conflict was the issue of outsourcing and how this should be organized. Also, the issue of continuous shifts as an issue of working time was very important. The drawn-out conflict can be seen as a struggle over principles, and under pressure the labor union had to concede ground on the aforementioned issues. The article concludes that in this specific conflict, the union represented its' female members to a lesser extent, because the other issues took such priority. Furthermore, because of the substantive concessions. the union lost some of its internal representativeness, and the stubbornness of the union may have even harmed the reputation of the union. This article also includes an early version of the representativeness framework, through which this conflict is analyzed. The second article discusses wage developments, union density and collective bargaining within the context of representativeness. It is shown that the union has been able to secure substantial benefits for its members, regardless of declining employment. Collective agreements have often been based on centralized incomes policies, but the paper sector has not always joined these. Attention is furthermore paid to the changing competition of the General Assembly, with a surprisingly strong position of the Left Alliance still. In an attempt to replicate analysis of union density measures, an analysis of sectoral union density shows that similar factors as in aggregate data influence this measure, though – due to methodological issues – the results may not be robust. On this issue, it can be said that the method of analysis for aggregate union density is not suitable for sectoral union density analysis. The increasingly conflict-ridden industrial relations predicted have not actually materialized. The article concludes by asking whether the aim of ever-increasing wages is a sustainable one in the light of the pressures of globalization, though wage costs are a relatively small part of total costs. The third article discusses the history and use of outsourcing in the Finnish paper industry. It is shown using Hyman's framework of constituencies that over time, the perspective of the union changed from 'members of the Paper Workers' Union' to a more specific view of who is a core member of the union. Within the context of the industrial unionism that the union claims to practice, this is an important change. The article shows that the union more and more caters for a core group, while auxiliary personnel is less important to the union's identity and constituencies, which means that the union's internal representativeness has decreased. Maintenance workers are an exception; the union and employers have developed a rotating system that increases the efficient allocation of these employees. The core reason of the exceptional status of maintenance personnel is their high level of non-transferable skills. In the end it is debatable whether the compromise on outsourcing solves the challenges facing the industry. The fourth article shows diverging discourses within the union with regard to union-employer partnership for competitiveness improvements and instruments of local union representatives. In the collective agreement of 2008, the provision regulating wage effects of significant changes in the organization or content of work was thoroughly changed, though this mainly reflected decisions by the Labor Court on the pre-2008 version of the provision. This change laid bare the deep rift between the Social Democratic and Left Alliance (ex-Communist) factions of the union. The article argues that through the changed legal meaning of the provision, the union was able to transform concession bargaining into a basis for partnership. The internal discontent about this issue is nonetheless substantial and a threat to the unity of the union, both locally and at the union level. On the basis of the results of the articles, other factors influencing representativeness, such as technology and EU law and an overview of the main changes in the Finnish paper industry, it is concluded that, especially in recent years, the Finnish Paper Workers' Union has lost some of its representativeness. In particular, the loss of the efficiency of strikes is noted, the compromise on outsourcing which may have alienated a substantial part of the union's membership, and the change in the collective agreement of 2008 have caused this decline. In the latter case, the internal disunion on that issue shows the constraints of the union's internal democracy. Furthermore, the failure of the union to join the TEAM industrial union (by democratic means), the internal conflicts and a narrow focus on its own sector may also hurt the union in the future, as the paper industry in Finland is going through a structural change. None of these changes in representativeness would have been so drastic without the considerable pressure of globalization - in particular changing markets, changing technology and a loss of domestic investments to foreign investments, which in the end have benefited the corporations more than the Finnish employees of these corporations. Taken together, the union risks becoming socially irrelevant in time, though it will remain formally very strong on the basis of its institutional setting and financial situation.

Proactive and Preventive Student Welfare Activities in Finnish Preschool and Elementary School: Handling of Transition to Formal Schooling and a National Anti-Bullying Program as Examples

Prerequisites and effects of proactive and preventive psycho-social student welfare activities in Finnish preschool and elementary school were of interest in the present thesis. So far, Finnish student welfare work has mainly focused on interventions and individuals, and the voluminous possibilities to enhance well-being of all students as a part of everyday school work have not been fully exploited. Consequently, in this thesis three goals were set: (1) To present concrete examples of proactive and preventive psycho-social student welfare activities in Finnish basic education; (2) To investigate measurable positive effects of proactive and preventive activities; and (3) To investigate implementation of proactive and preventive activities in ecological contexts. Two prominent phenomena in preschool and elementary school years—transition to formal schooling and school bullying—were chosen as examples of critical situations that are appropriate targets for proactive and preventive psycho-social student welfare activities. Until lately, the procedures concerning both school transitions and school bullying have been rather problem-focused and reactive in nature. Theoretically, we lean on the bioecological model of development by Bronfenbrenner and Morris with concentric micro-, meso-, exo- and macrosystems. Data were drawn from two large-scale research projects, the longitudinal First Steps Study: Interactive Learning in the Child–Parent– Teacher Triangle, and the Evaluation Study of the National Antibullying Program KiVa. In Study I, we found that the academic skills of children from preschool–elementary school pairs that implemented several supportive activities during the preschool year developed more quickly from preschool to Grade 1 compared with the skills of children from pairs that used fewer practices. In Study II, we focused on possible effects of proactive and preventive actions on teachers and found that participation in the KiVa antibullying program influenced teachers‘ self-evaluated competence to tackle bullying. In Studies III and IV, we investigated factors that affect implementation rate of these proactive and preventive actions. In Study III, we found that principal‘s commitment and support for antibullying work has a clear-cut positive effect on implementation adherence of student lessons of the KiVa antibullying program. The more teachers experience support for and commitment to anti-bullying work from their principal, the more they report having covered KiVa student lessons and topics. In Study IV, we wanted to find out why some schools implement several useful and inexpensive transition practices, whereas other schools use only a few of them. We were interested in broadening the scope and looking at local-level (exosystem) qualities, and, in fact, the local-level activities and guidelines, along with teacherreported importance of the transition practices, were the only factors significantly associated with the implementation rate of transition practices between elementary schools and partner preschools. Teacher- and school-level factors available in this study turned out to be mostly not significant. To summarize, the results confirm that school-based promotion and prevention activities may have beneficial effects not only on students but also on teachers. Second, various top-down processes, such as engagement at the level of elementary school principals or local administration may enhance implementation of these beneficial activities. The main message is that when aiming to support the lives of children the primary focus should be on adults. In future, promotion of psychosocial well-being and the intrinsic value of inter- and intrapersonal skills need to be strengthened in the Finnish educational systems. Future research efforts in student welfare and school psychology, as well as focused training for psychologists in educational contexts, should be encouraged in the departments of psychology and education in Finnish universities. Moreover, a specific research centre for school health and well-being should be established.

Scheduling of guarded command based models

Formal methods provide a means of reasoning about computer programs in order to prove correctness criteria. One subtype of formal methods is based on the weakest precondition predicate transformer semantics and uses guarded commands as the basic modelling construct. Examples of such formalisms are Action Systems and Event-B. Guarded commands can intuitively be understood as actions that may be triggered when an associated guard condition holds. Guarded commands whose guards hold are nondeterministically chosen for execution, but no further control flow is present by default. Such a modelling approach is convenient for proving correctness, and the Refinement Calculus allows for a stepwise development method. It also has a parallel interpretation facilitating development of concurrent software, and it is suitable for describing event-driven scenarios. However, for many application areas, the execution paradigm traditionally used comprises more explicit control flow, which constitutes an obstacle for using the above mentioned formal methods. In this thesis, we study how guarded command based modelling approaches can be conveniently and efficiently scheduled in different scenarios. We first focus on the modelling of trust for transactions in a social networking setting. Due to the event-based nature of the scenario, the use of guarded commands turns out to be relatively straightforward. We continue by studying modelling of concurrent software, with particular focus on compute-intensive scenarios. We go from theoretical considerations to the feasibility of implementation by evaluating the performance and scalability of executing a case study model in parallel using automatic scheduling performed by a dedicated scheduler. Finally, we propose a more explicit and non-centralised approach in which the flow of each task is controlled by a schedule of its own. The schedules are expressed in a dedicated scheduling language, and patterns assist the developer in proving correctness of the scheduled model with respect to the original one.

Formal development and quantitative verification of dependable systems

-

Biomedical Event Extraction with Machine Learning

Biomedical natural language processing (BioNLP) is a subfield of natural language processing, an area of computational linguistics concerned with developing programs that work with natural language: written texts and speech. Biomedical relation extraction concerns the detection of semantic relations such as protein-protein interactions (PPI) from scientific texts. The aim is to enhance information retrieval by detecting relations between concepts, not just individual concepts as with a keyword search. In recent years, events have been proposed as a more detailed alternative for simple pairwise PPI relations. Events provide a systematic, structural representation for annotating the content of natural language texts. Events are characterized by annotated trigger words, directed and typed arguments and the ability to nest other events. For example, the sentence “Protein A causes protein B to bind protein C” can be annotated with the nested event structure CAUSE(A, BIND(B, C)). Converted to such formal representations, the information of natural language texts can be used by computational applications. Biomedical event annotations were introduced by the BioInfer and GENIA corpora, and event extraction was popularized by the BioNLP'09 Shared Task on Event Extraction. In this thesis we present a method for automated event extraction, implemented as the Turku Event Extraction System (TEES). A unified graph format is defined for representing event annotations and the problem of extracting complex event structures is decomposed into a number of independent classification tasks. These classification tasks are solved using SVM and RLS classifiers, utilizing rich feature representations built from full dependency parsing. Building on earlier work on pairwise relation extraction and using a generalized graph representation, the resulting TEES system is capable of detecting binary relations as well as complex event structures. We show that this event extraction system has good performance, reaching the first place in the BioNLP'09 Shared Task on Event Extraction. Subsequently, TEES has achieved several first ranks in the BioNLP'11 and BioNLP'13 Shared Tasks, as well as shown competitive performance in the binary relation Drug-Drug Interaction Extraction 2011 and 2013 shared tasks. The Turku Event Extraction System is published as a freely available open-source project, documenting the research in detail as well as making the method available for practical applications. In particular, in this thesis we describe the application of the event extraction method to PubMed-scale text mining, showing how the developed approach not only shows good performance, but is generalizable and applicable to large-scale real-world text mining projects. Finally, we discuss related literature, summarize the contributions of the work and present some thoughts on future directions for biomedical event extraction. This thesis includes and builds on six original research publications. The first of these introduces the analysis of dependency parses that leads to development of TEES. The entries in the three BioNLP Shared Tasks, as well as in the DDIExtraction 2011 task are covered in four publications, and the sixth one demonstrates the application of the system to PubMed-scale text mining.

Formal development of resilient distributed systems

Resilience is the property of a system to remain trustworthy despite changes. Changes of a different nature, whether due to failures of system components or varying operational conditions, significantly increase the complexity of system development. Therefore, advanced development technologies are required to build robust and flexible system architectures capable of adapting to such changes. Moreover, powerful quantitative techniques are needed to assess the impact of these changes on various system characteristics. Architectural flexibility is achieved by embedding into the system design the mechanisms for identifying changes and reacting on them. Hence a resilient system should have both advanced monitoring and error detection capabilities to recognise changes as well as sophisticated reconfiguration mechanisms to adapt to them. The aim of such reconfiguration is to ensure that the system stays operational, i.e., remains capable of achieving its goals. Design, verification and assessment of the system reconfiguration mechanisms is a challenging and error prone engineering task. In this thesis, we propose and validate a formal framework for development and assessment of resilient systems. Such a framework provides us with the means to specify and verify complex component interactions, model their cooperative behaviour in achieving system goals, and analyse the chosen reconfiguration strategies. Due to the variety of properties to be analysed, such a framework should have an integrated nature. To ensure the system functional correctness, it should rely on formal modelling and verification, while, to assess the impact of changes on such properties as performance and reliability, it should be combined with quantitative analysis. To ensure scalability of the proposed framework, we choose Event-B as the basis for reasoning about functional correctness. Event-B is a statebased formal approach that promotes the correct-by-construction development paradigm and formal verification by theorem proving. Event-B has a mature industrial-strength tool support { the Rodin platform. Proof-based verification as well as the reliance on abstraction and decomposition adopted in Event-B provides the designers with a powerful support for the development of complex systems. Moreover, the top-down system development by refinement allows the developers to explicitly express and verify critical system-level properties. Besides ensuring functional correctness, to achieve resilience we also need to analyse a number of non-functional characteristics, such as reliability and performance. Therefore, in this thesis we also demonstrate how formal development in Event-B can be combined with quantitative analysis. Namely, we experiment with integration of such techniques as probabilistic model checking in PRISM and discrete-event simulation in SimPy with formal development in Event-B. Such an integration allows us to assess how changes and di erent recon guration strategies a ect the overall system resilience. The approach proposed in this thesis is validated by a number of case studies from such areas as robotics, space, healthcare and cloud domain.

Formal modelling for digital media distribution

Human beings have always strived to preserve their memories and spread their ideas. In the beginning this was always done through human interpretations, such as telling stories and creating sculptures. Later, technological progress made it possible to create a recording of a phenomenon; first as an analogue recording onto a physical object, and later digitally, as a sequence of bits to be interpreted by a computer. By the end of the 20th century technological advances had made it feasible to distribute media content over a computer network instead of on physical objects, thus enabling the concept of digital media distribution. Many digital media distribution systems already exist, and their continued, and in many cases increasing, usage is an indicator for the high interest in their future enhancements and enriching. By looking at these digital media distribution systems, we have identified three main areas of possible improvement: network structure and coordination, transport of content over the network, and the encoding used for the content. In this thesis, our aim is to show that improvements in performance, efficiency and availability can be done in conjunction with improvements in software quality and reliability through the use of formal methods: mathematical approaches to reasoning about software so that we can prove its correctness, together with the desirable properties. We envision a complete media distribution system based on a distributed architecture, such as peer-to-peer networking, in which different parts of the system have been formally modelled and verified. Starting with the network itself, we show how it can be formally constructed and modularised in the Event-B formalism, such that we can separate the modelling of one node from the modelling of the network itself. We also show how the piece selection algorithm in the BitTorrent peer-to-peer transfer protocol can be adapted for on-demand media streaming, and how this can be modelled in Event-B. Furthermore, we show how modelling one peer in Event-B can give results similar to simulating an entire network of peers. Going further, we introduce a formal specification language for content transfer algorithms, and show that having such a language can make these algorithms easier to understand. We also show how generating Event-B code from this language can result in less complexity compared to creating the models from written specifications. We also consider the decoding part of a media distribution system by showing how video decoding can be done in parallel. This is based on formally defined dependencies between frames and blocks in a video sequence; we have shown that also this step can be performed in a way that is mathematically proven correct. Our modelling and proving in this thesis is, in its majority, tool-based. This provides a demonstration of the advance of formal methods as well as their increased reliability, and thus, advocates for their more wide-spread usage in the future.