Universitätspublikationen
Refine
Year of publication
- 2012 (34) (remove)
Document Type
- Article (12)
- Bachelor Thesis (6)
- Conference Proceeding (6)
- Doctoral Thesis (4)
- Working Paper (4)
- Contribution to a Periodical (1)
- Master's Thesis (1)
Has Fulltext
- yes (34) (remove)
Is part of the Bibliography
- no (34)
Keywords
- Formale Semantik (2)
- Funktionale Programmierung (2)
- LHC (2)
- Lambda-Kalkül (2)
- Nebenläufigkeit (2)
- ALICE (1)
- ALICE experiment (1)
- Abstrakter Automat (1)
- Comparison with QCD (1)
- Correctness (1)
Institute
- Informatik (34) (remove)
Time-critical applications process a continuous stream of input data and have to meet specific timing constraints. A common approach to ensure that such an application satisfies its constraints is over-provisioning: The application is deployed in a dedicated cluster environment with enough processing power to achieve the target performance for every specified data input rate. This approach comes with a drawback: At times of decreased data input rates, the cluster resources are not fully utilized. A typical use case is the HLT-Chain application that processes physics data at runtime of the ALICE experiment at CERN. From a perspective of cost and efficiency it is desirable to exploit temporarily unused cluster resources. Existing approaches aim for that goal by running additional applications. These approaches, however, a) lack in flexibility to dynamically grant the time-critical application the resources it needs, b) are insufficient for isolating the time-critical application from harmful side-effects introduced by additional applications or c) are not general because application-specific interfaces are used. In this thesis, a software framework is presented that allows to exploit unused resources in a dedicated cluster without harming a time-critical application. Additional applications are hosted in Virtual Machines (VMs) and unused cluster resources are allocated to these VMs at runtime. In order to avoid resource bottlenecks, the resource usage of VMs is dynamically modified according to the needs of the time-critical application. For this purpose, a number of previously not combined methods is used. On a global level, appropriate VM manipulations like hot migration, suspend/resume and start/stop are determined by an informed search heuristic and applied at runtime. Locally on cluster nodes, a feedback-controlled adaption of VM resource usage is carried out in a decentralized manner. The employment of this framework allows to increase a cluster’s usage by running additional applications, while at the same time preventing negative impact towards a time-critical application. This capability of the framework is shown for the HLT-Chain application: In an empirical evaluation the cluster CPU usage is increased from 49% to 79%, additional results are computed and no negative effect towards the HLT-Chain application are observed.
We introduce tree-width for first order formulae φ, fotw(φ). We show that computing fotw is fixed-parameter tractable with parameter fotw. Moreover, we show that on classes of formulae of bounded fotw, model checking is fixed parameter tractable, with parameter the length of the formula. This is done by translating a formula φ with fotw(φ)<k into a formula of the k-variable fragment Lk of first order logic. For fixed k, the question whether a given first order formula is equivalent to an Lk formula is undecidable. In contrast, the classes of first order formulae with bounded fotw are fragments of first order logic for which the equivalence is decidable. Our notion of tree-width generalises tree-width of conjunctive queries to arbitrary formulae of first order logic by taking into account the quantifier interaction in a formula. Moreover, it is more powerful than the notion of elimination-width of quantified constraint formulae, defined by Chen and Dalmau (CSL 2005): for quantified constraint formulae, both bounded elimination-width and bounded fotw allow for model checking in polynomial time. We prove that fotw of a quantified constraint formula φ is bounded by the elimination-width of φ, and we exhibit a class of quantified constraint formulae with bounded fotw, that has unbounded elimination-width. A similar comparison holds for strict tree-width of non-recursive stratified datalog as defined by Flum, Frick, and Grohe (JACM 49, 2002). Finally, we show that fotw has a characterization in terms of a cops and robbers game without monotonicity cost.
Spam detection in wikis
(2012)
Wikis haben durch ihre kollaborativen Eigenschaften maßgeblich an der Entstehung des Web 2.0 beigetragen: Durch die Zusammenarbeit vieler Benutzer ist es möglich geworden, große Mengen an Daten aufzubereiten und strukturiert zusammenzustellen. So ist ein Datenschatz angewachsen, der wertvoll für die maschinelle Verarbeitung von Text ist: Mittels der Techniken des TextMining lassen sich aus Wikis viele Informationen extrahieren. Dazu ist es zunächst sinnvoll, deren Inhalte herunterzuladen und lokal zu speichern.
Zum Editieren von Seiten existieren häufig keine Zugangsbeschränkungen. So wird die genannte Akkumulation von Informationen ermöglicht, da sich viele Benutzer beteiligen können. Jedoch birgt dies die Gefahr, dass Wikis durch Spam verunreinigt werden: Zur Verwendung als Wissensbasis ist dies hinderlich.
Gängige Anti-Spam-Maßnahmen finden online statt und setzen unter anderem auf die Überwachung durch die Nutzer oder den Einsatz von Blacklists für Weblinks. Im Gegensatz dazu wird im Rahmen dieser Arbeit folgender Ansatz gewählt: Ein lokal gespeichertes Wiki wird einer Bestandsaufnahme unterzogen und in seiner Gesamtheit untersucht. Es werden ausschließlich die Inhalte der Seiten berücksichtigt. Die Spam-Erkennung beruht auf einer Kombination von Entscheidungsregeln sowie der Berücksichtigung von Wortwahrscheinlichkeiten. Dadurch konnten gute Ergebnisse erzielt werden.
This paper shows equivalence of applicative similarity and contextual approximation, and hence also of bisimilarity and contextual equivalence, in LR, the deterministic call-by-need lambda calculus with letrec extended by data constructors, case-expressions and Haskell's seqoperator. LR models an untyped version of the core language of Haskell. Bisimilarity simplifies equivalence proofs in the calculus and opens a way for more convenient correctness proofs for program transformations.
The proof is by a fully abstract and surjective transfer of the contextual approximation into a call-by-name calculus, which is an extension of Abramsky's lazy lambda calculus. In the latter calculus equivalence of similarity and contextual approximation can be shown by Howe's method. Using an equivalent but inductive definition of behavioral preorder we then transfer similarity back to the calculus LR.
The translation from the call-by-need letrec calculus into the extended call-by-name lambda calculus is the composition of two translations. The first translation replaces the call-by-need strategy by a call-by-name strategy and its correctness is shown by exploiting infinite tress, which emerge by unfolding the letrec expressions. The second translation encodes letrec-expressions by using multi-fixpoint combinators and its correctness is shown syntactically by comparing reductions of both calculi. A further result of this paper is an isomorphism between the mentioned calculi, and also with a call-by-need letrec calculus with a less complex definition of reduction than LR.
This paper describes the ongoing efforts of the authors to present ancient Greek and Roman numismatic data on the public internet, with an emphasis on efforts to integrate information from multiple sources using Linked Data and Semantic Web techniques. By way of very modern metaphor, it is useful to think of coins as intentionally created packages of 'named entities'. Each coin was struck by a particular authority, often at a known site, and coins often make reference to familiar concepts such as deities, historical events, or symbols that were widely recognized in the ancient world. The institutions represented among the authors have deployed search interfaces that allow users to take advantage of this aspect of numismatic databases. The American Numismatic Society's database provides faceted search to its collection of over 550,000 objects. The Portable Antiquities Scheme (PAS) in the UK presents individual finds (and hoards) recorded throughout the country. The Römisch-Germanische Kommission and the University of Frankfurt (DBIS) are developing a prototype metaportal (INTERFACE) that accesses national databases of coin finds held in in Frankfurt, Vienna and Utrecht. Each of these resources is beginning to explore Semantic Web/Linked data approaches so that the role of numismatic standards is immediately coming to the fore. DBIS and INTERFACE are developing a numismatic ontology. At the ANS and PAS, the public database already presents RDF serializations based on Dublin Core. Together, the authors have begun to explore standardization of conceptual names on the basis of the vocabulary presented at the site http://nomisma.org . Nomisma.org is a collaborative effort to provide stable digital representations of numismatic concepts and entities. It provides URIs for such basic concepts as 'coin', 'mint', 'axis'. All of these are defined within the scope of numismatics but are already being linked to other stable resources where available. This is particularly the case for mints. For example, the URI http://nomisma.org/id/corinth is intended to represent that ancient city in its role as a minter/issuer of coins. The URI is linked via the SKOS ontology to the Pleiades Gazetteer of ancient places. This allows Nomisma to be the basis for a common representation of the concept that an object is a coin minted at Corinth. The ANS has already deployed such relationships in its public database. The work of all these projects is very much in progress so that this paper hopes to generate discussion on how multiple large projects can move forward in their own work while encouraging sufficient commonality to support large scale research questions undertaken by diverse audiences.
Scenegraph LoD-Analyse
(2012)
Level of Detail-Verfahren sind in der Computergrafik alltäglich und allgegenwärtig. Da das Thema seit Jahren ein aktiv bearbeitetes Feld in der Wissenschaft ist, existiert eine extreme Fülle an Verfahren mit unterschiedlichen Ansätzen oder Verfeinerungen. Es ist jedoch sehr schwer, die Unterschiede zwischen den Verfahren zu quantifizieren. Jede Arbeit nutzt ihre eigenen Testfälle und Methoden, wodurch sich selten echte Rückschlüsse auf Vergleiche zu anderen Verfahren ziehen lassen. Um hier einen Ansatz zur Lösung dieses Problems zu präsentieren, wird vorgeschlagen, ein allgemein nutzbares Testframework zu erstellen, das geeignet ist, LOD-Verfahren auf unterschiedliche Aspekte hin zu untersuchen. Es wird eine Reihe von konkreten Tests und ein dazugehöriges Programm als Rahmenwerk vorgestellt werden, das einen solchen Ansatz implementiert. Diese Testimplementierung ist bewusst einfach gehalten, sie wird jedoch einen guten Überblick darüber geben, welche Probleme es zu lösen gilt und worauf dabei geachtet werden muss.
This paper considers the logic FOcard, i.e., first-order logic with cardinality predicates that can specify the size of a structure modulo some number. We study the expressive power of FOcard on the class of languages of ranked, finite, labelled trees with successor relations. Our first main result characterises the class of FOcard-definable tree languages in terms of algebraic closure properties of the tree languages. As it can be effectively checked whether the language of a given tree automaton satisfies these closure properties, we obtain a decidable characterisation of the class of regular tree languages definable in FOcard. Our second main result considers first-order logic with unary relations, successor relations, and two additional designated symbols < and + that must be interpreted as a linear order and its associated addition. Such a formula is called addition-invariant if, for each fixed interpretation of the unary relations and successor relations, its result is independent of the particular interpretation of < and +. We show that the FOcard-definable tree languages are exactly the regular tree languages definable in addition-invariant first-order logic. Our proof techniques involve tools from algebraic automata theory, reasoning with locality arguments, and the use of logical interpretations. We combine and extend methods developed by Benedikt and Segoufin (ACM ToCL, 2009) and Schweikardt and Segoufin (LICS, 2010).
In dieser Arbeit wurden Web Browser bezüglich ihrer Eignung zum Erstellen interaktiver eLearning Fragen untersucht. Vor dem Hintergrund der speziellen Charakteristika von mobilen Endgeräten wurden insbesondere die Aspekte der Beschränkung auf standardisierte Technologien, sowie die Clientseitigkeit der Applikation hervorgehoben. Es konnte eine Grundlage geschaffen werden, die das Erstellen von interaktiven Fragen nur mit Hilfe von HTML und Javascript ermöglicht und es wurde ein weitgehender Verzicht auf serverseitige Komponenten erreicht.
The calculus CHF models Concurrent Haskell extended by concurrent, implicit futures. It is a process calculus with concurrent threads, monadic concurrent evaluation, and includes a pure functional lambda-calculus which comprises data constructors, case-expressions, letrec-expressions, and Haskell’s seq. Futures can be implemented in Concurrent Haskell using the primitive unsafeInterleaveIO, which is available in most implementations of Haskell. Our main result is conservativity of CHF, that is, all equivalences of pure functional expressions are also valid in CHF. This implies that compiler optimizations and transformations from pure Haskell remain valid in Concurrent Haskell even if it is extended by futures. We also show that this is no longer valid if Concurrent Haskell is extended by the arbitrary use of unsafeInterleaveIO.
he first measurements of the invariant differential cross sections of inclusive π0 and η meson production at mid-rapidity in proton–proton collisions at s=0.9 TeV and s=7 TeV are reported. The π0 measurement covers the ranges 0.4<pT<7 GeV/c and 0.3<pT<25 GeV/c for these two energies, respectively. The production of η mesons was measured at s=√7 TeV in the range 0.4<pT<15 GeV/c. Next-to-Leading Order perturbative QCD calculations, which are consistent with the π0 spectrum at s=0.9 TeV, overestimate those of π0 and η mesons at s=√7 TeV, but agree with the measured η/π0 ratio at s=√7 TeV.
A measurement of the multi-strange Ξ− and Ω− baryons and their antiparticles by the ALICE experiment at the CERN Large Hadron Collider (LHC) is presented for inelastic proton–proton collisions at a centre-of-mass energy of 7 TeV. The transverse momentum (pT) distributions were studied at mid-rapidity (|y|<0.5) in the range of 0.6<pT<8.5 GeV/c for Ξ− and Ξ¯+ baryons, and in the range of 0.8<pT<5 GeV/c for Ω− and Ω¯+. Baryons and antibaryons were measured as separate particles and we find that the baryon to antibaryon ratio of both particle species is consistent with unity over the entire range of the measurement. The statistical precision of the current data has allowed us to measure a difference between the mean pT of Ξ− (Ξ¯+) and Ω− (Ω¯+). Particle yields, mean pT, and the spectra in the intermediate pT range are not well described by the PYTHIA Perugia 2011 tune Monte Carlo event generator, which has been tuned to reproduce the early LHC data. The discrepancy is largest for Ω− (Ω¯+). This PYTHIA tune approaches the pT spectra of Ξ− and Ξ¯+ baryons below pT<0.85 GeV/c and describes the Ξ− and Ξ¯+ spectra above pT>6.0 GeV/c. We also illustrate the difference between the experimental data and model by comparing the corresponding ratios of (Ω−+Ω¯+)/(Ξ−+Ξ¯+) as a function of transverse mass.
The ALICE experiment has measured low-mass dimuon production in pp collisions at √s=7 TeV in the dimuon rapidity region 2.5<y<4. The observed dimuon mass spectrum is described as a superposition of resonance decays (η,ρ,ω,η′,ϕ) into muons and semi-leptonic decays of charmed mesons. The measured production cross sections for ω and ϕ are σω(1<pt<5 GeV/c,2.5<y<4)=5.28±0.54(stat)±0.49(syst) mb and σϕ(1<pt<5 GeV/c,2.5<y<4)=0.940±0.084(stat)±0.076(syst) mb. The differential cross sections d2σ/dydpt are extracted as a function of pt for ω and ϕ. The ratio between the ρ and ω cross section is obtained. Results for the ϕ are compared with other measurements at the same energy and with predictions by models.
Identical neutral kaon pair correlations are measured in √s=7 TeV pp collisions in the ALICE experiment. One-dimensional Ks0Ks0 correlation functions in terms of the invariant momentum difference of kaon pairs are formed in two multiplicity and two transverse momentum ranges. The femtoscopic parameters for the radius and correlation strength of the kaon source are extracted. The fit includes quantum statistics and final-state interactions of the a0/f0 resonance. Ks0Ks0 correlations show an increase in radius for increasing multiplicity and a slight decrease in radius for increasing transverse mass, mT, as seen in ππ correlations in pp collisions and in heavy-ion collisions. Transverse mass scaling is observed between the Ks0Ks0 and ππ radii. Also, the first observation is made of the decay of the f2′(1525) meson into the Ks0Ks0 channel in pp collisions.
The ALICE Collaboration reports the measurement of the relative J/ψ yield as a function of charged particle pseudorapidity density dNch/dη in pp collisions at √s=7 TeV at the LHC. J/ψ particles are detected for pt>0, in the rapidity interval |y|<0.9 via decay into e+e−, and in the interval 2.5<y<4.0 via decay into μ+μ− pairs. An approximately linear increase of the J/ψ yields normalized to their event average (dNJ/ψ/dy)/〈dNJ/ψ/dy〉 with (dNch/dη)/〈dNch/dη〉 is observed in both rapidity ranges, where dNch/dη is measured within |η|<1 and pt>0. In the highest multiplicity interval with 〈dNch/dη(bin)〉=24.1, corresponding to four times the minimum bias multiplicity density, an enhancement relative to the minimum bias J/ψ yield by a factor of about 5 at 2.5<y<4 (8 at |y|<0.9) is observed.
The ALICE Collaboration has measured inclusive J/ψ production in pp collisions at a center-of-mass energy √s=2.76 TeV at the LHC. The results presented in this Letter refer to the rapidity ranges |y|<0.9 and 2.5<y<4 and have been obtained by measuring the electron and muon pair decay channels, respectively. The integrated luminosities for the two channels are Linte=1.1 nb−1 and Lintμ=19.9 nb−1, and the corresponding signal statistics are NJ/ψe+e−=59±14 and NJ/ψμ+μ−=1364±53. We present dσJ/ψ/dy for the two rapidity regions under study and, for the forward-y range, d2σJ/ψ/dydpt in the transverse momentum domain 0<pt<8 GeV/c. The results are compared with previously published results at s=7 TeV and with theoretical calculations.
Computing the diameter of a graph is a fundamental part of network analysis. Even if the data fits into main memory the best known algorithm needs O(n2) [3] with high probability to compute the exact diameter. In practice this is usually too costly. Therefore, heuristics have been developed to approximate the diameter much faster. The heuristic “double sweep lower bound” (dslb) has reasonably good results and needs only two Breadth-First Searches (BFS). Hence, dslb has a complexity of O(n+m). If the data does not fit into main memory, an external-memory algorithm is needed. In this thesis the I/O model by Vitter and Shriver [4] is used. It is widely accepted and has produced suitable results in the past. The best known external-memory BFS implementation has an I/O-complexity of W(pn B + sort(n)) for sparse graphs [5]. But this is still very expensive compared to the I/O complexity of sorting with O(N/B * logM/B (N/B)). While there is no improvement for the external-memory computation of BFS yet, Meyer published a different approach called “Parallel clustering growing approach” (PAR_APPROX) that is a trade-off between the I/O complexity and the approximation guarantee [6].
In this thesis different existing approaches will be evaluated. Also, PAR_APPROX will be implemented and analyzed if it is viable in practice. One main result will be that it is difficult to choose the parameter in a way that PAR_APPROX is reasonably fast for every graph class without using the semi external-memory Single Source Shortest Path (SSSP) implementation by [1]. However, the gain is small compared to external-memory BFS using this approach. Therefore, the approach PAR_APPROX_R will be developed. Furthermore, a lower bound for the expected error of PAR_APPROX_R will be proved on a carefully chosen difficult input class. With PAR_APPROX_R the desired gain will be reached.
Heavy flavour decay muon production at forward rapidity in proton–proton collisions at √s=7 TeV
(2012)
The production of muons from heavy flavour decays is measured at forward rapidity in proton–proton collisions at √s=7 TeV collected with the ALICE experiment at the LHC. The analysis is carried out on a data sample corresponding to an integrated luminosity Lint=16.5 nb−1. The transverse momentum and rapidity differential production cross sections of muons from heavy flavour decays are measured in the rapidity range 2.5<y<4, over the transverse momentum range 2<pt<12 GeV/c. The results are compared to predictions based on perturbative QCD calculations.
Harmonic decomposition of two particle angular correlations in Pb–Pb collisions at √sNN=2.76 TeV
(2012)
Angular correlations between unidentified charged trigger (t) and associated (a) particles are measured by the ALICE experiment in Pb–Pb collisions at √sNN=2.76 TeV for transverse momenta 0.25<pTt,a<15 GeV/c, where pTt>pTa. The shapes of the pair correlation distributions are studied in a variety of collision centrality classes between 0 and 50% of the total hadronic cross section for particles in the pseudorapidity interval |η|<1.0. Distributions in relative azimuth Δϕ≡ϕt−ϕa are analyzed for |Δη|≡|ηt−ηa|>0.8, and are referred to as “long-range correlations”. Fourier components VnΔ≡〈cos(nΔϕ)〉 are extracted from the long-range azimuthal correlation functions. If particle pairs are correlated to one another through their individual correlation to a common symmetry plane, then the pair anisotropy VnΔ(pTt,pTa) is fully described in terms of single-particle anisotropies vn(pT) as VnΔ(pTt,pTa)=vn(pTt)vn(pTa). This expectation is tested for 1⩽n⩽5 by applying a global fit of all VnΔ(pTt,pTa) to obtain the best values vn{GF}(pT). It is found that for 2⩽n⩽5, the fit agrees well with data up to pTa∼3–4 GeV/c, with a trend of increasing deviation as pTt and pTa are increased or as collisions become more peripheral. This suggests that no pair correlation harmonic can be described over the full 0.25<pT<15 GeV/c range using a single vn(pT) curve; such a description is however approximately possible for 2⩽n⩽5 when pTa<4 GeV/c. For the n=1 harmonic, however, a single v1(pT) curve is not obtained even within the reduced range pTa<4 GeV/c.
Die vorliegende Bachelorarbeit untersucht die Möglichkeiten der mobilen Produktion und Verwaltung von Web- und Multimedia-Inhalten, welche mit geografischen Koordinaten verknüpft sind.
Durch die stetig wachsende Verbreitung mobiler Geräte wie Smartphones, Tablets oder Netbooks und der damit in Anspruch genommenen Verfügbarkeit von mobilen Internetzugängen in Form von WLAN, GPRS, UMTS oder LTE, wird die gemeinsame Erstellung und Verwaltung von geolokalisierten Inhalten durch Teilnehmer einer Interessengruppe ermöglicht.
Besonders Inhalte deren Standort relevant ist, können von automatisierter Lokalisierung profitieren. Durch Ortungsmechanismen können Daten bei ihrer Erstellung oder Bearbeitung automatisch mit dem Standort des Geräts versehen werden. So lassen sich zum einen geografische Daten sammeln und zum anderen Inhalte auf unkomplizierte Art und Weise mit dem Standort des Autors zum Zeitpunkt ihrer Erstellung verknüpfen.
Darüber hinaus können Anwender abhängig von ihrem Aufenthaltsort Informationen über ihre Umgebung abrufen, ohne zuvor in einer Kartenansicht zu ihrer aktuellen Position navigieren zu müssen.
Die vorliegende Arbeit behandelt sowohl das Erhalten als auch das Erzeugen multimedialer Inhalte in Abhängigkeit von ihren geografischen Koordinaten. Die technische Realisierung dieses Konzepts findet mit Hilfe der frei verfügbaren MediaWiki-Software[1] als Content-Management-System sowie einer, für mobile Geräte optimierten Webseite als Frontend statt.
Der Umfang der Arbeit umfasst neben dem Entwurf eines Konzepts und der ausführlichen Beschreibung einer möglichen Implementierung eine Einführung in die Grundlagen der verwendeten Komponenten. Zuletzt sollen ein Fazit und ein Ausblick Konzept und Realisierung kritisch betrachten, um einen Einblick in vorhandene Potenziale der Lösung zu bieten.
Diese Arbeit zeigt, dass die optimale Verteilung von Individuen in Gruppen unter Beachtung ihrer Zeitpräferenzen ein NP-schweres Problem ist. Daher liegt es Nahe, dass für große Teilnehmerzahlen eine optimale Lösung nicht in praxistauglicher Zeit berechnet werden kann. Hier kann eine geeignete Heuristik Abhilfe schaffen.
Da dieses Problem in Universitäten für Studierende bei der Zuteilung der Übungsgruppen für Hunderte von Teilnehmern jedes Semester aufs Neue gelöst werden muss, macht es Sinn, dabei eine rechnergestützte Lösung einzusetzen.
In dieser Arbeit werden die gängigsten in Deutschland und insbesondere an der Goethe-Universität Frankfurt am Main verwendeten Gruppeneinteilungssysteme untersucht. Alle aktuell eingesetzten Lösungen weisen offensichtliche Mängel auf. In dieser Arbeit wird analysiert, weshalb es dazu kommt und gezeigt, wie diese Mängel vermieden werden können. Außerdem werden Kriterien entwickelt und diskutiert, die ein gutes Gruppeneinteilungssystem erfüllen sollte.
Es wird beschrieben, inwiefern eine gute mit einer Heuristik schnell berechenbare approximative Lösung des Gruppeneinteilungsproblems besser als eine perfekte Lösung sein könnte. Mehrere Heuristiken werden verglichen und eine für dieses Problem gut passende wird entwickelt und implementiert. Mithilfe der Beispielimplementierung und anhand anonymisierter Anmeldedaten für die Veranstaltungen aus vergangenen Jahren wird gezeigt, welche Ergebnisse bei dem Wechsel zu einem solchen System erreicht werden können.
Weiterhin wird analysiert, wie ein solches Gruppeneinteilungssystem an die anderen an Universitäten eingesetzten digitalen Systeme angekoppelt werden kann. Das ist notwendig, um zu vermeiden, dass die redundanten Studierendendaten doppelt gepflegt werden müssen. Somit werden Konsistenz und Korrektheit der Daten bei dem Einsatz eines neuen Systems gefördert.
Abschließend wird ein Ausblick in die Zukunft der Gruppeneinteilungssysteme gegeben und beschrieben, welche Aspekte in diesem Bereich weiterhin wichtig sein könnten.
The diagram-based method to prove correctness of program transformations consists of computing
complete set of (forking and commuting) diagrams, acting on sequences of standard reductions
and program transformations. In many cases, the only missing step for proving correctness of a
program transformation is to show the termination of the rearrangement of the sequences. Therefore
we encode complete sets of diagrams as term rewriting systems and use an automated tool
to show termination, which provides a further step in the automation of the inductive step in
correctness proofs.
With increasing heterogeneity of modern hardware, different requirements for 3d applications arise. Despite the fact that real-time rendering of photo-realistic images is possible using today’s graphics cards, still large computational effort is required. Furthermore, smart-phones or computers with older, less powerful graphics cards may not be able to reproduce these results. To retain interactive rendering, usually the detail of a scene is reduced, and so less data needs to be processed. This removal of data, however, may introduce errors, so called artifacts. These artifacts may be distracting for a human spectator when gazing at the display. Thus, the visual quality of the presented scene is reduced. This is counteracted by identifying features of an object that can be removed without introducing artifacts. Most methods utilize geometrical properties, such as distance or shape, to rate the quality of the performed reduction. This information used to generate so called Levels Of Detail (LODs), which are made available to the rendering system. This reduces the detail of an object using the precalculated LODs, e.g. when it is moved into the back of the scene. The appropriate LOD is selected using a metric, and it is replaced with the current displayed version. This exchange must be made smoothly, requiring both LOD-versions to be drawn simultaneously during a transition. Otherwise, this exchange will introduce discontinuities, which are easily discovered by a human spectator. After completion of the transition, only the newly introduced LOD-version is drawn and the previous overhead removed. These LOD-methods usually operate with discrete levels and exploit limitations of both the display and the spectator: the human.
Humans are limited in their vision. This ranges from being unable to distinct colors at varying illumination scenarios to the limitation to focus only at one location at a time. Researchers have developed many applications to exploit these limitations to increase the quality of an applied compression. Some popular methods of vision-based compression are MPEG or JPEG. For example, a JPEG compression exploits the reduced sensitivity of humans regarding color and so encodes colors with a lower resolution. Also, other fields, such as auditive perception, allow the exploitation of human limitations. The MP3 compression, for example, reduces the quality of stored frequencies if other frequencies are masking it. For representation of perception various computer models exist. In our rendering scenario, a model is advantageous that cannot be influenced by a human spectator, such as the visual salience or saliency.
Saliency is a notion from psycho-physics that determines how an object “pops out” of its surrounding. These outstanding objects (or features) are important for the human vision and are directly evaluated by our Human Visual System (HVS). Saliency combines multiple parts of the HVS and allows an identification of regions where humans are likely to look at. In applications, saliency-based methods have been used to control recursive or progressive rendering methods. Especially expensive display methods, such as pathtracing or global illumination calculations, benefit from a perceptual representation as recursions or calculations can be aborted if only small or unperceivable errors are expected to occur. Yet, saliency is commonly applied to 2d images, and an extension towards 3d objects has only partially been presented. Some issues need to be addressed to accomplish a complete transfer.
In this work, we present a smart rendering system that not only utilizes a 3d visual salience model but also applies the reduction in detail directly during rendering. As opposed to normal LOD-methods, this detail reduction is not limited to a predefined set of levels, but rather a dynamic and continuous LOD is created. Furthermore, to apply this reduction in a human-oriented way, a universal function to compute saliency of a 3d object is presented. The definition of this function allows to precalculate and store object-related visual salience information. This stored data is then applicable in any illumination scenario and allows to identify regions of interest on the surface of a 3d object. Unlike preprocessed methods, which generate a view-independent LOD, this identification includes information of the scene as well. Thus, we are able to define a perception-based, view-specific LOD. Performance measures of a prototypical implementation on computers with modern graphic cards achieved interactive frame rates, and several tests have proven the validity of the reduction.
The adaptation of an object is performed with a dynamic data structure, the TreeCut. It is designed to operate on hierarchical representations, which define a multi-resolution object. In such a hierarchy, the leaf nodes contain the highest detail while inner nodes are approximations of their respective subtree. As opposed to classical hierarchical rendering methods, a cut is stored and re-traversal of a tree during rendering is avoided. Due to the explicit cut representation, the TreeCut can be altered using only two core operations: refine and coarse. The refine-operation increases detail by replacing a node of the tree with its children while the coarse-operation removes the node along with its siblings and replaces them with their parent node. These operations do not rely on external information and can be performed in a local manner. These only require direct successor or predecessor information. Different strategies to evolve the TreeCut are presented, which adapt the representation using only information given by the current cut. These evaluate the cut by assigning either a priority or a target-level (or bucket) to each cut-node. The former is modelled as an optimization problem that increases the average priority of a cut while being restricted in some way, e.g. in size. The latter evolves the cut to match a certain distribution. This is applied in cases where a prioritization of nodes is not applicable. Both evaluation strategies operate with linear time complexity with respect to the size of the current TreeCut.
The data layout is chosen to separate rendering data and hierarchy to enable multi-threaded evaluation and display. The object is adapted over multiple frames while the rendering is not interrupted by the used evaluation strategy. Therefore, we separate the representation of the hierarchy from the rendering data. Due to its design, this overhead imposed to the TreeCut data structure does not influence rendering performance, and a linear time complexity for rendering is retained. The TreeCut is not only limited to alter geometrical detail of an object. The TreeCut has successfully been applied to create a non-photo-realistic stippling display, which draws the object with equal sized points in varying density. In this case the bucket-based evaluation strategy is utilized, which determines the distribution of the cut based on local illumination information. As an alternative, an attention drawing mechanism is proposed, which applies the TreeCut evaluation strategies to define the display style of a notification icon. A combination of external priorities is used to derive the appropriate icon version. An application for this mechanism is a messaging system that accounts for the current user situation.
When optimizing an object or scene, perceptual methods allow to account for or exploit human limitations. Therefore, visual salience approaches derive a saliency map, which encodes regions of interest in a 2d map. Rendering algorithms extract importance from such a map and adapt the rendering accordingly, e.g. abort a recursion when the current location is unsalient. The visual salience depends on multiple factors including the view and the illumination of the scene. We extend the existing definition of the 2d saliency and propose a universal function for 3d visual salience: the Bidirectional Saliency Weight Distribution Function (BSWDF). Instead of extracting the saliency from 2d image and approximate 3d information, we directly compute this information using the 3d data. We derive a list of equivalent features for the 3d scenario and add them to the BSWDF. As the BSWDF is universal, also 2d images are covered with the BSWDF, and the calculation of the important regions within images is possible.
To extract the individual features that contribute to visual salience, capabilities of modern graphics card in combination with an accumulation method for rendering is utilized. Inspired from point-based rendering methods local features are summed up in a single surface element (surfel) and are compared with their surround to determine whether they “pop out”. These operations are performed with a shader-program that is executed on the Graphics Processing Unit (GPU) and has direct access to the 3d data. This increases processing speed because no transfer of the data is required. After computation, each of these object-specific features can be combined to derive a saliency map for this object. Surface specific information, e.g. color or curvature, can be preprocessed and stored onto disk. We define a sampling scheme to determine the views that need to be evaluated for each object. With these schemes, the features can be interpolated for any view that occurs during rendering, and the according surface data is reconstructed. These sampling schemes compose a set of images in form of a lookup table. This is similar to existing rendering techniques, which extract illumination information from a lookup. The size of the lookup table increases only with the number of samples or the image size used for creation as the images are of equal size. Thus, the quality of the saliency data is independent of the object’s geometrical complexity. The computation of a BSWDF can be performed either on a Central Processing Unit (CPU) or a GPU, and an implementation requires only a few instructions when using a shader program. If the surface features have been stored during a preprocess, a reprojection of the data is performed and combined with the current information of the object. Once the data is available, the computation of the saliency values is done using a specialized illumination model, and a priority for each primitive is extracted. If the GPU is used, the calculated data has to be transferred from the graphics card. We therefore use the “transform feedback” capabilities, which allow high transfer rates and preserve the order of processed primitives. So, an identification of regions of interest based on the currently used primitives is achieved. The TreeCut evaluation strategies are then able to optimize the representation in an perception-based manner.
As the adaptation utilizes information of the current scene, each change to an object can result in new visual salience information. So, a self-optimizing system is defined: the Feedback System. The output generated by this system converges towards a perception-optimized solution. To proof the saliency information to be useful, user tests have been performed with the results generated by the proposed Feedback System. We compared a saliency-enhanced object compression to a pure geometrical approach, common for LOD-generation. One result of the tests is that saliency information allows to increase compression even further as possible with the pure geometrical methods. The participants were not able to distinguish between objects even if the saliency-based compression had only 60% of the size of the geometrical reduced object. If the size ratio is greater, saliency-based compression is rated, on average, with higher score and these results have a high significance using statistical tests. The Feedback System extends an 3d object with the capability of self-optimization. Not only geometrical detail but also other properties can be limited and optimized using the TreeCut in combination with a BSWDF. We present a dynamic animation, which utilizes a Software Development Kit (SDK) for physical simulations. This was chosen, on the one hand, to show the universal applicability of the proposed system, and on the other hand, to focus on the connection between the TreeCut and the SDK. We adapt the existing framework, and include the SDK within our design. In this case, the TreeCut-operations not only alter geometrical but also simulation detail. This increases calculation performance because both the rendering and the SDK operate on less data after the reduction has been completed.
The selected simulation type is a soft-body simulation. Soft-bodies are deformable in a certain degree but retain their internal connection. An example is a piece of cloth that smoothly fits the underlying surface without tearing apart. Other types are rigid bodies, i.e. idealistic objects that cannot be deformed, and fluids or gaseous materials, which are well suited for point-based simulations. Any of these simulations scales with the number of simulation nodes used, and a reduction of detail increases performance significantly. We define a specialized BSWDF to evaluate simulation specific features, such as motion. The Feedback System then increases detail in highly salient regions, e.g. those with large motion, and saves computation time by reducing detail in static parts of the simulation. So, detail of the simulation is preserved while less nodes are simulated.
The incorporation of perception in real-time rendering is an important part of recent research. Today, the HVS is well understood, and valid computer models have been derived. These models are frequently used in commercial and free software, e.g. JPEG compression. Within this thesis, the Tree-Cut is presented to change the LOD of an object in a dynamic and continuous manner. No definition of the individual levels in advance is required, and the transitions are performed locally. Furthermore, in combination with an identification of important regions by the BSWDF, a perceptual evaluation of a 3d object is achieved. As opposed to existing methods, which approximate data from 2d images, the perceptual information is directly acquired from 3d data. Some of this data can be preprocessed if necessary, to defer additional computations during rendering. The Feedback System, created by the TreeCut and the BSWDF, optimizes the representation and is not limited to visual data alone. We have shown with our prototype that interactive frame rates can be achieved with modern hardware, and we have proven the validity of the reductions by performing several user tests. However, the presented system only focuses on specific aspects, and more research is required to capture even more capabilities that a perception-based rendering system can provide.
The pT-differential inclusive production cross section of the prompt charm-strange meson Ds+ in the rapidity range |y|<0.5 was measured in proton–proton collisions at s=7 TeV at the LHC using the ALICE detector. The analysis was performed on a data sample of 2.98×108 events collected with a minimum-bias trigger. The corresponding integrated luminosity is Lint=4.8 nb−1. Reconstructing the decay Ds+→ϕπ+, with ϕ→K−K+, and its charge conjugate, about 480 Ds± mesons were counted, after selection cuts, in the transverse momentum range 2<pT<12 GeV/c. The results are compared with predictions from models based on perturbative QCD. The ratios of the cross sections of four D meson species (namely D0, D+, D⁎+ and Ds+) were determined both as a function of pT and integrated over pT after extrapolating to full pT range, together with the strangeness suppression factor in charm fragmentation. The obtained values are found to be compatible within uncertainties with those measured by other experiments in e+e−, ep and pp interactions at various centre-of-mass energies.
This thesis will first introduce in more detail the Bayesian theory and its use in integrating multiple information sources. I will briefly talk about models and their relation to the dynamics of an environment, and how to combine multiple alternative models. Following that I will discuss the experimental findings on multisensory integration in humans and animals. I start with psychophysical results on various forms of tasks and setups, that show that the brain uses and combines information from multiple cues. Specifically, the discussion will focus on the finding that humans integrate this information in a way that is close to the theoretical optimal performance. Special emphasis will be put on results about the developmental aspects of cue integration, highlighting experiments that could show that children do not perform similar to the Bayesian predictions. This section also includes a short summary of experiments on how subjects handle multiple alternative environmental dynamics. I will also talk about neurobiological findings of cells receiving input from multiple receptors both in dedicated brain areas but also primary sensory areas. I will proceed with an overview of existing theories and computational models of multisensory integration. This will be followed by a discussion on reinforcement learning (RL). First I will talk about the original theory including the two different main approaches model-free and model-based reinforcement learning. The important variables will be introduced as well as different algorithmic implementations. Secondly, a short review on the mapping of those theories onto brain and behaviour will be given. I mention the most in uential papers that showed correlations between the activity in certain brain regions with RL variables, most prominently between dopaminergic neurons and temporal difference errors. I will try to motivate, why I think that this theory can help to explain the development of near-optimal cue integration in humans. The next main chapter will introduce our model that learns to solve the task of audio-visual orienting. Many of the results in this section have been published in [Weisswange et al. 2009b,Weisswange et al. 2011]. The model agent starts without any knowledge of the environment and acts based on predictions of rewards, which will be adapted according to the reward signaling the quality of the performed action. I will show that after training this model performs similarly to the prediction of a Bayesian observer. The model can also deal with more complex environments in which it has to deal with multiple possible underlying generating models (perform causal inference). In these experiments I use di#erent formulations of Bayesian observers for comparison with our model, and find that it is most similar to the fully optimal observer doing model averaging. Additional experiments using various alterations to the environment show the ability of the model to react to changes in the input statistics without explicitly representing probability distributions. I will close the chapter with a discussion on the benefits and shortcomings of the model. The thesis continues whith a report on an application of the learning algorithm introduced before to two real world cue integration tasks on a robotic head. For these tasks our system outperforms a commonly used approximation to Bayesian inference, reliability weighted averaging. The approximation is handy because of its computational simplicity, because it relies on certain assumptions that are usually controlled for in a laboratory setting, but these are often not true for real world data. This chapter is based on the paper [Karaoguz et al. 2011]. Our second modeling approach tries to address the neuronal substrates of the learning process for cue integration. I again use a reward based training scheme, but this time implemented as a modulation of synaptic plasticity mechanisms in a recurrent network of binary threshold neurons. I start the chapter with an additional introduction section to discuss recurrent networks and especially the various forms of neuronal plasticity that I will use in the model. The performance on a task similar to that of chapter 3 will be presented together with an analysis of the in uence of different plasticity mechanisms on it. Again benefits and shortcomings and the general potential of the method will be discussed. I will close the thesis with a general conclusion and some ideas about possible future work.
A concurrent implementation of software transactional memory in Concurrent Haskell using a call-by-need functional language with processes and futures is given. The description of the small-step operational semantics is precise and explicit, and employs an early abort of conflicting transactions. A proof of correctness of the implementation is given for a contextual semantics with may- and should-convergence. This implies that our implementation is a correct evaluator for an abstract specification equipped with a big-step semantics.
Conceptual design of an ALICE Tier-2 centre integrated into a multi-purpose computing facility
(2012)
This thesis discusses the issues and challenges associated with the design and operation of a data analysis facility for a high-energy physics experiment at a multi-purpose computing centre. At the spotlight is a Tier-2 centre of the distributed computing model of the ALICE experiment at the Large Hadron Collider at CERN in Geneva, Switzerland. The design steps, examined in the thesis, include analysis and optimization of the I/O access patterns of the user workload, integration of the storage resources, and development of the techniques for effective system administration and operation of the facility in a shared computing environment. A number of I/O access performance issues on multiple levels of the I/O subsystem, introduced by utilization of hard disks for data storage, have been addressed by the means of exhaustive benchmarking and thorough analysis of the I/O of the user applications in the ALICE software framework. Defining the set of requirements to the storage system, describing the potential performance bottlenecks and single points of failure and examining possible ways to avoid them allows one to develop guidelines for selecting the way how to integrate the storage resources. The solution, how to preserve a specific software stack for the experiment in a shared environment, is presented along with its effects on the user workload performance. The proposal for a flexible model to deploy and operate the ALICE Tier-2 infrastructure and applications in a virtual environment through adoption of the cloud computing technology and the 'Infrastructure as Code' concept completes the thesis. Scientific software applications can be efficiently computed in a virtual environment, and there is an urgent need to adapt the infrastructure for effective usage of cloud resources.
The ALICE Collaboration has made the first measurement at the LHC of J/ψ photoproduction in ultra-peripheral Pb–Pb collisions at sNN=2.76 TeV. The J/ψ is identified via its dimuon decay in the forward rapidity region with the muon spectrometer for events where the hadronic activity is required to be minimal. The analysis is based on an event sample corresponding to an integrated luminosity of about 55 μb−1. The cross section for coherent J/ψ production in the rapidity interval −3.6<y<−2.6 is measured to be dσJ/ψcoh/dy=1.00±0.18(stat)−0.26+0.24(syst) mb. The result is compared to theoretical models for coherent J/ψ production and found to be in good agreement with those models which include nuclear gluon shadowing.
Poster presentation: Calcium plays a pivotal role in relaying electrical signals of the cell to subcellular compartments, such as the nucleus. Since this one ion type is used by the cell for many processes a neuron needs to establish finely tuned calcium pathways in order to be able to differentiate multiple tasks, [1-3].
While it is known that neurons can actively change their shape upon neuronal activity, [4-7], we here present novel findings of activity-regulated nuclear morphology, [8,9]. With the help of an experimental and computational modeling approach, we show that hippocampal neurons can change the previously spherical shape of their nuclei to complex and infolded morphologies. This morphology regulation is demonstrated to be regulated by NMDA-receptor gated calcium, while synaptic and extra-synaptic NMDA-receptors elicit opposing effects on nuclear morphology, [8].
The structural alterations of the cell nucleus have significant effects on nuclear calcium dynamics. Compartmentalization of the nucleus, due to membrane infoldings, changes calcium frequencies, amplitudes and spatial distributions, [8,10]. Since these parameters have been shown to control downstream events towards gene transcription, [11,12], the results elucidate the cellular control of nuclear function with the help of morphology modulation. With respect to processes downstream of calcium, we show that histone H3 phosphorylation is closely linked to nuclear morphology. Investigating the nuclear morphologies of hippocampal neurons, two major classes were identified [9,10]. One class contains non-infolded nuclei that have the function of calcium signal integrators, while the other class contains highly infolded nuclei, which function as frequency detectors of nuclear calcium, [10].
Extending this interdisciplinary approach of investigating structure/function relationships in neurons, the effects of cellular morphology – as well as the morphology of the endoplasmic reticulum and other organelles – on neuronal calcium signals is currently being investigated. This endeavor makes use of highly detailed, three-dimensional models of neuronal calcium dynamics, including the three-dimensional morphology of the cell and its organelles.
We show how Sestoft’s abstract machine for lazy evaluation of purely functional programs can be extended to evaluate expressions of the calculus CHF – a process calculus that models Concurrent Haskell extended by imperative and implicit futures. The abstract machine is modularly constructed by first adding monadic IO-actions to the machine and then in a second step we add concurrency. Our main result is that the abstract machine coincides with the original operational semantics of CHF, w.r.t. may- and should-convergence.
This volume contains the proceedings of the 12th International Workshop on Termination (WST 2012), to be held February 19–23, 2012 in Obergurgl, Austria. The goal of the Workshop on Termination is to be a venue for presentation and discussion of all topics in and around termination. In this way, the workshop tries to bridge the gaps between different communities interested and active in research in and around termination. The 12th International Workshop on Termination in Obergurgl continues the successful workshops held in St. Andrews (1993), La Bresse (1995), Ede (1997), Dagstuhl (1999), Utrecht (2001), Valencia (2003), Aachen (2004), Seattle (2006), Paris (2007), Leipzig (2009), and Edinburgh (2010). The 12th International Workshop on Termination did welcome contributions on all aspects of termination and complexity analysis. Contributions from the imperative, constraint, functional, and logic programming communities, and papers investigating applications of complexity or termination (for example in program transformation or theorem proving) were particularly welcome. We did receive 18 submissions which all were accepted. Each paper was assigned two reviewers. In addition to these 18 contributed talks, WST 2012, hosts three invited talks by Alexander Krauss, Martin Hofmann, and Fausto Spoto.