Syftet med studien är att bidra med kunskap om rektors och skolans besluts-processer och hur dessa kan förstås ur ett organisationsteoretiskt perspektiv. Fallstudien har använts som forskningsmetod och en F-9 skola ingår i studien. Det empiriska materialet består av mötesobservationer, intervjuer och doku-mentanalys. Den teoretiska utgångspunkten för studien är organisationsteori med särskilt fokus på beslutsteori. Två modeller används som analysverktyg: faser i beslutsprocessen och sammanfattning av beslutsmodeller. Rektors roll i beslutsprocesserna är också en viktig faktor i analysen.En fråga i uppsatsen fokuserar på hur beslutsprocesserna går till på den stude-rade skolan och vad är rektors roll i dessa är. Resultatet visar här att det mesta av informationen som samlas in av rektor inför beslutsfattande är verbal och få val mellan direkta alternativ görs. Beslut är ofta vaga och de beslut som fattas rör i hög utsträckning praktiska frågor. Mycket lite av verkställande och upp-följning av beslut har setts i studien.Den andra fråga som ställs i uppsatsen är hur beslutsprocesserna kan beskrivas och förstås utifrån organisationsteoretiska och beslutsteoretiska begrepp och modeller. Resultatet pekar på att det är den inkrementella beslutsmodell som bäst stämmer in på den studerade skolans beslutsprocesser, med detta sagt är en modell aldrig en direkt avspegling av verkligheten utan inslag från fler mo-deller kan ses i studien. Då resultatet visar på vaga och otydliga beslutsproces-ser är slutsatsen att skolor skulle vinna på att tydliggöra processerna för alla inblandade, att börja tala om en designad beslutsprocess. / The purpose of this essay is to make a knowledge contribution regarding head teachers’ and schools’ decision processes and how these can be understood from an organizational theoretical perspective. A case study was carried out in a so called “F - 9” school (pre-school class and year 1 - 9 compulsory school). A triangulation of the methods observation, document analysis and interviews was used. The theoretical point of departure for the study is organisational the-ory with special focus on decision theory. Two models are used as analytical tools: phases in the decision process and a summary of the decision models used. The role of the head teacher is also an important factor in the analysis.One question in the essay focuses on how the decision processes are carried out and what the head teacher’s role in these are. The results show that most of the information gathered by the head teacher before the decisions is verbal and that few choices between alternatives are made. Decisions are often vague and the decisions made primarily concerns practical questions. Very little in terms of implementation and follow up of the decisions have been seen in the study.The second question asked in the essay is how the decision processes can be described and understood with organisation theoretical and decision theoretical terms and models. The result indicates that it is the incremental decision model that best describe the decision process of the participating school, however, no model is ever a direct reflection of reality and elements of more models can be seen in the study. As the results indicate vague and unclear decision processes, the conclusion is that schools would gain from clarifying the processes for all concerned, there is need to talk about a designed decision process.

Nous explorons l'étendue du champ applicatif des processus markoviens décisionnels au travers de deux problématiques. La première, de nature industrielle, propose l'étude numérique de l'optimisation d'un processus d'intégration lanceur en collaboration avec Airbus DS. Il s'agit d'un cas particulier des problèmes de gestion d'inventaire dans lequel un calendrier de tirs joue un rôle central. La modélisation adoptée entraîne l'impossibilité d'appliquer les procédures d'optimisation classiques liées au formalisme des processus markoviens décisionnels. Nous étudions alors des algorithmes basés sur des simulations qui rendent des stratégies optimales non triviales et qui sont utilisables dans la pratique. La deuxième problématique, de nature théorique, se concentre sur les questions d'arrêt optimal partiellement observables. Nous proposons une méthode d'approximation par quantification de ces problèmes lorsque les espaces d'états sont quelconques. Nous étudions la convergence de la valeur optimale approchée vers la valeur optimale réelle ainsi que sa vitesse. Nous appliquons notre méthode à un exemple numérique. / We investigate the potential of the Markov decision processes theory through two applications. The first part of this work is dedicated to the numerical study of an industriallauncher integration process in co-operation with Airbus DS. It is a particular case of inventory control problems where a launch calendar has a key role. The model we propose implies that standard optimization techniques cannot be used. We then investigate two simulation-based algorithms. They return non trivial optimal policies which can be applied in actual practice. The second part of this work deals with the study of partially observable optimal stopping problems. We propose an approximation method using optimal quantization for problems with general state space. We study the convergence of the approximated optimal value towards the real optimal value. The convergence rate is also under study. We apply our method to a numerical example.

No description available.

Au sein de la communauté scientifique, l’étude des réseaux d’énergie suscite un vif intérêt puisque ces infrastructures deviennent de plus en plus importantes dans notre monde moderne. Des outils mathématiques avancés et complexes sont nécessaires afin de bien concevoir et mettre en œuvre ces réseaux. La précision et l’optimalité sont deux caractéristiques essentielles pour leur conception. Bien que ces deux aspects soient au cœur des méthodes formelles, leur application effective reste largement inexplorée aux réseaux d’énergie. Cela motive fortement le travail développé dans cette thèse. Un accent particulier est placé sur le problème général de planification de la consommation d'énergie. Il s'agit d'un scénario dans lequel les consommateurs ont besoin d’une certaine quantité d’énergie et souhaitent que cette demande soit satisfaite dans une période spécifique (e.g., un Véhicule Électrique (VE) doit être rechargé dans une fenêtre de temps définie par son propriétaire). Par conséquent, chaque consommateur doit choisir une puissance de consommation à chaque instant (par un système informatisé), afin que l'énergie finale accumulée atteigne un niveau souhaité. La manière dont les puissances sont choisies est obtenue par l’application d’une « stratégie » qui prend en compte à chaque instant les informations pertinentes d'un consommateur afin de choisir un niveau de consommation approprié (e.g., l’énergie accumulée pour recharge le VE). Les stratégies peuvent être conçues selon une approche centralisée (dans laquelle il n'y a qu'un seul décideur qui contrôle toutes les stratégies des consommateurs) ou décentralisée (dans laquelle il y a plusieurs contrôleurs, chacun représentant un consommateur). Nous analysons ces deux scénarios dans cette thèse en utilisant des méthodes formelles, la théorie des jeux et l’optimisation. Plus précisément, nous modélisons le problème de planification de la consommation d'énergie à l'aide des processus de décision de Markov et des jeux stochastiques. Par exemple, l’environnement du système électrique, à savoir : la partie non contrôlable de la consommation totale (e.g., la consommation hors VEs), peut être représentée par un modèle stochastique. La partie contrôlable de la consommation totale peut s’adapter aux contraintes du réseau de distribution (e.g., pour ne pas dépasser la température maximale d'arrêt du transformateur électrique) et à leurs objectifs (e.g., tous les VEs soient rechargés). Cela peut être vu comme un système stochastique avec des multi-objectifs sous contraintes. Par conséquent, cette thèse concerne également une contribution aux modèles avec des objectives multicritères, ce qui permet de poursuivre plusieurs objectifs à la fois et une conception des stratégies qui sont fonctionnellement correctes et robustes aux changements de l'environnement. / Within the research community, there is a great interest in exploring many applications of energy grids since these become more and more important in our modern world. To properly design and implement these networks, advanced and complex mathematical tools are necessary. Two key features for their design are correctness and optimality. While these last two properties are in the core of formal methods, their effective application to energy networks remains largely unexploited. This constitutes one strong motivation for the work developed in this thesis. A special emphasis is made on the generic problem of scheduling power consumption. This is a scenario in which the consumers have a certain energy demand and want to have this demand fulfilled before a set deadline (e.g., an Electric Vehicle (EV) has to be recharged within a given time window set by the EV owner). Therefore, each consumer has to choose at each time the consumption power (by a computerized system) so that the final accumulated energy reaches a desired level. The way in which the power levels are chosen is according to a ``strategy’’ mapping at any time the relevant information of a consumer (e.g., the current accumulated energy for EV-charging) to a suitable power consumption level. The design of such strategies may be either centralized (in which there is a single decision-maker controlling all strategies of consumers), or decentralized (in which there are several decision-makers, each of them representing a consumer). We analyze both scenarios by exploiting ideas originating from formal methods, game theory and optimization. More specifically, the power consumption scheduling problem can be modelled using Markov decision processes and stochastic games. For instance, probabilities provide a way to model the environment of the electrical system, namely: the noncontrollable part of the total consumption (e.g., the non-EV consumption). The controllable consumption can be adapted to the constraints of the distribution network (e.g., to the maximum shutdown temperature of the electrical transformer), and to their objectives (e.g., all EVs are recharged). At first glance, this can be seen as a stochastic system with multi-constraints objectives. Therefore, the contributions of this thesis also concern the area of multi-criteria objective models, which allows one to pursue several objectives at a time such as having strategy designs functionally correct and robust against changes of the environment.

V tejto práci sa zoberáme problémom automatizovanej syntézy pravdepodobnostných programov: majme konečnú rodinu kandidátnych programov, v ktorej chceme efektívne identifikovať program spĺňajúci danú špecifikáciu. Aj riešenie tých najjednoduchších syntéznych problémov v praxi predstavuje NP-ťažký problém. Pokrok v tejto oblasti prináša nástroj Paynt, ktorý na riešenie tohto problému používa novú integrovanú metódu syntézy pravdepodobnostných programov. Aj keď sa tento prístup dokáže efektívne vysporiadať s exponenciálnym rastom rodín kandidátnych riešení, stále tu existuje problém spôsobený exponenciálnym rastom jednotlivých členov týchto rodín. S cieľom vysporiadať sa aj s týmto problémom, sme implementovali GPU orientované algoritmy slúžiace na overovanie kandidátnych programov (modelov), ktoré danú úlohu paralelizujú na stavovej úrovni pravdepodobnostých modelov. Celkové zrýchlenie doshiahnuté týmto prístupom za určitých podmienok potom prinieslo takmer teoretický limit možného zrýchlenia syntézneho procesu.

The level of indoor comfort can highly be influenced by window opening and closing behavior of the occupant in an office building. It will not only affect the comfort level but also affects the energy consumption, if not properly managed. This occupant behavior is not easy to predict and control in conventional way. Nowadays, to call a system smart it must learn user behavior, as it gives valuable information to the controlling system. To make an efficient way of controlling a window, we propose RL (Reinforcement Learning) in our thesis which should be able to learn user behavior and maintain optimal indoor climate. This model free nature of RL gives the flexibility in developing an intelligent control system in a simpler way, compared to that of the conventional techniques. Data in our thesis is taken from an office building in Beijing. There has been implementation of Value-based Reinforcement learning before for controlling the window, but here in this thesis we are applying policy-based RL (REINFORCE algorithm) and also compare our results with value-based (Q-learning) and there by getting a better idea, which suits better for the task that we have in our hand and also to explore how they behave. Based on our work it is found that policy based RL provides a great trade-off in maintaining optimal indoor temperature and learning occupant’s behavior, which is important for a system to be called smart.

Dans cette thèse, nous étudions le contrôle dynamique des systèmes de partage de ressources qui se posent dans divers domaines : réseaux de gestion des stocks, services de santé, réseaux de communication, etc. Nous visons à allouer efficacement les ressources disponibles entre des projets concurrents, selon certains critères de performance. Ce type de problème est de nature stochastique et peut être très complexe à résoudre. Nous nous concentrons donc sur le développement de méthodes heuristiques performantes. Dans la partie I, nous nous plaçons dans le cadre des Restless Bandit Problems, qui est une classe générale de problèmes d’optimisation dynamique stochastique. Relaxer la contrainte de trajectoire dans le problème d’optimisation permet de définir une politique d’index comme heuristique pour le modèle contraint d’origine, aussi appelée politique d’index de Whittle. Nous dérivons une expression analytique pour l’index de Whittle en fonction des probabilités stationnaires de l’état dans le cas où les bandits (ou projets) suivent un processus de naissance et de mort. D’une part, cette expression nécessite la vérification de plusieurs conditions techniques, d’autre part elle ne peut être calculée explicitement que dans certains cas spécifiques. Nous prouvons ensuite, que dans le cas particulier d’une file d’attente multi-classe avec abandon, la politique d’index de Whittle est asymptotiquement optimale aussi bien pour les régimes à faible trafic comme pour ceux à fort trafic. Dans la partie II, nous dérivons des heuristiques issues de l’approximation des systèmes stochastiques de partage de ressources par des modèles fluides déterministes. Nous formulons dans un premier temps une version fluide du problème d’optimisation relaxé que nous avons introduit dans la partie I, et développons une politique d’index fluide. L’index fluide peut toujours être calculé explicitement et surmonte donc les questions techniques qui se posent lors du calcul de l’index de Whittle. Nous appliquons les politiques d’index de Whittle et de l’index fluide à plusieurs cas : les fermes de serveurs éco-conscients, l’ordonnancement opportuniste dans les systèmes sans fil, et la gestion de stockage de produits périssables. Nous montrons numériquement que ces politiques d’index sont presque optimales. Dans un second temps, nous étudions l’ordonnancement optimal de la version fluide d’une file d’attente multi-classe avec abandon. Nous obtenons le contrôle optimal du modèle fluide en présence de deux classes de clients en concurrence pour une même ressource. En nous appuyant sur ces derniers résultats, nous proposons une heuristique pour le cas général de plusieurs classes. Cette heuristique montre une performance quasi-optimale lorsqu’elle est appliquée au modèle stochastique original pour des charges de travail élevées. Enfin, dans la partie III, nous étudions les phénomènes d’abandon dans le contexte d’un problème de distribution de contenu. Nous caractérisons une politique optimale de regroupement afin que des demandes issues d’utilisateurs impatients puissent être servies efficacement en mode diffusion. / In this thesis we study the dynamic control of resource-sharing systems that arise in various domains: e.g. inventory management, healthcare and communication networks. We aim at efficiently allocating the available resources among competing projects according to a certain performance criteria. These type of problems have a stochastic nature and may be very complex to solve. We therefore focus on developing well-performing heuristics. In Part I, we consider the framework of Restless Bandit Problems, which is a general class of dynamic stochastic optimization problems. Relaxing the sample-path constraint in the optimization problem enables to define an index-based heuristic for the original constrained model, the so-called Whittle index policy. We derive a closed-form expression for the Whittle index as a function of the steady-state probabilities for the case in which bandits (projects) evolve in a birth-and-death fashion. This expression requires several technical conditions to be verified, and in addition, it can only be computed explicitly in specific cases. In the particular case of a multi-class abandonment queue, we further prove that the Whittle index policy is asymptotically optimal in the light-traffic and heavy-traffic regimes. In Part II, we derive heuristics by approximating the stochastic resource-sharing systems with deterministic fluid models. We first formulate a fluid version of the relaxed optimization problem introduced in Part I, and we develop a fluid index policy. The fluid index can always be computed explicitly and hence overcomes the technical issues that arise when calculating the Whittle index. We apply the Whittle index and the fluid index policies to several systems: e.g. power-aware server-farms, opportunistic scheduling in wireless systems, and make-to-stock problems with perishable items. We show numerically that both index policies are nearly optimal. Secondly, we study the optimal scheduling control for the fluid version of a multi-class abandonment queue. We derive the fluid optimal control when there are two classes of customers competing for a single resource. Based on the insights provided by this result we build a heuristic for the general multi-class setting. This heuristic shows near-optimal performance when applied to the original stochastic model for high workloads. In Part III, we further investigate the abandonment phenomena in the context of a content delivery problem. We characterize an optimal grouping policy so that requests, which are impatient, are efficiently transmitted in a multi-cast mode.

This thesis develops a new abstraction for solving problems in decision automation. Decision automation is the process of creating algorithms which use data to make decisions without the need for human intervention. In this abstraction, four key ideas/problems are highlighted which must be considered when solving any decision problem. These four problems are the decision problem, the learning problem, the model reduction problem, and the verification problem. One of the benefits of this abstraction is that a wide range of decision problems from many different areas can be broken down into these four “key” sub-problems. By focusing on these key sub-problems and the interactions between them, one can systematically arrive at a solution to the original problem. Three new learning platforms have been developed in the areas of portfolio optimization, business intelligence, and automated water management in order to demonstrate how this abstraction can be applied to three different types of problems. For the automated water management platform a full solution to the problem is developed using this abstraction. This yields an automated decision process which decides how much water to release from the Piute Reservoir into the Sevier River during an irrigation season. Another motivation for developing these learning platforms is that they can be used to introduce students of all disciplines to automated decision making.

I nästan 20 år har mega projektet med Nya Karolinska Solna pågått. Upphandlingen har blivit en av de största i Sveriges historia och fått stor medial uppmärksamhet, inte bara nationellt men även internationellt. Rapporten syftar på att analysera samtliga planerings- och beslutsprocesser för byggnationen av Nya Karolinska Solna för att sedan undersöka om det finns några kopplingar baserat på beslutsteorier och hur dessa kan ha påverkat det slutliga resultatet. En litteraturstudie och intervjustudie har genomförts under arbetets gång. Rapporten behandlar olika beslutsteorier som rationella beslutsteorin och narrativa beslutsteorin. Vidare presenteras hur komplexa beslutsprocesser har kopplingar till olika teorier. Under byggprojektets gång har en rad olika aktörer varit involverade och dessa presenteras under avsnittet aktörer. Byggherren för projektet har varit Stockholms Läns Landsting, entreprenören har varit projektbolaget Swedish Hospital Partners (SHP) med dess två underleverantörer, Skanska Healthcare AB (SHC) och Coor Service Management AB (Coor). NKS förvaltningen var en organisation som inrättades för att ha ett organ som arbetade med hela organisationen. Gällande beslut om all byggnation, upphandlingen och organiseringen av vården hade förvaltningen exekutiv makt. Vidare tar rapporten upp de lagrum som varit aktuella i beslutsprocesserna under avsnittet gällande rätt. De mest centrala lagarna har varit Plan- och bygglagen (2010:900), Miljöbalken (1998:808), Myndighetsförordning (2007:515) och Förvaltningslagen (2017:900). Därefter redovisas alla utredningar och planprocesser som skett i ett tidigt skede och vilka beslut som tagits. Rapporten beskriver den slutgiltiga byggnationen som fått stor kritik för brister i utformningen. Efter intervjuer med aktörer från Skanska, Solna stad och NKS ger rapporten läsaren en bättre inblick i de olika beslutsprocesserna. Avslutningsvis analyseras intervjuerna utifrån de narrativa-, rationella och komplexa beslutsteorierna av Kerstin-Sahlin Andersson. Av analyserna framgår hur konsulter utgetts för experter och visat sig vara ett praktexempel på hur förvaltningar kan användas för att formulera berättelsen och därmed kontrollera premisserna för en beslutsprocess. När förvaltningen senare avsattes, för att ersättas med ett team från KS, förändrades hela strukturen och därmed utgången. Att involvera kompetenta medarbetare i arbetet kring och utformningen av sjukhuset kom att leda till positiva utfall. Det styrker även belägget om att inhämtning bruksinformation är en av de viktigaste delarna inom beslutsteorin för ett projekt av den karaktär Nya Karolinska Solna bär. / For almost 20 years, the mega-project with Nya Karolinska Solna has been ongoing. The procurement has become one of the largest in Sweden's history and received a lot of attention in the media, not only nationally but also internationally. The report aims to analyze all planning and decision-making processes for the construction of Nya Karolinska Solna and then investigate whether there are any connections based on decision theories and how these may have influenced the final result. A literature study and interview study have been made during the course of the report. The report deals with different decision theories such as the rational decision theory and the narrative decision theory. Furthermore, it is presented how complex decision-making processes have connections to different theories. During the course of the construction project, a number of different actors have been involved and these are presented in the actor section. The client for the project has been Stockholm County Council, the contractor has been the project company Swedish Hospital Partners (SHP) with its two subcontractors, Skanska Healthcare AB (SHC) and Coor Service Management AB (Coor). The NKS administration was an organization that was formed to have a unit that worked with the entire organization. Regarding decisions about all construction, procurement and the organization of care, the administration had executive power. Furthermore, the report covers the areas of legislation that were relevant in the decision- making processes according to the section of the law. The most central laws have been the Planning and Building Law (2010:900), the Environmental Law (1998:808), the Authority Ordinance (2007:515) and the Administration Law (2017:900). Afterwards, all investigations and planning processes that took place at an early stage and what decisions were taken are reported. The report describes the final construction, which received much criticism for building flaws. After interviews with actors from Skanska, Solna city and NKS, the report gives the reader a better insight into the various decision-making processes. Finally, the interviews are analyzed based on Kerstin-Sahlin Andersson's narrative, rational and complex decision theories. The analyzes show how consultants were passed off as experts and proved to be a prime example of how administrations can be used to formulate the story and thereby control the premises for a decision-making process. When the administration was later removed, to be replaced by a team from KS, the entire structure changed and thus the outcome. Involving competent employees in the work around and designing the hospital led to positive results. It also confirms the evidence that gathering usage information is one of the most important parts of decision theory for a project of the nature of Nya Karolinska Solna.

The ability to provide succinct information about why a property does, or does not, hold in a given system is a key feature in the context of formal verification and model checking. It can be used both to explain the behavior of the system to a user of verification software, and as a tool to aid automated abstraction and synthesis procedures. Counterexample traces, which are executions of the system that do not satisfy the desired specification, are a classical example. Specifications of systems with probabilistic behavior usually require that an event happens with sufficiently high (or low) probability. In general, single executions of the system are not enough to demonstrate that such a specification holds. Rather, standard witnesses in this setting are sets of executions which in sum exceed the required probability bound. In this thesis we consider methods to certify and witness that probabilistic reachability constraints hold in Markov decision processes (MDPs) and probabilistic timed automata (PTA). Probabilistic reachability constraints are threshold conditions on the maximal or minimal probability of reaching a set of target-states in the system. The threshold condition may represent an upper or lower bound and be strict or non-strict. We show that the model-checking problem for each type of constraint can be formulated as a satisfiability problem of a system of linear inequalities. These inequalities correspond closely to the probabilistic transition matrix of the MDP. Solutions of the inequalities are called Farkas certificates for the corresponding property, as they can indeed be used to easily validate that the property holds. By themselves, Farkas certificates do not explain why the corresponding probabilistic reachability constraint holds in the considered MDP. To demonstrate that the maximal reachability probability in an MDP is above a certain threshold, a commonly used notion are witnessing subsystems. A subsystem is a witness if the MDP satisfies the lower bound on the optimal reachability probability even if all states not included in the subsystem are made rejecting trap states. Hence, a subsystem is a part of the MDP which by itself satisfies the lower-bounded threshold constraint on the optimal probability of reaching the target-states. We consider witnessing subsystems for lower bounds on both the maximal and minimal reachability probabilities, and show that Farkas certificates and witnessing subsystems are related. More precisely, the support (i.e., the indices with a non-zero entry) of a Farkas certificate induces the state-space of a witnessing subsystem for the corresponding property. Vice versa, given a witnessing subsystem one can compute a Farkas certificate whose support corresponds to the state-space of the witness. This insight yields novel algorithms and heuristics to compute small and minimal witnessing subsystems. To compute minimal witnesses, we propose mixed-integer linear programming formulations whose solutions are Farkas certificates with minimal support. We show that the corresponding decision problem is NP-complete even for acyclic Markov chains, which supports the use of integer programs to solve it. As this approach does not scale well to large instances, we introduce the quotient-sum heuristic, which is based on iteratively solving a sequence of linear programs. The solutions of these linear programs are also Farkas certificates. In an experimental evaluation we show that the quotient-sum heuristic is competitive with state-of-the-art methods. A large part of the algorithms proposed in this thesis are implemented in the tool SWITSS. We study the complexity of computing minimal witnessing subsystems for probabilistic systems that are similar to trees or paths. Formally, this is captured by the notions of tree width and path width. Our main result here is that the problem of computing minimal witnessing subsystems remains NP-complete even for Markov chains with bounded path width. The hardness proof identifies a new source of combinatorial hardness in the corresponding decision problem. Probabilistic timed automata generalize MDPs by including a set of clocks whose values determine which transitions are enabled. They are widely used to model and verify real-time systems. Due to the continuously-valued clocks, their underlying state-space is inherently uncountable. Hence, the methods that we describe for finite-state MDPs do not carry over directly to PTA. Furthermore, a good notion of witness for PTA should also take into account timing aspects. We define two kinds of subsystems for PTA, one for maximal and one for minimal reachability probabilities, respectively. As for MDPs, a subsystem of a PTA is called a witness for a lower-bounded constraint on the (maximal or minimal) reachability probability, if it itself satisfies this constraint. Then, we show that witnessing subsystems of PTA induce Farkas certificates in certain finite-state quotients of the PTA. Vice versa, Farkas certificates of such a quotient induce witnesses of the PTA. Again, the support of the Farkas certificates corresponds to the states included in the subsystem. These insights are used to describe algorithms for the computation of minimal witnessing subsystems for PTA, with respect to three different notions of size. One of them counts the number of locations in the subsystem, while the other two take into account the possible clock valuations in the subsystem.:1 Introduction 2 Preliminaries 3 Farkas certificates 4 New techniques for witnessing subsystems 5 Probabilistic systems with low tree width 6 Explications for probabilistic timed automata 7 Conclusion