This project pursues issues on the border of information technologies and process optimization. Previously published concepts of~modeling projects and shared resources with object-oriented Petri nets are presented and further expanded. The possibilites of~the use of~genetic algorithms for dynamic realtime optimization of the resource schedules are explored. The resource constrained project sheduling problem is presented and it is shown, how instances of the problem can be implemented. A more complex model that is inspired by real production systems is then created. Next, a control agent, which monitors a running production system and allows for it's dynamic optimization is designed. The whole system is implemented in the Squeak Smalltalk environment with the use of the tool PNtalk, which is an experimental implementation of the object oriented Petri nets paradigm.

Cette thèse porte sur le diagnostic des défauts dans des Systèmes à Evènements Discrets (SED) pour lesquels l’occurrence des événements est soumise à des contraintes temporelles. Les domaines d’application potentiels sont nombreux et variés allant de la production manufacturière aux systèmes de transport en passant par les réseaux de communication et les systèmes d’information. La complexité croissante de ces systèmes nécessite l’élaboration de méthodes de surveillance de plus en plus efficaces et performantes pour garantir leur sécurité, leur disponibilité ainsi que le maintien de leurs propriétés dans le temps. Les réseaux de Petri Stochastiques Temporisés Partiellement Observés (RdPSTPO) sont utilisés pour modéliser le système ainsi que les défauts qui peuvent l’affecter. L’étude concerne particulièrement les défauts qui se traduisent par la violation des contraintes temporelles. Une exploitation pertinente des informations temporelles, en vue du diagnostic, constitue la contribution majeure de la thèse. En effet, une meilleure utilisation de ces informations permet de discerner avec précision les différents comportements qui expliquent les mesures. De plus, la probabilité d’occurrence des défauts est calculée en fonction des dates des mesures collectées. Deux approches sont développées : la première est dédiée aux défauts ponctuels et la seconde aux dérives lentes dans les systèmes cycliques. / This PhD thesis deals with the fault diagnosis of Discrete Event Systems (DES) for which the occurrence of events is constrained by temporal specifications. The domain of application is large and varied ranging from manufacturing systems to transportation systems, communication networks and information systems. The increasing complexity of these systems requires the development of effective and efficient monitoring methods to ensure their security, availability and the maintenance of their properties over the time. For that purpose, Partially Observed Stochastic Timed Petri Nets (POSTPN) are used to model the system and the different faults that may affect it. The study is particularly concerned with faults that result after the violation of temporal constraints. Our main contribution in this thesis is the relevant exploitation of the timed information for the fault diagnosis. In fact, a better use of these temporal informations allow to discern with precision the different behaviors that are consistent with the measurements. In addition, the probability of faults occurrence is evaluated according to the dates of collected measurements. Two approaches are developed : the first one is used for single faults and the second one for slow drifts in cyclical systems.

The brain extracellular space (ECS) contains specified macromolecules forming the extracellular matrix (ECM), containing a high amount of negative charges that could bind water or other soluble ions and molecules diffusing within the ECS. In specific brain areas, the ECM molecules form a condensed, reticular-like structure of perineuronal nets (PNNs). It has been found that PNNs appear at the end of the critical period, when they stabilize the synapses and terminate their plasticity and may have also neuroprotective function. To study the role of brain link protein 2 (Bral2) in stabilizing the ECM complexes, we employed the real-time iontophoretic method and immunohistochemical analysis to show the difference in the ECS diffusion parameters and level of expression of the ECM molecules between the wild type and Bral2-deficient mice. We also compared changes in the ECS diffusion parameters induced by Bral2 deficiency with those appeared after enzymatic destruction of the ECM by the chondroitinase ABC (chABC). In the Bral2-deficient mice, we discovered significantly decreased values of tortuosity in the trapezoid body. This difference was age related and did not manifest itself in young mice. Immunohistochemical analysis showed that inferior colliculus does not contain Bral2-brevican based...

Tauopathy is accompanied by both loss of neurons and synapses. The neuronal loss is irreversible with very low chance of functional replacement therapy. However, lost synapses could be restored with proper stimuli. Perineuronal nets (PNNs) are serving as a protecting barrier for neurons, on the other hand they are significantly decreasing the synaptic plasticity. Temporary disintegration of the PNNs by enzymatic therapy might lead to rewiring and accelerate processes of memory and learning. Model of Cold Induced plasticity leads to the withdrawal of significant number of synapses across the brain. The recovery of these could be followed in healthy and diseased animals. Moreover, it can stimulate Cold shock protein dependent neuroprotective mechanisms. This master thesis is focused on these two forms of synaptic plasticity models; forced remodeling of PNNs and model of cold induced synaptic plasticity. Both will serve as a tool to modulate processes of memory and learning in the P301S tauopathy, in mice. In detail, the work will follow changes in the number of synapses at the region of CA1 of hippocampus and synaptic protein levels at level of whole hippocampus and behavioral recovery of pre-trained long-term memory task dependent on dorsal hippocampus. Key words: Perineuronal nets, aggrecan,...

Since the ability of Workforce Management Systems to handle mobility induced challenges of mobile environments like data-communication cut-offs, reduced network bandwidth, and security concerns improved recently, the optimization efforts of mobile enterprises increasingly focus on the organizational setup of their mobile environment. This includes issues like, e.g., the dimension and staffing of regional subdivisions, qualification balance of the workforce, and resource allocation strategies. While this multitude of possible adjustment parameters for optimization prevents from the analytical prediction of organizational change efforts, simulation is a promising approach to analyze mobile environments and their change. In this work we present a formal model representing a generalization of mobile environments. This model can be utilized to examine the cost situation and performance of both real mobile enterprises and projected future development scenarios of such enterprises. The model is developed using colored petri nets (CPN) and the software suite CPN Tools. We show that our model is capable of predicting the outcomes of organizational change projects by the utilization of simulation and present a validation of our model based on real-world data of a German gas and power supply.

This paper presents a class of Stochastic Petri Nets with concurrent transition firings. It is assumed that transitions occur in steps and that for every step each enabled transition decides probabilistically whether it wants to participate in the step or not. Among the transitions which what to participate in a step, a maximal number is chosen to perform the firing step. The observable behavior is defined and equivalence relations are introduced. The equivalence relations extend the well-known trace and bisimulation equivalences for systems with step semantics to Stochastik Petri Nets with concurrent transition firing. It is shown that the equivalence notions form a lattice of interrelations.

To meet ambitious climate goals, of keeping global warming below 2°C, past emissions need to be removed from the atmosphere with the help of negative emissions technologies (NETs). The transition of energy systems, however, needs to follow the requirements of sustainable development to benefit all three pillars of sustainability, those are the environment, society, and economy. A NET that has gained increased attention from policymakers and businesses in recent years is direct air capture (DAC). The technology is currently on a small scale and faces challenges for scale-up such as energy and water intensity, the unclear requirements of resources and uncertain environmental, social, and economic impacts. The aim of this study was, therefore, to address DAC's impact on the three pillars of sustainability to answer the research question: How does direct air capture influence or connect to the three pillars of sustainable development? Because of the lack of research on DAC in connection with sustainability a qualitative interview approach was chosen where five interviews were conducted with researchers working with DAC. The findings derived from the interviews were separated into the different pillars of sustainability. The finding for the sustainability aspect included the definition of sustainability, various justice aspects and contributions to the SDGs. For the environmental aspect, DAC's carbon footprint and impact on mitigation were highlighted. The economic aspect of DAC showed the need for a clear business model and a supportive carbon mechanism. Lastly, for the social aspect low level of knowledge and the importance of social acceptance were recognized. Concluding, these different aspects influence the pillars of sustainability and need to be considered before further scale-up of DAC.

La technologie de workflow, tendant à automatiser les processus d'entreprise et à fournir un support pour leur gestion, est aujourd'hui un secteur actif de recherche. C'est dans ce contexte que se situent ces travaux de thèse qui portent aussi bien sur la modélisation des processus workflow que sur leur vérification. Ces processus, pouvant être contraints par des ressources partagées ou encore par des durées de traitement, doivent être vérifiés avant d'être confiés aux systèmes de gestion de workflow qui vont les exécuter. Nous nous sommes intéressés par la vérification de la propriété de cohérence (soundness) des réseaux de workflow (WF-net) : sous-classes des réseaux de Petri (RdPs) modélisant les processus workflow.Dans ce cadre, en explorant la théorie structurelle des RdPs, nous avons identifié des sous-classes de WF-nets pour lesquelles la cohérence peut être vérifiée et caractérisée efficacement. Nous nous sommes focalisés en outre sur l'extension de ces sous-classes en tenant compte de la présence de ressources partagées et sur la propriété de cohérence en présence d'un nombre arbitraire d'instances prêtes à s'exécuter. Dans cette partie, nous avons dû automatiser le calcul des siphons minimaux dans un RdP. Pour ce faire, nous avons choisi un algorithme de la littérature et l'amélioré par la recherche et la contraction de circuits alternés.Ensuite, nous avons abordé la modélisation et la vérification de processus workflow tenant compte des contraintes temporelles. Nous avons en premier lieu proposé un modèle de TWF-net (WF-net Temporisé). Pour ce modèle, nous avons défini la propriété de cohérence temporelle et proposé une condition nécessaire et suffisante pour la vérifier. En deuxième lieu, nous avons relaxé les contraintes temporelles adoptées par la proposition d'un modèle temporel visant des processus à contraintes temporelles variant dans des intervalles de temps. Nous avons défini formellement le modèle de ITWF-net (Interval Timed WF-net) et donné sa sémantique. Par ailleurs, nous avons développé et testé un prototype de modélisation et de simulation des ITWF-nets.La dernière partie de cette thèse a concerné la vérification formelle des processus workflow par SPIN model checker. Nous avons dû en premier lieu traduire la spécification des workflows adoptée vers Promela : le langage de description des modèles à vérifier par SPIN. En second lieu, nous avons exprimé les propriétés de cohérence en Logique Linéaire Temporelle (LTL) et utilisé SPIN pour tester si chaque propriété est satisfaite par le modèle Promela du WF-net en question. Enfin, nous avons exprimé les propriétés de k-cohérence pour les WF-nets modélisant plusieurs instances et de (k,R)-cohérence pour les processus workflow concurrents et qui possèdent des ressources partagées. / Workflow technology, whose role is to automate business processes and to provide a support for their management, is today an active sector of research. This thesis deals with the modelling of the workflow processes and their analysis. These processes, probably constrained by shared resources or by durations of treatment, must be checked before being executed by their workflow management systems. In this direction, we were interested by the checking of the soundness property of workflow nets (WF-nets): subclasses of Petri nets modelling the workflow processes.To begin with, by exploring the structure theory of Petri nets, we have identified subclasses of WF-nets for which soundness can be checked and characterized effectively. We also extended these subclasses by taking account of the presence of shared resources and we focused on the soundness property in the presence of an arbitrary number of instances ready to be carried out. In this part, we had to automate the computation of minimal siphons in a Petri net. For that, we chose an algorithm of the literature and improved it by the research and the contraction of alternate circuits.Then, we were concerned by the modelling and the analysis of workflow processes holding temporal constraints. We initially proposed the model of TWF-net (Timed WF-net). For this model, we defined its soundness and proposed a method to check it. Then, we released the adopted temporal constraints by the proposal of a model covering workflow processes for witch temporal constraints vary in time intervals. We formally defined the model of ITWF-net (Interval Timed WF-net) and gave its semantics. In addition, we developed and tested a prototype of modelling and simulation of ITWF-nets.The last part of this thesis concerns the formal analysis of workflow processes with SPIN model checker. We initially translated the workflow specification into Promela: the model description language used by SPIN. Then, we expressed the soundness properties in Linear Temporal Logic (LTL) and used SPIN to test if each property is satisfied by the Promela model of a given WF-net. Moreover, we expressed the properties of k-soundness for WF-nets modelling several instances and (k,R)-soundness for competitive workflow processes which share resources.

Notre thèse est consacrée à l’étude de la supervision des réseaux de Petri en vue de la conception de systèmes manufacturiers flexibles. L’objectif est la définition de stratégies de pilotage en ligne pour l’évitement de conflits et d’interblocages, dans le cadre de la théorie de la supervision. Le point de départ de notre travail est d’exploiterle graphe de marquage du réseau de Petri, ce qui permet en particulier d’obtenir des stratégies de commande maximalement permissive pour des problèmes d’évitement de conflits et d’interblocages. Nous avons ainsi introduit des techniques originales, manipulations d’inégalités ou réductions d’ensembles de marquages, destinées à diminuerla complexité algorithmique d’une telle méthode. Dans premier temps, nous avons focalisé sur la synthèse de superviseurs dits purs, ce qui correspond au cas particulier où l’ensemble de marquage légaux, est convexe.Cette optimisation est ensuite considérée du point de vue de la facilité de mise en oeuvre. Nous traitons ainsi de la minimisation de la structure du superviseur et de son coût d’implémentation en préservant une structure de supervision qui offre à la fois la permissivité maximale et une complexité de calcul raisonnable en vue d’utilisationsur des installations réelles. Aussi, nous avons cherché à réduire le nombre de places de contrôle nécessaires pour réaliser un superviseur maximalement permissif, pour cela nous avons formule le calcul du nombre minimal de places de contrôle en termes d’un problème de programmation linéaire. Afin d’affaiblir la complexité de ce calcul de superviseur, deux versions de l’algorithme sont proposées. Ce problème de minimisation de la taille dusuperviseur, quoique fondamental, n’est pas abordé aussi directement dans la littérature. Il s’agit là d’une première contribution.Dans u second temps, nous nous sommes intéressés aux réseaux de Petri à boucles (self-loops). Les boucles étant représentées par une variable qui s’ajoute dans la contrainte inégalité définissant l’ensemble de marquages légaux. Après avoir proposé une méthode de réduction du nombre d’inégalités ainsi que du superviseur optimalen se basant sur les approches et résultats précédents, nous avons établi une condition suffisante d’obtention d’un superviseur maximalement permissif permettant de traiter des ensembles de marquages légaux non convexes.Enfin nous proposons une méthode de synthèse de contrôleur pour une nouvelle classe de réseaux de Petri, avec des arcs inhibiteurs correspondant à des contraintes définies par des intervalles. La taille du contrôleur ainsi obtenu et défini en termes d’arcs inhibiteurs à intervalles s’en trouve réduite ainsi que par conséquent sont coût d’implémentation. / Reachability graph analysis is an important technique for deadlockcontrol, which always suffers from a state explosion problem since it requires togenerate all or a part of reachable markings.Based on this technique, an optimal or suboptimal supervisor with high behavioralpermissiveness can always be achieved. This thesis focuses on designing liveness enforcing Petri net supervisors for FMSs by considering their behavioralpermissiveness, supervisory structure, and computationnal complexity.The following research contributions are made in this thesis.1. The design of a maximally permissive liveness-enforcing supervisor for an FMSis proposed by solving integer linear programming problems (ILPPs).2. Structural complexity is also an important issue for a maximally permissivePetri net supervisor. A deadlock prevention policy for FMSs is proposed, which canobtain a maximally permissive liveness-enforcing Petri net supervisor while thenumber of control places is compressed.3. In order to overcome the computational complexity problem in MCPP and ensurethat the controlled system is maximally permissive with a simple structure, wedevelop an iterative deadlock prevention policy and a modified version.4. We consider the hardware and software costs in the stage of controlimplementation of a deadlock prevention policy, aiming to obtain a maximallypermissive Petri net supervisor with the lowest implementation cost. A supervisorconsists of a set of control places and the arcs connecting control places totransitions. We assign an implementation cost for each control place and controland observation costs for each transition. Based on reachability graph analysis,maximal permissiveness can be achieved by designing place invariants that prohibitall FBMs but no legal markings.5. Self-loops are used to design maximally permissive supervisors. A self-loop ina Petri net cannot be mathematically represented by its incidence matrix. Wepresent a mathematical method to design a maximally permissive Petri netsupervisor that is expressed by a set of control places with self-loops. A controlplace with a self-loop can be represented by a constraint and a selfloopassociated with a transition whose firing may lead to an illegal marking.

Weathering of silicate minerals has long been a known source of natural CO2 sequestration, that could be increased in the presence of microorganisms. Bio-enhanced weathering of silicate minerals could increase the sequestration of CO2 from the atmosphere.   The aim of this project was to evaluate the potential for a new Neutral emission technology (NET), using four different organisms, Aspergillus Niger, Knufia Petricola, Bacillus Subtilis and Cupriavidus Metallidurans and their potential to increase olivine weathering (dunite). Straw, manure and digestate was used as carbon sources. In total 9 biotic - and 9 abioitc reactors were made, containing a mixture of dunite and one of the three carbon sources. In total 250 mL of water was added to each reactor per week, for 6 weeks, and collected at the end of the week for analysis. Geochemical analyses of the leachate were performed, including pH, conductivity, alkalinity, total organic carbon (TOC), total inorganic carbon (TIC), cations, anions and three organic acids: citrate, acetate, and oxalate. Scanning emission microscope (SEM) was used to monitor potential differences pre- and post-treatment.   Straw reactors produced the most growth, both on the carbon source and the dunite grains. Likely due to the increased labile organic carbon concentrations. The total inorganic carbon and alkalinity demonstrated that inoculation of the reactors promoted weathering for all carbon sources, most significantly for the straw reactors. This observation was evidenced by etch pits in the SEM images and higher TIC, alkalinity, and magnesium values. Microbially enhanced silicate weathering has demonstrated it could be used for the development of NETs for the sequestration of atmospheric carbon. / BAM!