Refine
Year of publication
Document Type
- Preprint (759)
- Article (402)
- Working Paper (119)
- Doctoral Thesis (93)
- Diploma Thesis (47)
- Conference Proceeding (41)
- Book (37)
- Bachelor Thesis (36)
- diplomthesis (28)
- Report (25)
Has Fulltext
- yes (1619)
Is part of the Bibliography
- no (1619)
Keywords
Institute
- Informatik (1619) (remove)
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).
The interactive verification system VeriFun is based on a polymorphic call-by-value functional language and on a first-order logic with initial model semantics w.r.t. constructors. It is designed to perform automatic induction proofs and can also deal with partial functions. This paper provides a reconstruction of the corresponding logic and semantics using the standard treatment of undefinedness which adapts and improves the VeriFun-logic by allowing reasoning on nonterminating expressions and functions. Equality of expressions is defined as contextual equivalence based on observing termination in all closing contexts. The reconstruction shows that several restrictions of the VeriFun framework can easily be removed, by natural generalizations: mutual recursive functions, abstractions in the data values, and formulas with arbitrary quantifier prefix can be formulated. The main results of this paper are: an extended set of deduction rules usable in VeriFun under the adapted semantics is proved to be correct, i.e. they respect the observational equivalence in all extensions of a program. We also show that certain classes of theorems are conservative under extensions, like universally quantified equations. Also other special classes of theorems are analyzed for conservativity.
The interactive verification system VeriFun is based on a polymorphic call-by-value functional language and on a first-order logic with initial model semantics w.r.t. constructors. This paper provides a reconstruction of the corresponding logic when partial functions are permitted. Typing is polymorphic for the definition of functions but monomorphic for terms in formulas. Equality of terms is defined as contextual equivalence based on observing termination in all contexts. The reconstruction also allows several generalizations of the functional language like mutual recursive functions and abstractions in the data values. The main results are: Correctness of several program transformations for all extensions of a program, which have a potential usage in a deduction system. We also proved that universally quantified equations are conservative, i.e. if a universally quantified equation is valid w.r.t. a program P, then it remains valid if the program is extended by new functions and/or new data types.
A logical framework consisting of a polymorphic call-by-value functional language and a first-order logic on the values is presented, which is a reconstruction of the logic of the verification system VeriFun. The reconstruction uses contextual semantics to define the logical value of equations. It equates undefinedness and non-termination, which is a standard semantical approach. The main results of this paper are: Meta-theorems about the globality of several classes of theorems in the logic, and proofs of global correctness of transformations and deduction rules. The deduction rules of VeriFun are globally correct if rules depending on termination are appropriately formulated. The reconstruction also gives hints on generalizations of the VeriFun framework: reasoning on nonterminating expressions and functions, mutual recursive functions and abstractions in the data values, and formulas with arbitrary quantifier prefix could be allowed.
In this paper we demonstrate how to relate the semantics given by the nondeterministic call-by-need calculus FUNDIO [SS03] to Haskell. After introducing new correct program transformations for FUNDIO, we translate the core language used in the Glasgow Haskell Compiler into the FUNDIO language, where the IO construct of FUNDIO corresponds to direct-call IO-actions in Haskell. We sketch the investigations of [Sab03b] where a lot of program transformations performed by the compiler have been shown to be correct w.r.t. the FUNDIO semantics. This enabled us to achieve a FUNDIO-compatible Haskell-compiler, by turning o not yet investigated transformations and the small set of incompatible transformations. With this compiler, Haskell programs which use the extension unsafePerformIO in arbitrary contexts, can be compiled in a "safe" manner.
Funktionale Programmiersprachen weisen viele Eigenschaften auf, die zur modernen Softwareentwicklung benotigt werden: Zuverlässigkeit, Modularisierung, Wiederverwendbarkeit und Verifizierbarkeit. Als schwer vereinbar mit diesen Sprachen stellte sich die Einbettung von Seiteneffekten in diese Sprachen heraus. Nach einigen mehr oder weniger gescheiterten Ansätzen hat sich mittlerweile fur die nichtstrikte funktionale Sprache Haskell der monadische Ansatz durchgesetzt, bei dem die Seiteneffekte geschickt verpackt werden, so dass zumindest IO-behaftete Teile eines Haskell-Programms dem klassischen imperativen Programmierstil ähneln. S. Peyton Jones bringt dieses in [Pey01, Seite 3] auf den Punkt, indem er schreibt "...Haskell is the world's finest imperative programming language." Dies ist einerseits vorteilhaft, denn die klassischen Programmiertechniken können angewendet werden, andererseits bedeutet dies auch eine Rückkehr zu altbekannten Problemen in diesen Sprachen: Der Programmcode wird unverständlicher, die Wiederverwendbarkeit von Code verschlechtert sich, Änderungen im Programm sind aufwendig. Zudem erscheint die monadische Programmierung teilweise umständlich. Deshalb wurde im Zuge der Entwicklung in fast jede Implementierung von Haskell ein Konstrukt eingebaut, dass von monadischem IO zu direktem IO führt. Da dieses nicht mit dem bisherigen Ansatz vereinbar schien, wird es als "unsafe" bezeichnet, die entsprechende Funktion heißt "unsafePerformIO". Zahlreiche Anwendungen benutzten diese Funktion, teilweise scheint die Verwendung zumindest aus Effizienzgründen unabdingbar. Allerdings ist die Frage, wann dieses verwendet werden darf, d.h. so angewendet wird, dass es nicht "unsicher" ist, nur unzureichend geklärt. Das Zitat in Abbildung 1.1 gibt wenig Aufschluss über die korrekte Anwendung, zumal immer wieder Diskussionen entstehen, ob die Verwendung von unsafePerformIO in diesem oder jenem Spezialfall korrekt ist.
The selection of features for classification, clustering and approximation is an important task in pattern recognition, data mining and soft computing. For real-valued features, this contribution shows how feature selection for a high number of features can be implemented using mutual in-formation. Especially, the common problem for mutual information computation of computing joint probabilities for many dimensions using only a few samples is treated by using the Rènyi mutual information of order two as computational base. For this, the Grassberger-Takens corre-lation integral is used which was developed for estimating probability densities in chaos theory. Additionally, an adaptive procedure for computing the hypercube size is introduced and for real world applications, the treatment of missing values is included. The computation procedure is accelerated by exploiting the ranking of the set of real feature values especially for the example of time series. As example, a small blackbox-glassbox example shows how the relevant features and their time lags are determined in the time series even if the input feature time series determine nonlinearly the output. A more realistic example from chemical industry shows that this enables a better ap-proximation of the input-output mapping than the best neural network approach developed for an international contest. By the computationally efficient implementation, mutual information becomes an attractive tool for feature selection even for a high number of real-valued features.
Grafik-Hardware ist programmierbar geworden. Graphic Processing Units (GPUs) der neuen Generation wie der GeForce3 von NVIDIA enthalten Prozessoren, die es dem Software-Entwickler erlauben kurze Routinen auf der Grafik-Hardware auszuführen. Ich gebe in dieser Arbeit einen umfassenden Überblick über die Architekur und Leistungsfähigkeit dieser neuen Chipgeneration, zeige deren Stärken und Schwächen auf und diskutiere Verbesserungsvorschläge. Als Teil der Arbeit präsentiere ich einige von mir entwickelte Schattierungsverfahren, sowie eine Wassersimulation. Diese Demonstratoren sind darauf ausgerichtet vollständig auf den Prozessoren der neuen Grafikchip- Generation zu laufen. Als Antwort auf die Mängel der zur Zeit verfügbaren Application Programming Interfaces stelle ich ein alternatives Interface zur Steuerung der neuen GPUKomponenten vor, das insbesondere die Austauschbarkeit und Kombinierbarkeit von GPU-Programmen unterstützt.
At the Large Hadron Collider at CERN in Geneva, Switzerland, atomic nuclei are collided at ultra-relativistic energies. Many final-state particles are produced in each collision and their properties are measured by the ALICE detector. The detector signals induced by the produced particles are digitized leading to data rates that are in excess of 48 GB/s. The ALICE High Level Trigger (HLT) system pioneered the use of FPGA- and GPU-based algorithms to reconstruct charged-particle trajectories and reduce the data size in real time. The results of the reconstruction of the collision events, available online, are used for high level data quality and detector-performance monitoring and real-time time-dependent detector calibration. The online data compression techniques developed and used in the ALICE HLT have more than quadrupled the amount of data that can be stored for offline event processing.
At the Large Hadron Collider at CERN in Geneva, Switzerland, atomic nuclei are collided at ultra-relativistic energies. Many final-state particles are produced in each collision and their properties are measured by the ALICE detector. The detector signals induced by the produced particles are digitized leading to data rates that are in excess of 48 GB/s. The ALICE High Level Trigger (HLT) system pioneered the use of FPGA- and GPU-based algorithms to reconstruct charged-particle trajectories and reduce the data size in real time. The results of the reconstruction of the collision events, available online, are used for high level data quality and detector-performance monitoring and real-time time-dependent detector calibration. The online data compression techniques developed and used in the ALICE HLT have more than quadrupled the amount of data that can be stored for offline event processing.
At the Large Hadron Collider at CERN in Geneva, Switzerland, atomic nuclei are collided at ultra-relativistic energies. Many final-state particles are produced in each collision and their properties are measured by the ALICE detector. The detector signals induced by the produced particles are digitized leading to data rates that are in excess of 48 GB/s. The ALICE High Level Trigger (HLT) system pioneered the use of FPGA- and GPU-based algorithms to reconstruct charged-particle trajectories and reduce the data size in real time. The results of the reconstruction of the collision events, available online, are used for high level data quality and detector-performance monitoring and real-time time-dependent detector calibration. The online data compression techniques developed and used in the ALICE HLT have more than quadrupled the amount of data that can be stored for offline event processing.
Raytracing und Szenengraphen
(2006)
Raytracing ist ein bekanntes Verfahren zur Erzeugung fotorealistischer Bilder. Globale Beleuchtungseffekte einer 3D-Szene werden durch das Raytracing-Verfahren physikalisch korrekt dargestellt. Erst aktuelle Forschungsarbeiten ermöglichen es, das sehr rechenintensive Verfahren bei interaktiven Bildraten in Echtzeit zu berechnen. Komplexe 3D-Szenen, wie sie beispielsweise in 3D-Spielen oder Simulationen vorkommen, können durch einen Szenengraphen modelliert und animiert werden. Damit die Rendering-Ergebnisse eines Szenengraphen näher an einem realen Bild liegen, ist es erforderlich das Raytracing-Verfahren in einen Szenengraphen einzugliedern. In dieser Arbeit werden die Möglichkeiten zur Integration eines Echtzeit-Raytracers in eine Szenengraph-API untersucht. Ziel dieser Diplomarbeit ist die Darstellung dynamischer Szenen bei interaktiven Bildraten unter Verwendung des Raytracing-Verfahrens auf einem herkömmlichen PC. Zunächst müssen bestehende Open Source Szenengraph-APIs und aktuelle Echtzeit-Raytracer auf ihre Eignung zur Integration hin überprüft werden. Bei der Verarbeitung dynamischer Szenen spielt die verwendete Beschleunigungsdatenstruktur des Raytracers eine entscheidende Rolle. Da eine komplette Neuerstellung der Datenstruktur in jedem Bild zuviel Zeit in Anspruch nimmt, ist eine schnelle und kostengünstige Aktualisierung erforderlich. Die in [LAM01] vorgestellte Lösung, eine Hüllkörperhierarchie (BVH) als Beschleunigungsdatenstruktur zu verwenden, fügt sich sehr gut in das Konzept eines Szenengraphen ein. Dadurch wird eine einfache Aktualisierung ermöglicht. Um das Ziel dieser Arbeit zu erreichen, ist es notwendig, die Parallelisierbarkeit des Raytracing-Verfahrens auszunutzen. Purcell zeigt in [Pur04], dass Grafikprozessoren (GPUs) neben ihrer eigentlichen Aufgabe auch für allgemeine, parallele Berechnungen wie das Raytracing verwendet werden können. Die in bisherigen Arbeiten über GPU-basiertes Raytracing entwickelten Systeme können dynamische Szenen nicht bei interaktiven Bildraten darstellen. Aus diesem Grund wird in dieser Diplomarbeit ein neues System konzipiert und implementiert, das den in [TS05] entwickelten Raytracer erweitert und in die Open Source Szenengraph-API OGRE 3D integriert. Das implementierte System ermöglicht die Darstellung statischer und dynamischer Szenen unter Verwendung einer Consumer-Grafikkarte bei interaktiven Bildraten. Durch seine Erweiterbarkeit bildet das System das Grundgerüst für ein Realtime-High-Quality-Rendering-System.
Raytracing und Szenegraphen
(2006)
Raytracing ist ein bekanntes Verfahren zur Erzeugung fotorealistischer Bilder. Globale Beleuchtungseffekte einer 3D-Szene werden durch das Raytracing-Verfahren physikalisch korrekt dargestellt. Erst aktuelle Forschungsarbeiten erm¨oglichen es, das sehr rechenintensive Verfahren bei interaktiven Bildraten in Echtzeit zu berechnen.
Komplexe 3D-Szenen, wie sie beispielsweise in 3D-Spielen oder Simulationen vorkommen, können durch einen Szenengraphen modelliert und animiert werden. Damit die Rendering-Ergebnisse eines Szenengraphen n¨aher an einem realen Bild liegen, ist es erforderlich das Raytracing-Verfahren in einen Szenengraphen einzugliedern.
In dieser Arbeit werden die Möglichkeiten zur Integration eines Echtzeit-Raytracers in eine Szenengraph-API untersucht. Ziel dieser Diplomarbeit ist die Darstellung dynamischer Szenen bei interaktiven Bildraten unter Verwendung des Raytracing-Verfahrens auf einem herk¨ommlichen PC. Zun¨achst m¨ussen bestehende Open Source Szenengraph-APIs und aktuelle Echtzeit-Raytracer auf ihre Eignung zur Integration hin überprüft werden.
Bei der Verarbeitung dynamischer Szenen spielt die verwendete Beschleunigungsdatenstruktur des Raytracers eine entscheidende Rolle. Da eine komplette Neuerstellung der Datenstruktur in jedem Bild zuviel Zeit in Anspruch nimmt, ist eine schnelle und kostengünstige Aktualisierung erforderlich. Die in [LAM01] vorgestellte Lösung, eine Hüllkörperhierarchie (BVH) als Beschleunigungsdatenstruktur zu verwenden, fügt sich sehr gut in das Konzept eines Szenengraphen ein. Dadurch wird eine einfache Aktualisierung ermöglicht.
Um das Ziel dieser Arbeit zu erreichen, ist es notwendig, die Parallelisierbarkeit des Raytracing-Verfahrens auszunutzen. Purcell zeigt in [Pur04], dass Grafikprozessoren (GPUs) neben ihrer eigentlichen Aufgabe auch für allgemeine, parallele Berechnungen wie das Raytracing verwendet werden können.
Die in bisherigen Arbeiten über GPU-basiertes Raytracing entwickelten Systeme können dynamische Szenen nicht bei interaktiven Bildraten darstellen. Aus diesem Grund wird in dieser Diplomarbeit ein neues System konzipiert und implementiert, das den in [TS05] entwickelten Raytracer erweitert und in die Open Source Szenengraph-API OGRE 3D integriert.
Das implementierte System ermöglicht die Darstellung statischer und dynamischer Szenen unter Verwendung einer Consumer-Grafikkarte bei interaktiven Bildraten. Durch seine Erweiterbarkeit bildet das System das Grundger¨ust für ein Realtime-High-Quality-Rendering-System.
The production yields of antideuterons and antiprotons are measured in pp collisions at a center-of-mass energy of √s=13 TeV, as a function of transverse momentum (pT) and rapidity (y), for the first time up to |y|=0.7. The measured spectra are used to study the pT and rapidity dependence of the coalescence parameter B2, which quantifies the coalescence probability of antideuterons. The pT and rapidity dependence of the obtained B2 is extrapolated for pT>1.7 GeV/c and |y|>0.7 using the phenomenological antideuteron production model implemented in PYTHIA 8.3 as well as a baryon coalescence afterburner model based on EPOS 3. Such measurements are of interest to the astrophysics community, since they can be used for the calculation of the flux of antinuclei from cosmic rays, in combination with coalescence models.
We have studied the transverse-momentum (pT) dependence of the inclusive J/ψ production in p-Pb collisions at sNN−−−√=5.02 TeV, in three center-of-mass rapidity (ycms) regions, down to zero pT. Results in the forward and backward rapidity ranges (2.03<ycms<3.53 and −4.46<ycms<−2.96) are obtained by studying the J/ψ decay to μ+μ−, while the mid-rapidity region (−1.37<ycms<0.43) is investigated by measuring the e+e− decay channel. The pT dependence of the J/ψ production cross section and nuclear modification factor are presented for each of the rapidity intervals, as well as the J/ψ mean pT values. Forward and mid-rapidity results show a suppression of the J/ψ yield, with respect to pp collisions, which decreases with increasing pT. At backward rapidity no significant J/ψ suppression is observed. Theoretical models including a combination of cold nuclear matter effects such as shadowing and partonic energy loss, are in fair agreement with the data, except at forward rapidity and low transverse momentum. The implications of the p-Pb results for the evaluation of cold nuclear matter effects on J/ψ production in Pb-Pb collisions are also discussed.
We have studied the transverse-momentum (pT) dependence of the inclusive J/ψ production in p-Pb collisions at sNN−−−√=5.02 TeV, in three center-of-mass rapidity (ycms) regions, down to zero pT. Results in the forward and backward rapidity ranges (2.03<ycms<3.53 and −4.46<ycms<−2.96) are obtained by studying the J/ψ decay to μ+μ−, while the mid-rapidity region (−1.37<ycms<0.43) is investigated by measuring the e+e− decay channel. The pT dependence of the J/ψ production cross section and nuclear modification factor are presented for each of the rapidity intervals, as well as the J/ψ mean pT values. Forward and mid-rapidity results show a suppression of the J/ψ yield, with respect to pp collisions, which decreases with increasing pT. At backward rapidity no significant J/ψ suppression is observed. Theoretical models including a combination of cold nuclear matter effects such as shadowing and partonic energy loss, are in fair agreement with the data, except at forward rapidity and low transverse momentum. The implications of the p-Pb results for the evaluation of cold nuclear matter effects on J/ψ production in Pb-Pb collisions are also discussed.
We have studied the transverse-momentum (pT) dependence of the inclusive J/ψ production in p-Pb collisions at sNN−−−√=5.02 TeV, in three center-of-mass rapidity (ycms) regions, down to zero pT. Results in the forward and backward rapidity ranges (2.03<ycms<3.53 and −4.46<ycms<−2.96) are obtained by studying the J/ψ decay to μ+μ−, while the mid-rapidity region (−1.37<ycms<0.43) is investigated by measuring the e+e− decay channel. The pT dependence of the J/ψ production cross section and nuclear modification factor are presented for each of the rapidity intervals, as well as the J/ψ mean pT values. Forward and mid-rapidity results show a suppression of the J/ψ yield, with respect to pp collisions, which decreases with increasing pT. At backward rapidity no significant J/ψ suppression is observed. Theoretical models including a combination of cold nuclear matter effects such as shadowing and partonic energy loss, are in fair agreement with the data, except at forward rapidity and low transverse momentum. The implications of the p-Pb results for the evaluation of cold nuclear matter effects on J/ψ production in Pb-Pb collisions are also discussed.
Rapidity and transverse momentum dependence of inclusive J/ψ production in pp collisions at √s=7 TeV
(2011)
The ALICE experiment at the LHC has studied inclusive J/ψ production at central and forward rapidities in pp collisions at √s=7 TeV. In this Letter, we report on the first results obtained detecting the J/ψ through the dilepton decay into e+e− and μ+μ− pairs in the rapidity ranges |y|<0.9 and 2.5<y<4, respectively, and with acceptance down to zero pT. In the dielectron channel the analysis was carried out on a data sample corresponding to an integrated luminosity Lint=5.6 nb−1 and the number of signal events is NJ/ψ=352±32(stat.)±28(syst.); the corresponding figures in the dimuon channel are Lint=15.6 nb−1 and NJ/ψ=1924±77(stat.)±144(syst.). The measured production cross sections are σJ/ψ(|y|<0.9)=10.7±1.0(stat.)±1.6(syst.)−2.3+1.6(syst.pol.)μb and σJ/ψ(2.5<y<4)=6.31±0.25(stat.)±0.76(syst.)−1.96+0.95(syst.pol.)μb. The differential cross sections, in transverse momentum and rapidity, of the J/ψ were also measured.