The complementary prism of a graph G is obtained from a copy of G and its complement G̅ by adding a perfect matching between the corresponding vertices of G and G̅. For any graph G, a set D ⊆ V (G) is a double dominating set (DDS) if that set dominates every vertex of G twice. The double domination number, denoted γ×2(G), is the cardinality of a minimum double dominating set of G. We have proven results on graphs of small order, specific families and lower bounds on γ×2(GG̅).

Let $G$ be any graph and let $\overline{G}$ be its complement. The complementary prism of $G$ is formed from the disjoint union of a graph $G$ and its complement $\overline{G}$ by adding the edges of a perfect matching between the corresponding vertices of $G$ and $\overline{G}$. An Italian dominating function on a graph $G$ is a function such that $f \, : \, V \to \{ 0,1,2 \}$ and for each vertex $v \in V$ for which $f(v)=0$, it holds that $\sum_{u \in N(v)} f(u) \geq 2$. The weight of an Italian dominating function is the value $f(V)=\sum_{u \in V(G)}f(u)$. The minimum weight of all such functions on $G$ is called the Italian domination number. In this thesis we will study Italian domination in complementary prisms. First we will present an error found in one of the references. Then we will define the small values of the Italian domination in complementary prisms, find the value of the Italian domination number in specific families of graphs complementary prisms, and conclude with future problems.

No / The ability of prisms to effectively dissipate contact stress at the surface will influence wear rates in teeth. The aim of this investigation was to begin to quantify the effect of prism orientation on surface stresses. Seven finite element models of enamel microstructure were created, each model differing in the angulation of prism orientation with regard to the wear surface. For validation purposes, the mechanical behavior of the model was compared with published experimental data. In order to test the enamel under lateral loads, a compressed food particle was dragged across the surface from the dentino-enamel junction (DEJ) towards the outer enamel surface (OES). Under these conditions, tensile stresses in the enamel model increased with increases in the coefficient of friction. More importantly, stresses were found to be lowest in models in which the prisms approach the surface at lower angles (i.e., more obliquely cut prisms), and highest when the prisms approached the surface at 60° (i.e., less obliquely cut). Finally, the direction of travel of the simulated food particle was reversed, allowing comparison of the difference in behavior between trailing and leading edge enamels (i.e., when the food particle was dragged either towards or away from the DEJ). Stresses at the trailing edge were usually lower than stresses at the leading edge. Taken together with what is known about prism orientation in primate teeth, such findings imply greater wear resistance at the intercuspal region and less wear resistance at the lateral enamel at midcrown. Such findings appear to be supported by archeological evidence.

No description available.

No description available.

Vorticity modeling is used to simulate the flow around a surface-mounted prism. The objective is to examine whether vorticity modeling can give satisfactory information about surface pressure fluctuations which are mostly due to the outer or inviscid flow. Differences between results obtained with vorticity modeling and what one should expect from DNS and LES are pointed out. These include the difference between the governing equations, the shortcomings of having a 2-D simulation and the realization of introducing and convecting vorticity to simulate some turbulence aspects. All necessary details needed for the setup of vorticity modeling for complex flows, such as the one considered here are given. These details include choice of elements, the calculation of velocities, the application of boundary conditions and calculation of pressure. The numerical procedure and our use of parallelization in the code are explained. The results presented on velocity magnitude, vorticity and pressure show important characteristics of the flow field in terms of interaction of positive and negative vorticities and their effects on the surface pressure. The calculated peak and mean values for the pressure coefficients at the leading edge are close to those measured in separating flows over prisms. / Master of Science

The issue of the effects of free stream turbulence on the flow field over a surface-mounted prism is examined through experimental and numerical investigations. In the experimental studies, particle image velocimetry measurements are conducted in the ESM water tunnel at Reynolds number of $9,600$ and under two cases of turbulent inflow conditions. The results show that the mean flow separation, reattachment and parameters such as mean velocity, root mean square, Reynolds stresses and turbulent kinetic energy are affected by the turbulence characteristics of the incident flow. The instantaneous dynamics of the interactions between the separating shear layer and the solid wall and between the shear layer and the turbulence in the incident flow are detailed. In the numerical studies, large eddy simulations of the flow over a surface-mounted prism under two inflow conditions, namely, smooth inflow and isotropic homogeneous turbulence inflow, are performed. The use of a fifth-order scheme (CUD-II-5), which is a member of a family of Compact Upwind Difference schemes, in large eddy simulations of this flow is assessed. The performance of this scheme is validated by comparing the rate of temporal decay of isotropic turbulence with available experimental measurements for grid-generated turbulence. The results show that the spectra are sensitive to the method of flux vector splitting needed for the implementation of the upwind scheme. With van Leer splitting, the CUD-II-5 scheme is found to be too dissipative. On the other hand, using the Lax-Friedrichs vector splitting yields good agreement with experiments by controlling the level of artificial dissipation. This led us to recommend a new procedure, we denote by C6CUD5 scheme, that combines a compact sixth-order scheme with the CUD-II-5 scheme for large eddy simulation of complex flows. The simulation results, including flow patterns, pressure fields and turbulence statistics show that the CUD-II-5 scheme, with Lax-Friedricks flux vector splitting, provides high resolution of local flow structures. The results present new physical aspects of the flow topology over surface-mounted prisms. The effects of the incident homogeneous turbulence on the size of the separation region and suction pressures are determined by pointing out differences in the flow topologies between the two incident flow cases. / Ph. D.

An entry for the World Trade Center Memorial Competition was expanded upon as a study into the nature of design. The project influenced its own evolution and revealed exciting outcomes. The memorial is a reinforced concrete tower with an acrylic water tank at the top. The water tank acts as a prism casting colorful light displays both in the tower and around the site. The tank is also the source for continually falling droplets of water. The drops fall 450 feet through an open chamber to land in a shallow overflowing pool and then wash over a stone sepulcher containing the unidentified remains of victims. / Master of Architecture

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

Nous nous intéressons à l'analyse des exigences de performabilité des systèmes communicants mobiles par model checking. Nous modélisons ces systèmes à l'aide d'un formalisme de haut niveau issu du π-calcul, permettant de considérer des comportements stochastiques, temporels, déterministes, ou indéterministes. Cependant, dans le π-calcul, la primitive de communication de base des systèmes est la communication en point-à-point synchrone. Or, les systèmes mobiles, qui utilisent des réseaux sans fil, communiquent essentiellement par diffusion locale. C'est pourquoi, dans un premier temps, nous définissons la communication par diffusion dans le π-calcul, afin de mieux modéliser les systèmes que nous étudions. Nous proposons d'utiliser des versions probabilistes et stochastiques de l'algèbre que nous avons défini, pour permettre des études de performance. Nous en définissons une version temporelle permettant de considérer le temps dans les modèles. Mais l'absence d'outils d'analyse des propriétés sur des modèles spécifiés en une algèbre issue du π-calcul est un obstacle majeur à notre travail. La définition de règles de traduction en langage PRISM, nous permet de traduire nos modèles, en modèles de bas niveau supports du model checking, à savoir des chaînes de Markov à temps discret, à temps continu, des automates temporisés, ou des automates temporisés probabilistes. Nous avons choisi l'outil PRISM car, à notre connaissance, dans sa dernière version, il est le seul outil à supporter les formalismes de bas niveau que nous venons de citer, et ainsi il permet de réaliser des études de performabilité complètes. Cette façon de procéder nous permet de pallier à l'absence d'outils d'analyse pour nos modèles. Par la suite, nous appliquons ces concepts théoriques aux réseaux de capteurs sans fil mobiles. / We are interested in analyzing the performability requirements of mobile communication systems by using model checking techniques. We model these systems using a high-level formalism derived from the π-calculus, for considering stochastic, timed, deterministic or indeterministic behaviors. However, in the π-calculus, the basic communication primitive of systems is the synchronous point-to-point communication. However, mobile systems that use wireless networks, mostly communicate by local broadcast. Therefore, we first define the broadcast communication into the π-calculus, to better model the systems we study. We propose to use probabilistic and stochastic versions of the algebra we have defined to allow performance studies. We define a temporal version to consider time in the models. But the lack of tools for analyzing properties of models specified with π-calculus is a major obstacle to our work and its objectives. The definition of translation rules into the PRISM language allows us to translate our models in low-level models which can support model checking, namely discrete time, or continuous time Markov chains, timed automata, or probabilistic timed automata. We chose the PRISM model checker because, in our best knowledge, in its latest version, it is the only tool that supports the low-level formalisms that we have previously cited, and thus, makes it possible to realize complete performability studies. This approach allows us to overcome the lack of model checkers for our models. Subsequently, we apply these theoretical concepts to analyse performability of mobile wireless sensor networks.