This dissertation focuses on topics related to the value of real-time information and/or to supply uncertainties due to uncertain lead-times and yields in supply chains. The first two of these topics address issues associated with freight transportation, while the remaining two topics are concerned with inventory replenishment. We first assess the value of dynamic tour determination for the traveling salesman problem (TSP). Given a network with traffic dynamics that can be modeled as a Markov chain, we present a policy determination procedure that optimally builds a tour dynamically. We then explore the potential for expected total travel cost reduction due to dynamic tour determination, relative to two a priori tour determination procedures. Second, we consider the situation where the decision to continue or abort transporting perishable freight from an origin to a destination can be made at intermediate locations, based on real-time freight status monitoring. We model the problem as a partially observed Markov decision process (POMDP) and develop an efficient procedure for determining an optimal policy. We determine structural characteristics of an optimal policy and upper and lower bounds on the optimal reward function. Third, we analyze a periodic review inventory control problem with lost sales and random yields and present conditions that guarantee the existence of an optimal policy having a so-called staircase structure. We make use of this structure to accelerate both value iteration and policy evaluation. Lastly, we examine a model of inventory replenishment where both lead time and supply qualities are uncertain. We model this problem as an MDP and show that the weighted sum of inventory in transit and inventory at the destination is a sufficient statistic, assuming that random shrinkage can occur from the origin to the supply system or destination, shrinkage is deterministic within the supply system and from the supply system to the destination, and no shrinkage occurs once goods reach the destination.

Decision-theoretic systems, such as Markov Decision Processes (MDPs), are used for sequential decision-making under uncertainty. MDPs provide a generic framework that can be applied in various domains to compute optimal policies. This thesis presents techniques that offer explanations of optimal policies for MDPs and then refine decision theoretic models (Bayesian networks and MDPs) based on feedback from experts. Explaining policies for sequential decision-making problems is difficult due to the presence of stochastic effects, multiple possibly competing objectives and long-range effects of actions. However, explanations are needed to assist experts in validating that the policy is correct and to help users in developing trust in the choices recommended by the policy. A set of domain-independent templates to justify a policy recommendation is presented along with a process to identify the minimum possible number of templates that need to be populated to completely justify the policy. The rejection of an explanation by a domain expert indicates a deficiency in the model which led to the generation of the rejected policy. Techniques to refine the model parameters such that the optimal policy calculated using the refined parameters would conform with the expert feedback are presented in this thesis. The expert feedback is translated into constraints on the model parameters that are used during refinement. These constraints are non-convex for both Bayesian networks and MDPs. For Bayesian networks, the refinement approach is based on Gibbs sampling and stochastic hill climbing, and it learns a model that obeys expert constraints. For MDPs, the parameter space is partitioned such that alternating linear optimization can be applied to learn model parameters that lead to a policy in accordance with expert feedback. In practice, the state space of MDPs can often be very large, which can be an issue for real-world problems. Factored MDPs are often used to deal with this issue. In Factored MDPs, state variables represent the state space and dynamic Bayesian networks model the transition functions. This helps to avoid the exponential growth in the state space associated with large and complex problems. The approaches for explanation and refinement presented in this thesis are also extended for the factored case to demonstrate their use in real-world applications. The domains of course advising to undergraduate students, assisted hand-washing for people with dementia and diagnostics for manufacturing are used to present empirical evaluations.

Ce travail contribue à la théorie de la décision possibiliste et plus précisément à la prise de décision séquentielle dans le cadre de la théorie des possibilités, à la fois au niveau théorique et pratique. Bien qu'attrayante pour sa capacité à résoudre les problèmes de décision qualitatifs, la théorie de la décision possibiliste souffre d'un inconvénient important : les critères d'utilité qualitatives possibilistes comparent les actions avec les opérateurs min et max, ce qui entraîne un effet de noyade. Pour surmonter ce manque de pouvoir décisionnel, plusieurs raffinements ont été proposés dans la littérature. Les raffinements lexicographiques sont particulièrement intéressants puisqu'ils permettent de bénéficier de l'arrière-plan de l'utilité espérée, tout en restant "qualitatifs". Cependant, ces raffinements ne sont définis que pour les problèmes de décision non séquentiels. Dans cette thèse, nous présentons des résultats sur l'extension des raffinements lexicographiques aux problèmes de décision séquentiels, en particulier aux Arbres de Décision et aux Processus Décisionnels de Markov possibilistes. Cela aboutit à des nouveaux algorithmes de planification plus "décisifs" que leurs contreparties possibilistes. Dans un premier temps, nous présentons des relations de préférence lexicographiques optimistes et pessimistes entre les politiques avec et sans utilités intermédiaires, qui raffinent respectivement les utilités possibilistes optimistes et pessimistes. Nous prouvons que les critères proposés satisfont le principe de l'efficacité de Pareto ainsi que la propriété de monotonie stricte. Cette dernière garantit la possibilité d'application d'un algorithme de programmation dynamique pour calculer des politiques optimales. Nous étudions tout d'abord l'optimisation lexicographique des politiques dans les Arbres de Décision possibilistes et les Processus Décisionnels de Markov à horizon fini. Nous fournissons des adaptations de l'algorithme de programmation dynamique qui calculent une politique optimale en temps polynomial. Ces algorithmes sont basés sur la comparaison lexicographique des matrices de trajectoires associées aux sous-politiques. Ce travail algorithmique est complété par une étude expérimentale qui montre la faisabilité et l'intérêt de l'approche proposée. Ensuite, nous prouvons que les critères lexicographiques bénéficient toujours d'une fondation en termes d'utilité espérée, et qu'ils peuvent être capturés par des utilités espérées infinitésimales. La dernière partie de notre travail est consacrée à l'optimisation des politiques dans les Processus Décisionnels de Markov (éventuellement infinis) stationnaires. Nous proposons un algorithme d'itération de la valeur pour le calcul des politiques optimales lexicographiques. De plus, nous étendons ces résultats au cas de l'horizon infini. La taille des matrices augmentant exponentiellement (ce qui est particulièrement problématique dans le cas de l'horizon infini), nous proposons un algorithme d'approximation qui se limite à la partie la plus intéressante de chaque matrice de trajectoires, à savoir les premières lignes et colonnes. Enfin, nous rapportons des résultats expérimentaux qui prouvent l'efficacité des algorithmes basés sur la troncation des matrices. / This work contributes to possibilistic decision theory and more specifically to sequential decision-making under possibilistic uncertainty, at both the theoretical and practical levels. Even though appealing for its ability to handle qualitative decision problems, possibilisitic decision theory suffers from an important drawback: qualitative possibilistic utility criteria compare acts through min and max operators, which leads to a drowning effect. To overcome this lack of decision power, several refinements have been proposed in the literature. Lexicographic refinements are particularly appealing since they allow to benefit from the expected utility background, while remaining "qualitative". However, these refinements are defined for the non-sequential decision problems only. In this thesis, we present results on the extension of the lexicographic preference relations to sequential decision problems, in particular, to possibilistic Decision trees and Markov Decision Processes. This leads to new planning algorithms that are more "decisive" than their original possibilistic counterparts. We first present optimistic and pessimistic lexicographic preference relations between policies with and without intermediate utilities that refine the optimistic and pessimistic qualitative utilities respectively. We prove that these new proposed criteria satisfy the principle of Pareto efficiency as well as the property of strict monotonicity. This latter guarantees that dynamic programming algorithm can be used for calculating lexicographic optimal policies. Considering the problem of policy optimization in possibilistic decision trees and finite-horizon Markov decision processes, we provide adaptations of dynamic programming algorithm that calculate lexicographic optimal policy in polynomial time. These algorithms are based on the lexicographic comparison of the matrices of trajectories associated to the sub-policies. This algorithmic work is completed with an experimental study that shows the feasibility and the interest of the proposed approach. Then we prove that the lexicographic criteria still benefit from an Expected Utility grounding, and can be represented by infinitesimal expected utilities. The last part of our work is devoted to policy optimization in (possibly infinite) stationary Markov Decision Processes. We propose a value iteration algorithm for the computation of lexicographic optimal policies. We extend these results to the infinite-horizon case. Since the size of the matrices increases exponentially (which is especially problematic in the infinite-horizon case), we thus propose an approximation algorithm which keeps the most interesting part of each matrix of trajectories, namely the first lines and columns. Finally, we reports experimental results that show the effectiveness of the algorithms based on the cutting of the matrices.

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.

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