Browsing by Subject "Lattice theory"
Now showing 1 - 7 of 7
- Results Per Page
- Sort Options
Item Applications of lattice theory to model checking(2008-08) Kashyap, Sujatha; Garg, Vijay K. (Vijay Kumar), 1963-Society is increasingly dependent on the correct operation of concurrent and distributed software systems. Examples of such systems include computer networks, operating systems, telephone switches and flight control systems. Model checking is a useful tool for ensuring the correctness of such systems, because it is a fully automatic technique whose use does not require expert knowledge. Additionally, model checking allows for the production of error trails when a violation of a desired property is detected. Error trails are an invaluable debugging aid, because they provide the programmer with the sequence of events that lead to an error. Model checking typically operates by performing an exhaustive exploration of the state space of the program. Exhaustive state space exploration is not practical for industrial use in the verification of concurrent systems because of the well-known phenomenon of state space explosion caused by the exploration of all possible interleavings of concurrent events. However, the exploration of all possible interleavings is not always necessary for verification. In this dissertation, we show that results from lattice theory can be applied to ameliorate state space explosion due to concurrency, and to produce short error trails when an error is detected. We show that many CTL formulae exhibit lattice-theoretic structure that can be exploited to avoid exploring multiple interleavings of a set of concurrent events. We use this structural information to develop efficient model checking techniques for both implicit (partial order) and explicit (interleaving) models of the state space. For formulae that do not exhibit the required structure, we present a technique called predicate filtering, which uses a weaker property with the desired structural characteristics to obtain a reduced state space which can then be exhaustively explored. We also show that lattice theory can be used to obtain a path of shortest length to an error state, thereby producing short error trails that greatly ease the task of debugging. We provide experimental results from a wide range of examples, showing the effectiveness of our techniques at improving the efficiency of verifying and debugging concurrent and distributed systems. Our implementation is based on the popular model checker SPIN, and we compare our performance against the state-of-the-art state space reduction strategies implemented in SPIN.Item The Brandt module of ternary quadratic lattices(2005) Tornaría López, Gonzalo; Rodriguez-Villegas, FernandoGiven a positive definite ternary quadratic lattice Λ, we construct a free module M(Λ) with Hecke action, together with a family of Hecke-linear maps ϑl from M(Λ) to certain spaces of modular forms of half integral weight. The latter are given explicitly by a new kind of generalized theta series, which we prove to be modular with level independent of l. Key to our work is the introduction of a refinement to the classic notion of proper equivalence of lattices.Item Cusps of arithmetic orbifolds(2006) McReynolds, David Ben; Reid, Alan W.This dissertation investigates cusp cross-sections of arithmetic real, complex, and quaternionic hyperbolic n–orbifolds. We give a smooth classification of these submanifolds and analyze their induced geometry. One of the primary tools is a new subgroup separability result for general arithmetic lattices.Item Dynamics of quantum control in cold-atom systems(2009-05) Roy, Analabha, 1978-; Reichl, L. E.The dynamics of mesoscopic two-boson systems that model an interacting pair of ultracold alkali atoms in the presence of electromagnetic potentials are considered. The translational degrees of freedom of such a system can be described by a simple reduced atom Hamiltonian. Introducing time modulations in the laser fields causes parametric variations of the Hamiltonian's Floquet eigenvalue spectrum. Broken symmetries cause level repulsion and avoided crossings in this spectrum that are quantum manifestations of the chaos in the underlying classical dynamics of the systems. We investigate the effects of this phenomenon in the coherent control of excitations in these systems. These systems can be coherently excited from their ground states to higher energy states via a Stimulated Raman Adiabatic Passage (STIRAP). The presence of avoided crossings alter the outcome of STIRAP. First, the classical dynamics of such two-boson systems in double wells is described and manifestations of the same to the quantum mechanical system are discussed. Second, the quantum dynamics of coherent control in the manner discussed above is detailed for a select choice(s) of system parameters. Finally, the same chaos-assisted adiabatic passage is demonstrated for optical lattice systems based on experiments on the same done with noninteracting atoms.Item Fast multiscale methods for lattice equations(2002) Martinsson, Per-Gunnar Johan; Rodin, G. J.; Babuška, IvoThe thesis concerns multi-scale analysis of equations defined on very large lattices. A new method for model reduction that allows the resolution scale to vary with spatial position is presented. It leads to fast numerical implementations and comes with strict error bounds. This is obtained by incorporating the averaging of the micro-structure directly into a solver that is based on hierarchical data structures, such as the Fast Multipole Method. For boundary value problems, a lattice analogue of the boundary element method is used. Homogenized equations of arbitrary order are derived and strict error bounds are proved. For mechanical lattice structures, special attention is paid to the question of non-degeneracy and whether rotational degrees of freedom should be incorporated. A computer program that automatically derives the homogenized equations was developed. For any lattice geometry, the lattice Green’s function is determined and its asymptotic expansion in rational poly-harmonic functions is derived. The presented results have applications in many areas of physics and engineering but particular attention is paid to how they can be used to design composite materials with high stiffness-to-weight ratios and prescribed wave-propagation modes. In particular, it is shown how to design materials that have phononic bandgaps, in other words, they block mechanical waves of certain frequencies.Item Monte Carlo simulations of pure chain fluids and chain fluid mixtures : size and chain length effects on thermodynamic properties(1995-05) Kirmse, Katherine Marie; Not availableItem The self-assembly of colloidal particles into 2D arrays(2007-12) Rabideau, Brooks Douglas, 1979-; Bonnecaze, R. T. (Roger T.)As the feature size of new devices continues to decrease so too does the feasibility of top-down methods of patterning them. In many cases bottom-up methods are replacing the existing methods of assembly, as having building blocks self-organize into the desired structure appears, in many cases, to be a much more advantageous route. Self-assembled nanoparticulate films have a wide range of potential applications; high-density magnetic media, sensing arrays, meta-materials and as seeds for 3D photonic crystals to name a few. Thus, it is critical that we understand the fundamental dynamics of pattern formation on the nanoparticulate and colloidal scale so that we may have better control over the formation and final quality of these structures. We study computationally the self-organization of colloidal particles in 2D using both Monte Carlo and dynamic simulation We present 3 studies employing Monte Carlo simulation. In the first study, Monte Carlo simulations were used to understand the experimental observation of highlyordered 2D arrays of bidisperse, stabilized gold nanoparticles. It was shown that the LS lattice forms with the addition of interparticle forces and a simple compressive force, revealing that bidisperse lattice formation is, in fact, a dynamic process. It was evident that the LS lattice forms in large part because the particles within the lattice reside in their respective interparticle potential wells. In the second Monte Carlo study, this information was used to predict size-ratios and surface coverages for novel lattice structures. These predictions are intended to guide experimentalists in their search for these exciting new structures. In the third study it was shown that polydisperse amounts of amorphous-silicon nanoparticles could form 2D clusters exhibiting long-range orientational order even in the absence of translational order. Monte Carlo simulations were performed, which included lateral capillary forces and a simple stabilizing repulsion, resulting in structures that were strikingly similar to the experimentally observed In the fourth study we used dynamic simulation to study the hydrodynamicallyassisted self-organization of DNA-functionalized colloids in 2D. It was shown that hydrodynamic forces allow a more thorough sampling of phase space than through thermal or Brownian forces alone.