In insurance risk theory, the surplus of an insurance company is modelled to monitor and quantify its risks. With the outgo of claims and inflow of premiums, the insurer needs to determine what financial portfolio ensures the soundness of the company’s future while satisfying the shareholders’ interests. It is usually assumed that the net profit condition (i.e. the expectation of the process is positive) is satisfied, which then implies that this process would drift towards infinity. To correct this unrealistic behaviour, the surplus process was modified to include the payout of dividends until the time of ruin. Under this more realistic surplus process, a topic of growing interest is determining which dividend strategy is optimal, where optimality is in the sense of maximizing the expected present value of dividend payments. This problem dates back to the work of Bruno De Finetti (1957) where it was shown that if the surplus process is modelled as a random walk with ± 1 step sizes, the optimal dividend payment strategy is a barrier strategy. Such a strategy pays as dividends any excess of the surplus above some threshold. Since then, other examples where a barrier strategy is optimal include the Brownian motion model (Gerber and Shiu (2004)) and the compound Poisson process model with exponential claims (Gerber and Shiu (2006)). In this thesis, we focus on the optimality of a barrier strategy in the more general Lévy risk models. The risk process will be formulated as a spectrally negative Lévy process, a continuous-time stochastic process with stationary increments which provides an extension of the classical Cramér-Lundberg model. This includes the Brownian and the compound Poisson risk processes as special cases. In this setting, results are expressed in terms of “scale functions”, a family of functions known only through their Laplace transform. In Loeffen (2008), we can find a sufficient condition on the jump distribution of the process for a barrier strategy to be optimal. This condition was then improved upon by Loeffen and Renaud (2010) while considering a more general control problem. The first chapter provides a brief review of theory of spectrally negative Lévy processes and scale functions. In chapter 2, we define the optimal dividends problem and provide existing results in the literature. When the surplus process is given by the Cramér-Lundberg process with a Brownian motion component, we provide a sufficient condition on the parameters of this process for the optimality of a dividend barrier strategy. Chapter 3 focuses on the case when the claims distribution is given by a univariate mixture of Erlang distributions with a common scale parameter. Analytical results for the Value-at-Risk and Tail-Value-at-Risk, and the Euler risk contribution to the Conditional Tail Expectation are provided. Additionally, we give some results for the scale function and the optimal dividends problem. In the final chapter, we propose an expectation maximization (EM) algorithm similar to that in Lee and Lin (2009) for fitting the univariate distribution to data. This algorithm is implemented and numerical results on the goodness of fit to sample data and on the optimal dividends problem are presented.

Dažnai realių stochastinių sistemų negalime aprašyti Markovo procesais, nes operacijų trukmės nėra pasiskirstę pagal eksponentinį dėsnį. Šiame darbe nagrinėjome sistemų aproksimavimo galimybes, taikant eksponentinių skirstinių mišinius ir sąsūkas. Skirstinių aproksimavimui taikėme Erlango mišinius ir Kokso skirstinį. Skirstinių aproksimavimą pritaikėme aptarnavimo sistemų M/G/1 ir G/M/1 tyrimui. Atlikti teoriniai skaičiavimai parodė, kad gaunamas aukštas aproksimavimo tikslumas. Aptarnavimo sistemų modeliavimui naudojome skaitmeninio Markovo procesų modeliavimo sistemą naudojant įvykių kalbą. Darbe sukurti metodai leidžia tiksliai apskaičiuoti sistemų charakteristikas, naudojant aproksimavimą eksponentiniais mišiniais ir sąsūkomis. Sukurta programinė įranga leidžia automatizuoti sistemų M/G/1 ir G/M/1 modeliavimą, naudojant aproksimavimą eksponentiniais mišiniais. Sistemos G/G/1 ( neištiriamos analiziniais metodais ) aproksimavimo rezultatai leidžia tikėtis, kad šiame darbe nagrinėjamas metodas gali būti naudojamas ir sudėtingų sistemų modeliavime. / Application of numerical methods with approximation allows to extend a class of systems represented by Markovian processes under investigation compared with analytical methods. In this paper we used approximation of positive distribution functions, using phase-type distributions: mixtures of Erlang distributions and Coxian distribution – both 2 and 3 moments-matching algorithms was used. Analysis of M/G/1 and G/M/1 queueing systems showed, that moment-based queueing approximation gives high accuracy. In purpose to compute characteristics of M/G/1 and G/M/1 systems described in an event-based language, algorithms and software was created. Comparison to simulation results shows, that event-based language enables to get more precise results. Analysis of G/G/1 systems showed, that moment-based approximation can be used to analyse difficult queueing systems.

In insurance risk theory, the surplus of an insurance company is modelled to monitor and quantify its risks. With the outgo of claims and inflow of premiums, the insurer needs to determine what financial portfolio ensures the soundness of the company’s future while satisfying the shareholders’ interests. It is usually assumed that the net profit condition (i.e. the expectation of the process is positive) is satisfied, which then implies that this process would drift towards infinity. To correct this unrealistic behaviour, the surplus process was modified to include the payout of dividends until the time of ruin. Under this more realistic surplus process, a topic of growing interest is determining which dividend strategy is optimal, where optimality is in the sense of maximizing the expected present value of dividend payments. This problem dates back to the work of Bruno De Finetti (1957) where it was shown that if the surplus process is modelled as a random walk with ± 1 step sizes, the optimal dividend payment strategy is a barrier strategy. Such a strategy pays as dividends any excess of the surplus above some threshold. Since then, other examples where a barrier strategy is optimal include the Brownian motion model (Gerber and Shiu (2004)) and the compound Poisson process model with exponential claims (Gerber and Shiu (2006)). In this thesis, we focus on the optimality of a barrier strategy in the more general Lévy risk models. The risk process will be formulated as a spectrally negative Lévy process, a continuous-time stochastic process with stationary increments which provides an extension of the classical Cramér-Lundberg model. This includes the Brownian and the compound Poisson risk processes as special cases. In this setting, results are expressed in terms of “scale functions”, a family of functions known only through their Laplace transform. In Loeffen (2008), we can find a sufficient condition on the jump distribution of the process for a barrier strategy to be optimal. This condition was then improved upon by Loeffen and Renaud (2010) while considering a more general control problem. The first chapter provides a brief review of theory of spectrally negative Lévy processes and scale functions. In chapter 2, we define the optimal dividends problem and provide existing results in the literature. When the surplus process is given by the Cramér-Lundberg process with a Brownian motion component, we provide a sufficient condition on the parameters of this process for the optimality of a dividend barrier strategy. Chapter 3 focuses on the case when the claims distribution is given by a univariate mixture of Erlang distributions with a common scale parameter. Analytical results for the Value-at-Risk and Tail-Value-at-Risk, and the Euler risk contribution to the Conditional Tail Expectation are provided. Additionally, we give some results for the scale function and the optimal dividends problem. In the final chapter, we propose an expectation maximization (EM) algorithm similar to that in Lee and Lin (2009) for fitting the univariate distribution to data. This algorithm is implemented and numerical results on the goodness of fit to sample data and on the optimal dividends problem are presented.

Data originating from non-voice sources is expected to play an increasingly important role in the next generation mobile communication services. To plan these networks, a detailed understanding of their traffic load is essential. Recent experimental studies have shown that network traffic originating from data applications can be self-similar, leading to a different queueing behavior than predicted by conventional traffic models. Heavy tailed probability distributions are appropriate for capturing this property, but including those random processes in a performance analysis makes it difficult and often impossible to find numerical results. In this thesis three related topics are addressed: It is shown that Markovian models with a large state space can be used to describe traffic which is self-similar over a large time scale, a Maximum Likelihood approach to fit parallel Erlang-k distributions directly to time series is developed, and the performance of a channel assignment procedure in a wireless communication network is evaluated using the above mentioned techniques to set up a Markovian model. Outcomes of the performance analysis are blocking probabilities and latency due to restrictions of the channel assignment procedure as well as estimations of the overall bandwidth that the system is required to offer in order to support a given number of users.

Ce mémoire décrit et évalue un système de module qui améliore la migration de code dans le langage de programmation distribuée Termite Scheme. Ce système de module a la possibilité d’être utilisé dans les applications qu’elles soient distribuées ou pas. Il a pour but de faciliter la conception des programmes dans une structure modulaire et faciliter la migration de code entre les nœuds d’un système distribué. Le système de module est conçu pour le système Gambit Scheme, un compilateur et interprète du langage Scheme utilisé pour implanter Termite. Le système Termite Scheme est utilisé pour implémenter les systèmes distribués. Le problème qui est résolu est la diffusion de code compilé entre les nœuds d’un système distribué quand le nœud destination n’a aucune connaissance préalable du code qu’il reçoit. Ce problème est difficile car les nœuds sont hétérogènes, ils ont différentes architectures (x86, ARM). Notre approche permet d’identifier les modules de façon unique dans un contexte dis- tribué. La facilité d’utilisation et la portabilité ont été des facteurs importants dans la conception du système de module. Le mémoire décrit la structure des modules, leur implémentation dans Gambit et leur application. Les qualités du système de module sont démontrées par des exemples et la performance est évaluée expérimentallement. / This thesis presents a module system for Termite Scheme that supports distributed computing. This module system facilitates application modularity and eases code migration between the nodes of a distributed system. This module system also works for developing non-distributed applications. The Gambit Scheme system is used to implement the distributed Termite and the Module system. The problem that is solved is the migration of compiled code between nodes of a distributed system when the receiving node has no prior knowledge of the code. This is a challenging problem because the nodes are not homogenous, they have different architectures (ARM, x86). Our approach uses a naming model for the modules that uniquely identifies them in a distributed context. Both ease of use and portability were important factors in the design of the module system. The thesis describes a module system and how it was integrated into Gambit. The system allows developing distributed modular systems. The features of this system are shown through application examples and the performance is evaluated experimentally.

Nous y introduisons une nouvelle classe de distributions bivariées de type Marshall-Olkin, la distribution Erlang bivariée. La transformée de Laplace, les moments et les densités conditionnelles y sont obtenus. Les applications potentielles en assurance-vie et en finance sont prises en considération. Les estimateurs du maximum de vraisemblance des paramètres sont calculés par l'algorithme Espérance-Maximisation. Ensuite, notre projet de recherche est consacré à l'étude des processus de risque multivariés, qui peuvent être utiles dans l'étude des problèmes de la ruine des compagnies d'assurance avec des classes dépendantes. Nous appliquons les résultats de la théorie des processus de Markov déterministes par morceaux afin d'obtenir les martingales exponentielles, nécessaires pour établir des bornes supérieures calculables pour la probabilité de ruine, dont les expressions sont intraitables. / In this contribution, we introduce a new class of bivariate distributions of Marshall-Olkin type, called bivariate Erlang distributions. The Laplace transform, product moments and conditional densities are derived. Potential applications of bivariate Erlang distributions in life insurance and finance are considered. Further, our research project is devoted to the study of multivariate risk processes, which may be useful in analyzing ruin problems for insurance companies with a portfolio of dependent classes of business. We apply results from the theory of piecewise deterministic Markov processes in order to derive exponential martingales needed to establish computable upper bounds of the ruin probabilities, as their exact expressions are intractable.

Nous y introduisons une nouvelle classe de distributions bivariées de type Marshall-Olkin, la distribution Erlang bivariée. La transformée de Laplace, les moments et les densités conditionnelles y sont obtenus. Les applications potentielles en assurance-vie et en finance sont prises en considération. Les estimateurs du maximum de vraisemblance des paramètres sont calculés par l'algorithme Espérance-Maximisation. Ensuite, notre projet de recherche est consacré à l'étude des processus de risque multivariés, qui peuvent être utiles dans l'étude des problèmes de la ruine des compagnies d'assurance avec des classes dépendantes. Nous appliquons les résultats de la théorie des processus de Markov déterministes par morceaux afin d'obtenir les martingales exponentielles, nécessaires pour établir des bornes supérieures calculables pour la probabilité de ruine, dont les expressions sont intraitables. / In this contribution, we introduce a new class of bivariate distributions of Marshall-Olkin type, called bivariate Erlang distributions. The Laplace transform, product moments and conditional densities are derived. Potential applications of bivariate Erlang distributions in life insurance and finance are considered. Further, our research project is devoted to the study of multivariate risk processes, which may be useful in analyzing ruin problems for insurance companies with a portfolio of dependent classes of business. We apply results from the theory of piecewise deterministic Markov processes in order to derive exponential martingales needed to establish computable upper bounds of the ruin probabilities, as their exact expressions are intractable.

In this dissertation, we study the verification of concurrent programs written in the programming language Erlang using infinite-state model-checking. Erlang is a widely used, higher order, dynamically typed, call-by-value functional language with algebraic data types and pattern-matching. It is further augmented with support for actor concurrency, i.e. asynchronous message passing and dynamic process creation. With decidable model-checking in mind, we identify actor communicating systems (ACS) as a suitable target model for an abstract interpretation of Erlang. ACS model a dynamic network of finite-state processes that communicate over a fixed, finite number of unordered, unbounded channels. Thanks to being equivalent to Petri nets, ACS enjoy good algorithmic properties. We develop a verification procedure that extracts a sound abstract model, in the form of an ACS, from a given Erlang program; the resulting ACS simulates the operational semantics of the input. Using this abstract model, we can conservatively verify coverability properties of the input program, i.e. a weak form of safety properties, with a Petri net model-checker. We have implemented this procedure in our tool Soter, which is the first sound verification tool for Erlang programs using infinite-state model-checking. In our experiments, we find that Soter is accurate enough to verify a range of interesting and non-trivial benchmarks. Even though ACS coverability is Expspace-complete, Soter's analysis of these verification problems is surprisingly quick. In order to improve the precision of our verification procedure with respect to recursion, we investigate an extension of ACS that allows pushdown processes: asynchronously communicating pushdown systems (ACPS). ACPS that satisfy the empty-stack constraint (a pushdown process may receive only when its stack is empty) are a popular subclass of ACPS with good decision and complexity properties. In the context of Erlang, the empty stack constraint is unfortunately not realistic. We introduce a relaxation of the empty-stack constraint for ACPS called the shaped stack constraint. Stacks that fit the shape constraint may reach arbitrary heights. Further, a process may execute any communication action (be it process creation, message send or retrieval) whether or not its stack is empty. We prove that coverability for shaped ACPS, i.e. ACPS that satisfy the shaped constraint, reduces to the decidable coverability problem for well-structured transition systems (WSTS). Thus, shaped ACPS enable the modelling and verification of a larger class of message passing programs. We establish a close connection between shaped ACPS and a novel extension of Petri nets: nets with nested coloured tokens (NNCT). Tokens in NNCT are of two types: simple and complex. Complex tokens carry an arbitrary number of coloured tokens. The rules of a NNCT can synchronise complex and simple tokens, inject coloured tokens into a complex token, and eject all tokens of a specified set of active colours to predefined places. We show that the coverability problem for NNCT is Tower-complete, a new complexity class for non-elementary decision problems introduced by Schmitz. To prove Tower-membership, we devise a geometrically inspired version of the Rackoff technique, and we obtain Tower-hardness by adapting Stockmeyer's ruler construction to NNCT. To our knowledge, NNCT is the first extension of Petri nets (belonging to the class of nets with an infinite set of token types) that is proven to have primitive recursive coverability. This result implies Tower-completeness of coverability for ACPS that satisfy the shaped stack constraint.

Les centres d’appels sont des éléments clés de presque n’importe quelle grande organisation. Le problème de gestion du travail a reçu beaucoup d’attention dans la littérature. Une formulation typique se base sur des mesures de performance sur un horizon infini, et le problème d’affectation d’agents est habituellement résolu en combinant des méthodes d’optimisation et de simulation. Dans cette thèse, nous considérons un problème d’affection d’agents pour des centres d’appels soumis a des contraintes en probabilité. Nous introduisons une formulation qui exige que les contraintes de qualité de service (QoS) soient satisfaites avec une forte probabilité, et définissons une approximation de ce problème par moyenne échantillonnale dans un cadre de compétences multiples. Nous établissons la convergence de la solution du problème approximatif vers celle du problème initial quand la taille de l’échantillon croit. Pour le cas particulier où tous les agents ont toutes les compétences (un seul groupe d’agents), nous concevons trois méthodes d’optimisation basées sur la simulation pour le problème de moyenne échantillonnale. Étant donné un niveau initial de personnel, nous augmentons le nombre d’agents pour les périodes où les contraintes sont violées, et nous diminuons le nombre d’agents pour les périodes telles que les contraintes soient toujours satisfaites après cette réduction. Des expériences numériques sont menées sur plusieurs modèles de centre d’appels à faible occupation, au cours desquelles les algorithmes donnent de bonnes solutions, i.e. la plupart des contraintes en probabilité sont satisfaites, et nous ne pouvons pas réduire le personnel dans une période donnée sont introduire de violation de contraintes. Un avantage de ces algorithmes, par rapport à d’autres méthodes, est la facilité d’implémentation. / Call centers are key components of almost any large organization. The problem of labor management has received a great deal of attention in the literature. A typical formulation of the staffing problem is in terms of infinite-horizon performance measures. The method of combining simulation and optimization is used to solve this staffing problem. In this thesis, we consider a problem of staffing call centers with respect to chance constraints. We introduce chance-constrained formulations of the scheduling problem which requires that the quality of service (QoS) constraints are met with high probability. We define a sample average approximation of this problem in a multiskill setting. We prove the convergence of the optimal solution of the sample-average problem to that of the original problem when the sample size increases. For the special case where we consider the staffing problem and all agents have all skills (a single group of agents), we design three simulation-based optimization methods for the sample problem. Given a starting solution, we increase the staffings in periods where the constraints are violated, and decrease the number of agents in several periods where decrease is acceptable, as much as possible, provided that the constraints are still satisfied. For the call center models in our numerical experiment, these algorithms give good solutions, i.e., most constraints are satisfied, and we cannot decrease any agent in any period to obtain better results. One advantage of these algorithms, compared with other methods, that they are very easy to implement.

Stateless model checking is a technique for testing and verifying concurrent programs, based on exploring the different ways in which operations executed by the processes of a concurrent program can be scheduled. The goal of the technique is to expose all behaviours that can be a result of scheduling non-determinism. As the number of possible schedulings is huge, however, techniques that reduce the number of schedulings that must be explored to achieve verification have been developed. Dynamic partial order reduction (DPOR) is a prominent such technique. This dissertation presents a number of improvements to dynamic partial order reduction that significantly increase the effectiveness of stateless model checking. Central among these improvements are the Source and Optimal DPOR algorithms (and the theoretical framework behind them) and a technique that allows the observability of the interference of operations to be used in dynamic partial order reduction. Each of these techniques can exponentially decrease the number of schedulings that need to be explored to verify a concurrent program. The dissertation also presents a simple bounding technique that is compatible with DPOR algorithms and effective for finding bugs in concurrent programs, if the number of schedulings is too big to make full verification possible in a reasonable amount of time, even when the improved algorithms are used. All improvements have been implemented in Concuerror, a tool for applying stateless model checking to Erlang programs. In order to increase the effectiveness of the tool, the interference of the high-level operations of the Erlang/OTP implementation is examined, classified and precisely characterized. Aspects of the implementation of the tool are also described. Finally, a use case is presented, showing how Concuerror was used to find bugs and verify key correctness properties in repair techniques for the CORFU chain replication protocol. / UPMARC / RELEASE