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.

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.

Class Size Reduction for the State of Florida: Is This the Solution for a Better Education?

Smaller class sizes have a positive impact on student achievement but Florida struggles with the problem of how to achieve smaller classes. Through a review of the literature, this paper discusses some of the programs currently used across the US, with the focus on Florida. Conclusions and implications are presented.

Cognitive competence and life course change in multi-problem adolescents

The dissertation reports on two studies. The purpose of Study I was to develop and evaluate a measure of cognitive competence (the Critical Problem Solving Skills Scale – Qualitative Extension) using Relational Data Analysis (RDA) with a multi-ethnic, adolescent sample. My study builds on previous work that has been conducted to provide evidence for the reliability and validity of the RDA framework in evaluating youth development programs (Kurtines et al., 2008). Inter-coder percent agreement among the TOC and TCC coders for each of the category levels was moderate to high, with a range of .76 to .94. The Fleiss' kappa across all category levels was from substantial agreement to almost perfect agreement, with a range of .72 to .91. The correlation between the TOC and the TCC demonstrated medium to high correlation, with a range of r(40)=.68, p<.001 to r(40)=.79, p<.001. Study II reports an investigation of a positive youth development program using an Outcome Mediation Cascade (OMC) evaluation model, an integrated model for evaluating the empirical intersection between intervention and developmental processes. The Changing Lives Program (CLP) is a community supported positive youth development intervention implemented in a practice setting as a selective/indicated program for multi-ethnic, multi-problem at risk youth in urban alternative high schools in the Miami Dade County Public Schools (M-DCPS). The 259 participants for this study were drawn from the CLP's archival data file. The study used a structural equation modeling approach to construct and evaluate the hypothesized model. Findings indicated that the hypothesized model fit the data (χ2 (7) = 5.651, p = .83; RMSEA = .00; CFI = 1.00; WRMR = .319). My study built on previous research using the OMC evaluation model (Eichas, 2010), and the findings are consistent with the hypothesis that in addition to having effects on targeted positive outcomes, PYD interventions are likely to have progressive cascading effects on untargeted problem outcomes that operate through effects on positive outcomes.

Cognitive Competence and Life Course Change in Multi-Problem Adolescents

The dissertation reports on two studies. The purpose of Study I was to develop and evaluate a measure of cognitive competence (the Critical Problem Solving Skills Scale – Qualitative Extension) using Relational Data Analysis (RDA) with a multi-ethnic, adolescent sample. My study builds on previous work that has been conducted to provide evidence for the reliability and validity of the RDA framework in evaluating youth development programs (Kurtines et al., 2008). Inter-coder percent agreement among the TOC and TCC coders for each of the category levels was moderate to high, with a range of .76 to .94. The Fleiss’ kappa across all category levels was from substantial agreement to almost perfect agreement, with a range of .72 to .91. The correlation between the TOC and the TCC demonstrated medium to high correlation, with a range of r(40)=.68, p Study II reports an investigation of a positive youth development program using an Outcome Mediation Cascade (OMC) evaluation model, an integrated model for evaluating the empirical intersection between intervention and developmental processes. The Changing Lives Program (CLP) is a community supported positive youth development intervention implemented in a practice setting as a selective/indicated program for multi-ethnic, multi-problem at risk youth in urban alternative high schools in the Miami Dade County Public Schools (M-DCPS). The 259 participants for this study were drawn from the CLP’s archival data file. The study used a structural equation modeling approach to construct and evaluate the hypothesized model. Findings indicated that the hypothesized model fit the data (χ2 (7) = 5.651, p = .83; RMSEA = .00; CFI = 1.00; WRMR = .319). My study built on previous research using the OMC evaluation model (Eichas, 2010), and the findings are consistent with the hypothesis that in addition to having effects on targeted positive outcomes, PYD interventions are likely to have progressive cascading effects on untargeted problem outcomes that operate through effects on positive outcomes.