Quantum transition state theory and solving a first order master equation for complex reactions numerically

The field of chemical kinetics is an exciting and active field. The prevailing theories make a number of simplifying assumptions that do not always hold in actual cases. Another current problem concerns a development of efficient numerical algorithms for solving the master equations that arise in the description of complex reactions. The objective of the present work is to furnish a completely general and exact theory of reaction rates, in a form reminiscent of transition state theory, valid for all fluid phases and also to develop a computer program that can solve complex reactions by finding the concentrations of all participating substances as a function of time. To do so, the full quantum scattering theory is used for deriving the exact rate law, and then the resulting cumulative reaction probability is put into several equivalent forms that take into account all relativistic effects if applicable, including one that is strongly reminiscent of transition state theory, but includes corrections from scattering theory. Then two programs, one for solving complex reactions, the other for solving first order linear kinetic master equations to solve them, have been developed and tested for simple applications.

The correlation of structure and electronic properties near the surface of transition metal oxides

The strong couplings between different degrees of freedom are believed to be responsible for novel and complex phenomena discovered in transition metal oxides (TMOs). The physical complexity is directly responsible for their tunability. Creating surfaces/interfaces add an additional ' man-made' twist, approaching the quantum phenomena of correlated materials. ^ The dissertation focused on the structural and electronic properties in proximity of surface of three prototype TMO compounds by using three complementary techniques: scanning tunneling microscopy, angle-resolved photoelectron spectroscopy and low energy electron diffraction, particularly emphasized the effects of broken symmetry and imperfections like defects on the coupling between charge and lattice degrees of freedom. ^ Ca1.5Sr0.5RuO4 is a layered ruthenate with square lattice and at the boundary of magnetic/orbital instability in Ca2-xSrxRuO4. That the substitution of Sr 2+ with Ca2+ causing RuO6 rotation narrows the dxy band width and changes the Fermi surface topology. Particularly, the γ(dxy) Fermi surface sheet exhibited hole-like in Ca1.5Sr0.5RuO4 in contrast to electron-like in Sr2RuO4, showing a strong charge-lattice coupling. ^ Na0.75CoO2 is a layered cobaltite with triangular lattice exhibiting extraordinary thermoelectric properties. The well-ordered CoO2-terminated surface with random Na distribution was observed. However, lattice constants of the surface are smaller than that in bulk. The surface density of states (DOS) showed strong temperature dependence. Especially, an unusual shift of the minimum DOS occurs below 230 K, clearly indicating a local charging effect on the surface. ^ Cd2Re2O7 is the first known pyrochlore oxide superconductor (Tc ∼ 1K). It exhibited an unusual second-order phase transition occurring at TS1 = 200 K and a controversial first-order transition at TS2 = 120 K. While bulk properties display large anomalies at TS1 but rather subtle and sample-dependent changes at TS2, the surface DOS near the EF show no change at T s1 but a substantial increase below TS2---a complete reversal as the signature for the transitions. We argued that crystal imperfections, mainly defects, which were considerably enhanced at the surface, resulted in the transition at TS2. ^

Colombian society in the 1990s: Fragmentation, legitimacy, and efficiency

During the nineties, Colombia experienced a two-fold process of restructuring. First, the political system underwent a process of constitutional reform in order to strengthen the state and increase its legitimacy, surpass the exclusionary character of the political regime, and achieve greater equity in the distribution of social resources. Second, the economy made the transition from a Keynesian development strategy to a strategy of “opening” or liberalization and internationalization of the economy, in order to increase the economic efficiency by reducing the “size” of the state and its regulatory role. The purpose of this dissertation is to analyze the interplay and contradictions of economic and political factors in the restructuring of the Colombian politico-economic system. ^ The main finding of this dissertation is that the simultaneous adoption of a neoliberal economic strategy and of the Political Constitution of 1991, have had a contradictory relationship: while the “political opening” has produced favorable conditions for fostering programs of democratization and social integration, the “economic opening” has counteracted that possibility given that it implies a social exclusionary process. This tension has aggravated the problems of political and social integration that have traditionally characterized Colombian society. ^ This crucial tension has also been characteristic of Latin America in the nineties. However, it has been neglected and undertheorized in most of the democratization studies of American comparative politics. Most of them lack consideration of structural aspects. According to those studies, the cause of regime change is determined by the strategic elections of actors. Contrary to these approaches, I develop a structural perspective. I consider that social phenomena are partly determined by structural factors, and scientific research should assign them decisive importance, since a fundamental basis for social action and transformation is to be found in the dynamics of relationships between individuals and structures and the development of contradictions within structures. ^

Formal modeling and analysis techniques for high level Petri nets

Petri Nets are a formal, graphical and executable modeling technique for the specification and analysis of concurrent and distributed systems and have been widely applied in computer science and many other engineering disciplines. Low level Petri nets are simple and useful for modeling control flows but not powerful enough to define data and system functionality. High level Petri nets (HLPNs) have been developed to support data and functionality definitions, such as using complex structured data as tokens and algebraic expressions as transition formulas. Compared to low level Petri nets, HLPNs result in compact system models that are easier to be understood. Therefore, HLPNs are more useful in modeling complex systems. ^ There are two issues in using HLPNs—modeling and analysis. Modeling concerns the abstracting and representing the systems under consideration using HLPNs, and analysis deals with effective ways study the behaviors and properties of the resulting HLPN models. In this dissertation, several modeling and analysis techniques for HLPNs are studied, which are integrated into a framework that is supported by a tool. ^ For modeling, this framework integrates two formal languages: a type of HLPNs called Predicate Transition Net (PrT Net) is used to model a system's behavior and a first-order linear time temporal logic (FOLTL) to specify the system's properties. The main contribution of this dissertation with regard to modeling is to develop a software tool to support the formal modeling capabilities in this framework. ^ For analysis, this framework combines three complementary techniques, simulation, explicit state model checking and bounded model checking (BMC). Simulation is a straightforward and speedy method, but only covers some execution paths in a HLPN model. Explicit state model checking covers all the execution paths but suffers from the state explosion problem. BMC is a tradeoff as it provides a certain level of coverage while more efficient than explicit state model checking. The main contribution of this dissertation with regard to analysis is adapting BMC to analyze HLPN models and integrating the three complementary analysis techniques in a software tool to support the formal analysis capabilities in this framework. ^ The SAMTools developed for this framework in this dissertation integrates three tools: PIPE+ for HLPNs behavioral modeling and simulation, SAMAT for hierarchical structural modeling and property specification, and PIPE+Verifier for behavioral verification.^

Formal Modeling and Analysis Techniques for High Level Petri Nets

Petri Nets are a formal, graphical and executable modeling technique for the specification and analysis of concurrent and distributed systems and have been widely applied in computer science and many other engineering disciplines. Low level Petri nets are simple and useful for modeling control flows but not powerful enough to define data and system functionality. High level Petri nets (HLPNs) have been developed to support data and functionality definitions, such as using complex structured data as tokens and algebraic expressions as transition formulas. Compared to low level Petri nets, HLPNs result in compact system models that are easier to be understood. Therefore, HLPNs are more useful in modeling complex systems. There are two issues in using HLPNs - modeling and analysis. Modeling concerns the abstracting and representing the systems under consideration using HLPNs, and analysis deals with effective ways study the behaviors and properties of the resulting HLPN models. In this dissertation, several modeling and analysis techniques for HLPNs are studied, which are integrated into a framework that is supported by a tool. For modeling, this framework integrates two formal languages: a type of HLPNs called Predicate Transition Net (PrT Net) is used to model a system's behavior and a first-order linear time temporal logic (FOLTL) to specify the system's properties. The main contribution of this dissertation with regard to modeling is to develop a software tool to support the formal modeling capabilities in this framework. For analysis, this framework combines three complementary techniques, simulation, explicit state model checking and bounded model checking (BMC). Simulation is a straightforward and speedy method, but only covers some execution paths in a HLPN model. Explicit state model checking covers all the execution paths but suffers from the state explosion problem. BMC is a tradeoff as it provides a certain level of coverage while more efficient than explicit state model checking. The main contribution of this dissertation with regard to analysis is adapting BMC to analyze HLPN models and integrating the three complementary analysis techniques in a software tool to support the formal analysis capabilities in this framework. The SAMTools developed for this framework in this dissertation integrates three tools: PIPE+ for HLPNs behavioral modeling and simulation, SAMAT for hierarchical structural modeling and property specification, and PIPE+Verifier for behavioral verification.

Formal verification and testing of software architectural models

Ensuring the correctness of software has been the major motivation in software research, constituting a Grand Challenge. Due to its impact in the final implementation, one critical aspect of software is its architectural design. By guaranteeing a correct architectural design, major and costly flaws can be caught early on in the development cycle. Software architecture design has received a lot of attention in the past years, with several methods, techniques and tools developed. However, there is still more to be done, such as providing adequate formal analysis of software architectures. On these regards, a framework to ensure system dependability from design to implementation has been developed at FIU (Florida International University). This framework is based on SAM (Software Architecture Model), an ADL (Architecture Description Language), that allows hierarchical compositions of components and connectors, defines an architectural modeling language for the behavior of components and connectors, and provides a specification language for the behavioral properties. The behavioral model of a SAM model is expressed in the form of Petri nets and the properties in first order linear temporal logic.^ This dissertation presents a formal verification and testing approach to guarantee the correctness of Software Architectures. The Software Architectures studied are expressed in SAM. For the formal verification approach, the technique applied was model checking and the model checker of choice was Spin. As part of the approach, a SAM model is formally translated to a model in the input language of Spin and verified for its correctness with respect to temporal properties. In terms of testing, a testing approach for SAM architectures was defined which includes the evaluation of test cases based on Petri net testing theory to be used in the testing process at the design level. Additionally, the information at the design level is used to derive test cases for the implementation level. Finally, a modeling and analysis tool (SAM tool) was implemented to help support the design and analysis of SAM models. The results show the applicability of the approach to testing and verification of SAM models with the aid of the SAM tool.^

Characterization, sources, and transformations of dissolved organic matter (DOM) in Florida coastal Everglades (FCE)

Dissolved organic matter (DOM) is one of the largest carbon reservoirs on this planet and is present in aquatic environments as a highly complex mixture of organic compounds. The Florida coastal Everglades (FCE) is one of the largest wetlands in the world. DOM in this system is an important biogeochemical component as most of the nitrogen (N) and phosphorous (P) are in organic forms. Achieving a better understanding of DOM dynamics in large coastal wetlands is critical, and a particularly important issue in the context of Everglades restoration. In this work, the environmental dynamics of surface water DOM on spatial and temporal scales was investigated. In addition, photo- and bio-reactivity of this DOM was determined, surface-to-groundwater exchange of DOM was investigated, and the size distribution of freshwater DOM in Everglades was assessed. The data show that DOM dynamics in this ecosystem are controlled by both hydrological and ecological drivers and are clearly different on spatial scales and variable seasonally. The DOM reactivity data, modeled with a multi-pool first order degradation kinetics model, found that fluorescent DOM in FCE is generally photo-reactive and bio-refractory. Yet the sequential degradation proved a “priming effect” of sunlight on the bacterial uptake and reworking of this subtropical wetland DOM. Interestingly, specific PARAFAC components were found to have different photo- and bio-degradation rates, suggesting a highly heterogeneous nature of fluorophores associated with the DOM. Surface-to-groundwater exchange of DOM was observed in different regions of the system, and compositional differences were associated with source and photo-reactivity. Lastly, the high degree of heterogeneity of DOM associated fluorophores suggested based on the degradation studies was confirmed through the EEM-PARAFAC analysis of DOM along a molecular size continuum, suggesting that the fluorescence characteristics of DOM are highly controlled by different size fractions and as such can exhibit significant differences in reactivity.

Formal verification and testing of software architectural models

Ensuring the correctness of software has been the major motivation in software research, constituting a Grand Challenge. Due to its impact in the final implementation, one critical aspect of software is its architectural design. By guaranteeing a correct architectural design, major and costly flaws can be caught early on in the development cycle. Software architecture design has received a lot of attention in the past years, with several methods, techniques and tools developed. However, there is still more to be done, such as providing adequate formal analysis of software architectures. On these regards, a framework to ensure system dependability from design to implementation has been developed at FIU (Florida International University). This framework is based on SAM (Software Architecture Model), an ADL (Architecture Description Language), that allows hierarchical compositions of components and connectors, defines an architectural modeling language for the behavior of components and connectors, and provides a specification language for the behavioral properties. The behavioral model of a SAM model is expressed in the form of Petri nets and the properties in first order linear temporal logic. This dissertation presents a formal verification and testing approach to guarantee the correctness of Software Architectures. The Software Architectures studied are expressed in SAM. For the formal verification approach, the technique applied was model checking and the model checker of choice was Spin. As part of the approach, a SAM model is formally translated to a model in the input language of Spin and verified for its correctness with respect to temporal properties. In terms of testing, a testing approach for SAM architectures was defined which includes the evaluation of test cases based on Petri net testing theory to be used in the testing process at the design level. Additionally, the information at the design level is used to derive test cases for the implementation level. Finally, a modeling and analysis tool (SAM tool) was implemented to help support the design and analysis of SAM models. The results show the applicability of the approach to testing and verification of SAM models with the aid of the SAM tool.