@phdthesis{4232,
author = {Harold Vladar},
publisher = {Faculty of mathematical and natural sciences, University of Groningen},
title = {{Stochasticity and Variability in the dynamics and genetics of populations}},
doi = {3811},
year = {2009},
}
@phdthesis{4363,
author = {Vasu Singh},
booktitle = {Formalizing and Verifying Transactional Memories},
publisher = {EPFL Lausanne},
title = {{Formalizing and Verifying Transactional Memories}},
year = {2009},
}
@phdthesis{3400,
abstract = {Invasive fungal infections pose a serious threat to immunocompromised people. Most of these infections are caused by either Candida or Aspergillus species, with A. fumigatus being the predominant causative agent of Invasive Aspergillosis. Affected people comprise mainly haematopoietic stem cell or solid organ transplant patients who receive either high-dose corticosteroids or immunosuppressants. These risk factors predispose to the development of Invasive
Aspergillosis which is lethal in 20 to 80 % of the cases, largely due to insufficient efficacy of current antifungal therapy. Thus one major aim in current mycological research is the identification of new drug targets.
The polysaccharide-based fungal cell wall is both essential to fungi and absent from human cells which makes it appear an attractive new target. Notably, many components of the A. fumigatus cell wall, including the polysaccharide galactomannan, glycoproteins, and glycolipids, contain the unusual sugar galactofuranose (Galf). In contrast to the other cell wall monosaccharides, Galf does not occur on human cells but is known as component of cell surface molecules of many pathogenic bacteria and protozoa, such as Mycobacterium tuberculosis or Leishmania major. These molecules are often essential for virulence or viability of these organisms which suggested a possible role of Galf in the pathogenicity of A. fumigatus.
To address the importance of Galf in A. fumigatus, the key biosynthesis gene glfA, encoding UDPgalactopyranose mutase (UGM), was deleted. In different experimental approaches it was demonstrated that the absence of the glfA gene led to a complete loss of Galf-containing glycans.
Analysis of the DeltaglfA phenotype revealed growth and sporulation defects, reduced thermotolerance and an increased susceptibility to antifungal drugs. Electron Microscopy indicated a cell wall defect as a likely cause for the observed impairments. Furthermore, the virulence of the DeltaglfA mutant was found to be severely attenuated in a murine model of Invasive Aspergillosis.
The second focus of this study was laid on further elucidation of the galactofuranosylation pathway in A. fumigatus. In eukaryotes, a UDP-Galf transporter is likely required to transport UDP-Galf from the
cytosol into the organelles of the secretory pathway, but no such activity had been described. Sixteen candidate genes were identified in the A. fumigatus genome of which one, glfB, was found in close proximity to the glfA gene. In vitro transport assays revealed specificity of GlfB for UDP-Galf suggesting that glfB encoded indeed a UDP-Galf transporter. The influence of glfB on
galactofuranosylation was determined by a DeltaglfB deletion mutant, which closely recapitulated the DeltaglfA phenotype and was likewise found to be completely devoid of Galf. It could be concluded that all galactofuranosylation processes in A. fumigatus occur in the secretory pathway, including the biosynthesis of the cell wall polysaccharide galactomannan whose subcellular origin was previously disputed.
Thus in the course of this study the first UDP-Galf specific nucleotide sugar transporter was identified and its requirement for galactofuranosylation in A. fumigatus demonstrated. Moreover, it was shown that blocking the galactofuranosylation pathway impaired virulence of A. fumigatus which suggests the UDP-Galf biosynthesis enzyme UGM as a target for new antifungal drugs.},
author = {Philipp Schmalhorst},
pages = {1 -- 72},
publisher = {Gottfried Wilhelm Leibniz UniversitĂ¤t Hannover},
title = {{Biosynthesis of Galactofuranose Containing Glycans and Their Relevance for the Pathogenic Fungus Aspergillus fumigatus}},
year = {2009},
}
@phdthesis{4409,
abstract = {Models of timed systems must incorporate not only the sequence of system events, but the timings of these events as well to capture the real-time aspects of physical systems. Timed automata are models of real-time systems in which states consist of discrete locations and values for real-time clocks. The presence of real-time clocks leads to an uncountable state space. This thesis studies verification problems on timed automata in a game theoretic framework.
For untimed systems, two systems are close if every sequence of events of one system is also observable in the second system. For timed systems, the difference in timings of the two corresponding sequences is also of importance. We propose the notion of bisimulation distance which quantifies timing differences; if the bisimulation distance between two systems is epsilon, then (a) every sequence of events of one system has a corresponding matching sequence in the other, and (b) the timings of matching events in between the two corresponding traces do not differ by more than epsilon. We show that we can compute the bisimulation distance between two timed automata to within any desired degree of accuracy. We also show that the timed verification logic TCTL is robust with respect to our notion of quantitative bisimilarity, in particular, if a system satisfies a formula, then every close system satisfies a close formula.
Timed games are used for distinguishing between the actions of several agents, typically a controller and an environment. The controller must achieve its objective against all possible choices of the environment. The modeling of the passage of time leads to the presence of zeno executions, and corresponding unrealizable strategies of the controller which may achieve objectives by blocking time. We disallow such unreasonable strategies by restricting all agents to use only receptive strategies --strategies which while not being required to ensure time divergence by any agent, are such that no agent is responsible for blocking time. Time divergence is guaranteed when all players use receptive strategies. We show that timed automaton games with receptive strategies can be solved by a reduction to finite state turn based game graphs. We define the logic timed alternating-time temporal logic for verification of timed automaton games and show that the logic can be model checked in EXPTIME. We also show that the minimum time required by an agent to reach a desired location, and the maximum time an agent can stay safe within a set of locations, against all possible actions of its adversaries are both computable.
We next study the memory requirements of winning strategies for timed automaton games. We prove that finite memory strategies suffice for safety objectives, and that winning strategies for reachability objectives may require infinite memory in general. We introduce randomized strategies in which an agent can propose a probabilistic distribution of moves and show that finite memory randomized strategies suffice for all omega-regular objectives. We also show that while randomization helps in simplifying winning strategies, and thus allows the construction of simpler controllers, it does not help a player in winning at more states, and thus does not allow the construction of more powerful controllers.
Finally we study robust winning strategies in timed games. In a physical system, a controller may propose an action together with a time delay, but the action cannot be assumed to be executed at the exact proposed time delay. We present robust strategies which incorporate such jitters and show that the set of states from which an agent can win robustly is computable.},
author = {Prabhu, Vinayak},
pages = {1 -- 137},
publisher = {University of California, Berkeley},
title = {{Games for the verification of timed systems}},
year = {2008},
}
@phdthesis{4415,
abstract = {Many computing applications, especially those in safety critical embedded systems, require highly predictable timing properties. However, time is often not present in the prevailing computing and networking abstractions. In fact, most advances in computer architecture, software, and networking favor average-case performance over timing predictability. This thesis studies several methods for the design of concurrent and/or distributed embedded systems with precise timing guarantees. The focus is on flexible and compositional methods for programming and verification of the timing properties. The presented methods together with related formalisms cover two levels of design: (1) Programming language/model level. We propose the distributed variant of Giotto, a coordination programming language with an explicit temporal semanticsâ€”the logical execution time (LET) semantics. The LET of a task is an interval of time that specifies the time instants at which task inputs and outputs become available (task release and termination instants). The LET of a task is always non-zero. This allows us to communicate values across the network without changing the timing information of the task, and without introducing nondeterminism. We show how this methodology supports distributed code generation for distributed real-time systems. The method gives up some performance in favor of composability and predictability. We characterize the tradeoff by comparing the LET semantics with the semantics used in Simulink. (2) Abstract task graph level. We study interface-based design and verification of applications represented with task graphs. We consider task sequence graphs with general event models, and cyclic graphs with periodic event models with jitter and phase. Here an interface of a component exposes time and resource constraints of the component. Together with interfaces we formally define interface composition operations and the refinement relation. For efficient and flexible composability checking two properties are important: incremental design and independent refinement. According to the incremental design property the composition of interfaces can be performed in any order, even if interfaces for some components are not known. The refinement relation is defined such that in a design we can always substitute a refined interface for an abstract one. We show that the framework supports independent refinement, i.e., the refinement relation is preserved under composition operations.},
author = {Matic, Slobodan},
pages = {1 -- 148},
publisher = {University of California, Berkeley},
title = {{Compositionality in deterministic real-time embedded systems}},
year = {2008},
}