Indiana University-Purdue University Indianapolis (IUPUI) / This thesis proposed an algorithm that can find optimized Petri nets from given observation sequences according to some rules of optimization. The basic idea of this algorithm is that although the length of the observation sequences can keep growing, we can think of the growing as periodic and algorithm deals with fixed observations at different time. And the algorithm developed has polynomial complexity. A segment of example code programed according to this algorithm has also been shown. Furthermore, we modify this algorithm and it can check whether a Petri net could fit the observation sequences after several steps. The modified algorithm could work in constant time. These algorithms could be used in optimization of the control systems and communication networks to simplify their structures.

Indiana University-Purdue University Indianapolis (IUPUI) / In automotive industry, driver assistance and active safety features are main areas of research. This thesis concentrates on designing one of the famous ADAS system feature called Adaptive cruise control. Feature development and analysis of various functionalities involved in the system control are done using Petri Nets. A background on the past and current ACC research is noted and taken as motivation. The idea is to implement the adaptive cruise control system in Petri net and analyze how to provide fault tolerance to the system. The system can be evaluated for various cases. The ACC technology implemented in di erent cars were compared and discussed. The interaction of the ACC module with other modules in the car is explained. The cruise system's algorithm in Petri net is used as the basis for developing Adaptive Cruise Control system's algorithm. The ACC system model is designed using Petri nets and various Petri net functionalities like place invariant, transition invariant and reachability tree of the model are analyzed. The results are veri ed using Matlab. Controllers are introduced for ideal cases and are implemented in Petri nets. Then the error cases are considered and fault tolerance techniques are carried out on the model to identify the fault places.

Tau mutations promote the formation of tau oligomers and filaments, which are neuropathological signs of several tau-associated dementias. Types of neurons in the CNS are spared of tau pathology and are surrounded by a specialized form of extracellular matrix; called perineuronal nets (PNs). Aggrecan, the major PN proteoglycans, is suggested to mediate PNs neuroprotective function by forming an external shield preventing the internalization of misfolded tau. We recently demonstrated a correlation between aggrecan amount and the expression and phosphorylation of tau in a TauP310L-acan mouse model, generated by crossbreeding heterozygous aggrecan mice with a significant reduction of aggrecan and homozygous TauP301L mice. Neurodegenerative processes have been associated with changes of PN structure and protein signature. In this study, we hypothesized that the structure and protein expression of PNs in this TauP310L-acan mouse is regulated by tau. Immunohistochemical and biochemical analyses demonstrate that protein levels of PN components differ between TauP301LHET-acanWT and TauP301LHET-acanHET mice, accompanied by changes in the expression of protein phosphatase 2 A. In addition, tau can modulate PN components such as brevican. Co-immunoprecipitation experiments revealed a physical connection between PN components and tau. These data demonstrate a complex, mutual interrelation of tau and the proteoglycans of the PN.

The ham mite, Tyrophagus putrescentiae (Schrank) (Sarcoptiformes: Acaridae) is the predominant pest of dry cured hams during aging in the processing facilities. Methyl bromide is currently the only known fumigant that is effective at controlling ham mite infestations in aging houses. However, methyl bromide is being phased out of all industries and will be depleted in the near future. The research objectives were to 1) evaluate dry cured hams that have been treated with previously developed food grade coatings for sensory differences, and 2) to develop and determine the efficacy of ham nets incorporated with food grade coatings on controlling mite infestations and sensory properties. Food grade coating combinations of 1) propylene glycol (PG), xanthan gum, and water or 2) PG, propylene glycol alginates, carrageenan and water were dipped and sprayed on whole hams in commercial facilities in the summers of 2014 and 2015 (composition patent pending). The lowest concentration of propylene glycol needed to control mites in laboratory studies was 15% with xanthan gum and 7.5% with propylene glycol alginate and carrageenan. Sensory difference from control tests with trained panelists indicated that there were slight to moderate differences detected in some of the treated hams in comparison to untreated control hams (P < 0.05) when hams were dipped with coatings. However, there were no differences (P > 0.05) detected between the treated hams and the control hams when hams were only sprayed rather than dipped with these coatings. Polyester/cotton blend or cotton nets were infused with various food grade coatings and evaluated on the bench top by inoculating 20 adult mites onto one inch ham cubes for their efficacy at controlling mite infestations. Live adults and mobile immature stages were counted after 14 d of incubation (23 ± 2 °C and 70 ± 5% RH). Mite infestation tests demonstrated that coatings and coating-treated nets were effective at controlling mite growth. Therefore, food grade coatings can be applied to dry cured hams and also can be infused into nets as a potential means to control mite growth in ham processing facilities.

Malaria is caused by Plasmodium parasites, which are transmitted via the bite of infected female anopheles mosquitoes. There were 217 million cases of malaria worldwide, and about 435,000 malaria related deaths in 2017. WHO Africa region accounted for 92% and 93% of malaria cases and deaths worldwide. According to The Gambia National Malaria Strategic Plan 2013-2020, malaria is a leading cause of morbidity and mortality. The aim of this study was to identify factors influencing attitude towards the use of mosquito nets in households in The Gambia using Demographic and Health Survey (DHS) data. The current study is a secondary data analysis with a, cross-sectional study design. The source of the data for this study is the DHS, which was conducted by the United States Agency for International Development (USAID) together with the Gambia Bureau of Statistics (GBOS) in 2013. The study sample is representative of The Gambian population. The sample size for the study was 5276 subjects. Statistical Analysis System (SAS 9.3) was used for data analysis. Descriptive statistics were generated for the factors been tested. These included area of residence, presence of electricity, indoor residual spraying, highest level of education and wealth index. The outcome variable measured was household use of mosquito nets (Yes/No). Logistic regression analysis was done to determine whether area of residence, wealth index, education level, presence of electricity and indoor residual spraying influence attitude towards use of mosquito nets in households. Stepwise binary logistic regression was used to determine the final model with the most significant predictors. Odds ratios and corresponding confidence intervals were reported. Most of the study participants were poor (46%). Those with no education made up 45.5% of the study population and 58% of dwellings had no indoor residual spraying done in the past year. 76.6% and 59.1% of respondents lived in households that had at least one mosquito net and no electricity supply, respectively. 50.6% of the respondents resided in rural areas. Logistic regression analysis showed that wealth index, indoor residual spraying and area of residence were significant factors (p<0.05) influencing attitude towards use of mosquito nets in households. Indoor residual spraying (OR=2.00; 95% C.I. 1.71-2.36), primary school education (OR=1.1; 95% C.I. 0.94-1.32), middle class wealth index (OR=1.32; 95% C.I. 1.05-1.67) and rural residence (OR=1.29; 95% C.I. 1.01-1.64) are all independent factors that increased likelihood of mosquito net usage in households. Identifying factors that influence the usage of mosquito nets in households, can be useful in developing target interventions to further reduce malaria morbidity and mortality in The Gambia. Knowledge from this study can be used to further strengthen the national malaria strategic plan. To further establish causality and increase strength of association between factors and outcome, a case control or cohort study design will be needed, since that is one of the limitations of a cross sectional study.

This study shows how the two investment strategies Net-nets and magic formula performs on the Swedish stock markets subgroups Small, Mid and Large Cap. Also, with the intention to see which of these two strategies suits the private investors on the Swedish stock market and see which gave the highest rate of return. The results after a 15-year long time period showed us that Magic Formula was the one to be preferred on the Swedish stock market much due to the incompatibility of Net-nets on the Swedish stock market. Mainly because of the small sample of compatibility companies that suited the Net-nets instructions. Magic Formula was therefore able to yield a higher rate of return on all the subgroups compared to Net-nets and gave us the conclusion that it performs best on the Mid Cap on the Swedish stock market.

Yes / Over the years, several approaches have been developed for the quantitative analysis of dynamic fault trees (DFTs). These approaches have strong theoretical and mathematical foundations; however, they appear to suffer from the state-space explosion and high computational requirements, compromising their efficacy. Modularisation techniques have been developed to address these issues by identifying and quantifying static and dynamic modules of the fault tree separately by using binary decision diagrams and Markov models. Although these approaches appear effective in reducing computational effort and avoiding state-space explosion, the reliance of the Markov chain on exponentially distributed data of system components can limit their widespread industrial applications. In this paper, we propose a hybrid modularisation scheme where independent sub-trees of a DFT are identified and quantified in a hierarchical order. A hybrid framework with the combination of algebraic solution, Petri Nets, and Monte Carlo simulation is used to increase the efficiency of the solution. The proposed approach uses the advantages of each existing approach in the right place (independent module). We have experimented the proposed approach on five independent hypothetical and industrial examples in which the experiments show the capabilities of the proposed approach facing repeated basic events and non-exponential failure distributions. The proposed approach could provide an approximate solution to DFTs without unacceptable loss of accuracy. Moreover, the use of modularised or hierarchical Petri nets makes this approach more generally applicable by allowing quantitative evaluation of DFTs with a wide range of failure rate distributions for basic events of the tree. / This work was supported in part by the Dependability Engineering Innovation for Cyber Physical Systems (CPS) (DEIS) H2020 Project under Grant 732242, and in part by the LIVEBIO: Light-weight Verification for Synthetic Biology Project under Grant EPSRC EP/R043787/1.

Yes / Dust storms are one of the natural phenomena, which have increased in frequency in recent years in North Africa, Australia and northern China. Satellite remote sensing is the common method for monitoring dust storms but its use for identifying dust storms over sandy ground is still limited as the two share similar characteristics. In this study, an artificial neural network (ANN) is used to detect dust storm using 46 sets of data acquired between 2001 and 2010 over North Africa by the Moderate Resolution Imaging Spectroradiometer (MODIS) instruments aboard the Terra and Aqua satellites. The ANN uses image data generated from Brightness Temperature Difference (BTD) between bands 23 and 31 and BTD between bands 31 and 32 with three bands 1, 3, and 4, to classify individual pixels on the basis of their multiple-band values. In comparison with the manually detection of dust storms, the ANN approach gave better result than the Thermal Infrared Integrated Dust Index approach for dust storms detection over the Sahara. The trained ANN using data from the Sahara desert gave an accuracy of 0.88 when tested on data from the Gobi desert and managed to detect 90 out of the 96 dust storm events captured worldwide by Terra and Aqua satellites in 2011 that were classified as dusty images on NASA Earth Observatory. / IEEE Geoscience and Remote Sensing Society

Embedded systems are used in a wide spectrum of applications ranging from home appliances and mobile devices to medical equipment and vehicle controllers. They are typically characterized by their real-time behavior and many of them must fulfill strict requirements on reliability and correctness. In this thesis, we concentrate on aspects related to modeling and formal verification of realtime embedded systems. First, we define a formal model of computation for real-time embedded systems based on Petri nets. Our model can capture important features of such systems and allows their representations at different levels of granularity. Our modeling formalism has a welldefined semantics so that it supports a precise representation of the system, the use of formal methods to verify its correctness, and the automation of different tasks along the design process. Second, we propose an approach to the problem of formal verification of real-time embedded systems represented in our modeling formalism. We make use of model checking to prove whether certain properties, expressed as temporal logic formulas, hold with respect to the system model. We introduce a systematic procedure to translate our model into timed automata so that it is possible to use available model checking ools. Various examples, including a realistic industrial case, demonstrate the feasibility of our approach on practical applications.

When system runs are modeled with interval orders, interval order structures are useful tools to model abstract concurrent histories, i.e. sets of equivalent system runs. For the general cases, Mazurkiewicz traces allow a representation of the entire partial order by a single sequence with independency relations, and Comtraces allow a representation of stratified order structures by single step sequences with appropriate simultaneity and serializability relations. Unfortunately, both of them are unable to clearly describe the abstract interval order semantics of inhibitor nets. The goal of the thesis is to provide a monoid based model called Interval Traces that would allow a single sequence of beginnings and endings to represent the entire stratified order structures as well as all equivalent interval order observations. And the thesis will also show how interval order structures can be modelled by interval traces and how interval traces can be used to describe interval order semantics. / Thesis / Doctor of Philosophy (PhD)