Computer hardware and software laid the foundation for fundamental innovations in science, technology, economics and society. Novel application areas generate an ever-increasing demand for computation power and storage capacities. Classic CMOS-based hardware and the von Neumann architecture are approaching their limits in miniaturization, power density and communication speed. To meet future demands, researchers work on new device technologies and architecture approaches which in turn require new algorithms and a hardware/software co-design to exploit their capabilities. Since the overall system heterogeneity and complexity increases, the challenge is to build systems with these technologies that are both correct and performant by design. Formal methods in general and model checking in particular are established verification methods in hardware design, and have been successfully applied to many hardware, software and integrated hardware/software systems. In many systems, probabilistic effects arise naturally, e.g., from input patterns, production variations or the occurrence of faults. Probabilistic model checking facilitates the quantitative analysis of performance and reliability measures in stochastic models that formalize this probabilism. The interdisciplinary research project Center for Advancing Electronics Dresden, cfaed for short, aims to explore hardware and software technologies for future information processing systems. It joins the research efforts of different groups working on technologies for all system layers ranging from transistor device research over system architecture up to the application layer. The collaborations among the groups showed a demand for new formal methods and enhanced tools to assist the design and analysis of technologies at all system layers and their cross-layer integration. Addressing these needs is the goal of this thesis. This work contributes to probabilistic model checking for Markovian models with new methods to compute two essential measures in the analysis of hardware/software systems and a method to tackle the state-space explosion problem: 1) Conditional probabilities are well known in stochastic theory and statistics, but efficient methods did not exist to compute conditional expectations in Markov chains and extremal conditional probabilities in Markov decision processes. This thesis develops new polynomial-time algorithms, and it provides a mature implementation for the probabilistic model checker PRISM. 2) Relativized long-run and relativized conditional long-run averages are proposed in this work to reason about probabilities and expectations in Markov chains on the long run when zooming into sets of states or paths. Both types of long-run averages are implemented for PRISM. 3) Symmetry reduction is an effective abstraction technique to tame the state-space explosion problem. However, state-of-the-art probabilistic model checkers apply it only after building the full model and offer no support for specifying non-trivial symmetric components. This thesis fills this gap with a modeling language based on symmetric program graphs that facilitates symmetry reduction on the source level. The new language can be integrated seamlessly into the PRISM modeling language. This work contributes to the research on future hardware/software systems in cfaed with three practical studies that are enabled by the developed methods and their implementations. 1) To confirm relevance of the new methods in practice and to validate the results, the first study analyzes a well-understood synchronization protocol, a test-and-test-and-set spinlock. Beyond this confirmation, the analysis demonstrates the capability to compute properties that are hardly accessible to measurements. 2) Probabilistic write-copy/select is an alternative protocol to overcome the scalability issues of classic resource-locking mechanisms. A quantitative analysis verifies the protocol's principle of operation and evaluates the performance trade-offs to guide future implementations of the protocol. 3) The impact of a new device technology is hard to estimate since circuit-level simulations are not available in the early stages of research. This thesis proposes a formal framework to model and analyze circuit designs for novel transistor technologies. It encompasses an operational model of electrical circuits, a functional model of polarity-controllable transistor devices and algorithms for design space exploration in order to find optimal circuit designs using probabilistic model checking. A practical study assesses the model accuracy for a lab-device based on germanium nanowires and performs an automated exploration and performance analysis of the design space of a given switching function. The experiments demonstrate how the framework enables an early systematic design space exploration and performance evaluation of circuits for experimental transistor devices.:1. Introduction 1.1 Related Work 2. Preliminaries 3. Conditional Probabilities in Markovian Models 3.1 Methods for Discrete- and Continuous-Time Markov Chains 3.2 Reset Method for Markov Decision Processes 3.3 Implementation 3.4 Evaluation and Comparative Studies 3.5 Conclusion 4. Long-Run Averages in Markov Chains 4.1 Relativized Long-Run Average 4.2 Conditional State Evolution 4.3 Implementation 4.4 Conclusion 5. Language-Support for Immediate Symmetry Reduction 5.1 Probabilistic Program Graphs 5.2 Symmetric Probabilistic Program Graphs 5.3 Implementation 5.4 Conclusion 6. Practical Applications of the Developed Techniques 6.1 Test-and-Test-and-Set Spinlock: Quantitative Analysis of an Established Protocol 6.2 Probabilistic Write/Copy-Select: Quantitative Analysis as Design Guide for a Novel Protocol 6.3 Circuit Design for Future Transistor Technologies: Evaluating Polarity-Controllable Multiple-Gate FETs 7. Conclusion Bibliography Appendices A. Conditional Probabilities and Expectations A.1 Selection of Benchmark Models A.2 Additional Benchmark Results A.3 Comparison PRISM vs. Storm B. Language-Support for Immediate Symmetry Reduction B.1 Syntax of the PRISM Modeling Language B.2 Multi-Core Example C. Practical Applications of the Developed Techniques C.1 Test-and-Test-and-Set Spinlock C.2 Probabilistic Write/Copy-Select C.3 Circuit Design for Future Transistor Technologies

In dieser Arbeit wird Terahertzspektroskopie (THz) eingesetzt, um nichtlineare niederfrequente Anregungen von kondensierter Materie zu untersuchen. Insbesondere die Anwendung zweidimensionaler (2D) THz-Spektroskopie ermöglicht es, verschiedene Beiträge zu nichtlinearen Signalen zu entflechten. Zunächst wird die nichtlineare polaronische Antwort solvatisierter Elektronen und umliegenden Lösungsmittelmolekülen in der polaren Flüssigkeit Isopropanol erforscht. Solvatisierte Elektronen werden durch Multiphotonen-Ionisation erzeugt. Longitudinale Polaronoszillationen mit THz-Frequenzen werden während der ultraschnellen Lokalisierung der Elektronen impulsiv angeregt. Die Störung solcher Polaronschwingungen mit einem externen THz-Impuls führt zu nichtlinearen Änderungen der transversalen Polaron-Polarisierbarkeit, die sich in deutlichen Änderungen der Oszillationsphase zeigen. Darüber hinaus wird die Erzeugung monozyklischer THz-Impulse in asymmetrischen Halbleiter-Quantentrögen bei resonanter Intersubband-Anregung im Mittelinfraroten (MIR) demonstriert. Die zeitliche Form des emittierten elektrischen THz-Feldes wird durch die Steuerung der Impulsdauer und des elektrischen Feldes der MIR Impulse verändert. Phasenaufgelöste 2D-MIR-Experimente bestätigen, dass die THz-Emission vorrangig auf einen nichtlinearen Verschiebungsstrom bei Femtosekunden-Intersubband-Anregung zurückzuführen ist. Der Einfluss von Intra- und Interbandströmen auf Symmetrieeigenschaften wird in 2D-THz-Experimenten an Wismut demonstriert. Nichtperturbative langwellige Anregung von Ladungsträgern nahe der L-Punkte führt zu einer anisotropen Ladungsträgerverteilung, die sich in einer hexagonalen Winkelabhängigkeit der pump-induzierten THz Transmission manifestiert. Eine damit einhergehende Symmetrieverringerung für bestimmte elektrische Feldpolarisationen erlaubt die Anregung von Zonenrand-Phononen, welche sich in in oszillierenden Signalen in der nichtlinearen 2D-THz-Antwort manifestieren. / This thesis exploits techniques of terahertz (THz) spectroscopy to investigate nonlinear low-frequency excitations of condensed matter. In particular, application of two-dimensional (2D) THz spectroscopy allows to disentangle different nonlinear signal contributions. The nonlinear polaronic response of solvated electrons and their surrounding solvent molecules in the polar liquid isopronal is studied. Solvated electrons are generated via multiphoton ionization. Longitudinal polaron oscillations with THz frequencies are impulsively excited during the ultrafast localization of the electrons. Perturbation of such polaron oscillations with an external THz pulse induces nonlinear changes of the transverse polaron polarizability, reflected in distinct modifications to the oscillation phase as mapped in 2D-THz experiments. Further, the generation of mono-cycle THz pulses from asymmetric semiconductor quantum wells upon resonant intersubband excitation in the mid-infrared (MIR) range is demonstrated. The temporal shape of the emitted THz electric field is modified by controlling pulse duration and peak electric field of the MIR driving pulses. Phase-resolved 2D-MIR experiments confirm that the THz emission is predominantly due to a nonlinear shift current generated upon femtosecond intersubband excitation. The influence of combined intra- and interband currents on symmetry properties, which opens novel quantum pathways for phonon excitation in narrow-band-gap materials, is demonstrated by 2D-THz experiments on bismuth. Nonperturbative long-wavelength excitation of charge carriers close to the L points leads to an anisotropic carrier distribution, reflected in a six-fold azimuthal angular dependence of the pump-induced change of THz transmission. A concomitant symmetry reduction for certain electric-field polarizations allows for the excitation of phonons at the zone boundary which are reflected in oscillatory signals in the nonlinear 2D-THz response.