Nous proposons dans cette thèse plusieurs contributions relatives à la vérification quantitative des systèmes. Cette discipline vise à évaluer les propriétés fonctionnelles et les performances d'un système. Une telle vérification requiert deux ingrédients : un modèle formel de représentation d'un système et une logique temporelle pour exprimer la propriété considérée. L'évaluation est alors faite par une méthode statistique ou numérique. La complexité spatiale des méthodes numériques, proportionnelle à la taille de l'espace d'états, les rend impraticables si les systèmes présentent une combinatoire importante. La méthode de comparaison stochastique basée sur les chaînes de Markov censurées réduit la mémoire occupée en restreignant l'analyse à un sous-ensemble des états de la chaîne originale. Dans cette thèse nous fournissons de nouvelles bornes dépendant de l'information disponible relative à la chaîne. Nous introduisons une nouvelle logique temporelle quantitative appelée Hybrid Automata Stochastic Logic (HASL), pour la vérification des processus stochastiques à événements discrets (DESP).HASL emploie les automates linéaires hybrides (LHA) pour sélectionner des préfixes de chemins d'exécution d'un DESP. LHA permet de collecter des informations élaborées durant la génération des chemins, fournissant ainsi à l'utilisateur un moyen d'exprimer des mesures sophistiquées. HASL supporte donc des raisonnements temporels mixés avec une analyse à base de récompenses. Nous avons aussi développé COSMOS, un outil qui implémente la vérification statistique de formules HASL pour des réseaux de Petri stochastiques. Les ateliers flexibles (FMS) ont souvent été modélisés par des réseaux de Petri. Cependant le modélisateur doit avoir une bonne connaissance de ce formalisme. Afin de faciliter cette modélisation nous proposons une méthodologie de modélisation compositionnelle orientée vers les applications qui ne requiert aucune connaissance des réseaux de Petri. / We propose in this thesis several contributions related to the quantitative verification of systems. This discipline aims to evaluate functional and performance properties of a system. Such a verification requires two ingredients: a formal model to represent the system and a temporal logic to express the desired property. Then the evaluation is done with a statistical or numerical method. The spatial complexity of numerical methods which is proportional to the size of the state space of the model makes them impractical when the state space is very large. The method of stochastic comparison with censored Markov chains is one of the methods that reduces memory requirements by restricting the analysis to a subset of the states of the original Markov chain. In this thesis we provide new bounds that depend on the available information about the chain. We introduce a new quantitative temporal logic named Hybrid Automata Stochastic Logic (HASL), for the verification of discrete event stochastic processes (DESP). HASL employs Linear Hybrid Automata (LHA) to select prefixes of relevant execution paths of a DESP. LHA allows rather elaborate information to be collected on-the-fly during path selection, providing the user with a powerful mean to express sophisticated measures. In essence HASL provides a unifying verification framework where temporal reasoning is naturally blended with elaborate reward-based analysis. We have also developed COSMOS, a tool that implements statistical verification of HASL formulas over stochastic Petri nets. Flexible manufacturing systems (FMS) have often been modelized by Petri nets. However the modeler should have a good knowledge of this formalism. In order to facilitate such a modeling we propose a methodology of compositional modeling that is application oriented and does not require any knowledge of Petri nets by the modeler.

We propose in this thesis several contributions related to the quantitative verification of systems. This discipline aims to evaluate functional and performance properties of a system. Such a verification requires two ingredients: a formal model to represent the system and a temporal logic to express the desired property. Then the evaluation is done with a statistical or numerical method. The spatial complexity of numerical methods which is proportional to the size of the state space of the model makes them impractical when the state space is very large. The method of stochastic comparison with censored Markov chains is one of the methods that reduces memory requirements by restricting the analysis to a subset of the states of the original Markov chain. In this thesis we provide new bounds that depend on the available information about the chain. We introduce a new quantitative temporal logic named Hybrid Automata Stochastic Logic (HASL), for the verification of discrete event stochastic processes (DESP). HASL employs Linear Hybrid Automata (LHA) to select prefixes of relevant execution paths of a DESP. LHA allows rather elaborate information to be collected on-the-fly during path selection, providing the user with a powerful mean to express sophisticated measures. In essence HASL provides a unifying verification framework where temporal reasoning is naturally blended with elaborate reward-based analysis. We have also developed COSMOS, a tool that implements statistical verification of HASL formulas over stochastic Petri nets. Flexible manufacturing systems (FMS) have often been modelized by Petri nets. However the modeler should have a good knowledge of this formalism. In order to facilitate such a modeling we propose a methodology of compositional modeling that is application oriented and does not require any knowledge of Petri nets by the modeler.

Las redes inal´ambricas actuales exhiben caracter´ısticas heterog´eneas de acceso m´ultiple mediante el despliegue, la coexistencia y la cooperaci´on de varias Tecnolog ´ıas de Acceso Radio (RAT2). En este escenario, la prestaci´on de servicios multimedia garantizando una cierta calidad de servicio (QoS3) es obligatoria. El objetivo global de las redes heterog´eneas de acceso inal´ambrico consiste en sustentar la realizaci´on del concepto ABC (del ingl´es Always Best Connected), en el que un usuario est´a siempre conectado a la RAT que mejor satisface sus necesidades de servicio en cualquier momento, en cualquier lugar, de cualquier modo. En este sentido, las estrat´egias de gesti´on de recursos radio comunes [del ingl´es, Common Radio Resource Management (CRRM)] se dise˜nan para proporcionar una utilizaci´on eficiente de los recursos radio y de espectro radioel´ectrico dentro de la red heterog´enea, ofreciendo un mejor rendimiento en comparaci´on con la realizaci´on independiente de RRM en cada RAT. Adem´as, los recursos de espectro asignados a cada una de las RATs deben ser utilizado de manera eficiente, ya que se trata de un recurso escaso y costoso. En este sentido, conceptos y metodolog´ıas de radio cognitiva (del ingl´es Cognitive Radio o CR) se han aplicado a la gesti´on del espectro, permitiendo una compartici´on dinamico-oportunista del mismo. En estos casos, el espectro sujeto a licencia se abre hacia el acceso de usuarios sin licencia siempre que no perjudiquen y que el funcionamiento libre de interferencias est´e garantizado. Esta tesis analiza estrategias de gesti´on de recursos radio y de espectro para ofrecer un uso mayor y eficiente de los escasos recursos radio y de espectro con el objetivo final de aumentar al m´aximo la capacidad de usuario, garantizando los requerimientos de QoS. En concreto, estas tesis se centra primero en como seleccionar una RAT al inicio de una llamada/sesi´on (en adelante, selecci´on inicial de RAT) en una red de acceso heterog´enea. Un modelo de Markov ha sido desarrollado para definir la asignaci´on de m´ultiples servicios (multi-servicio) en m´ultiples RATs (multi-acceso). En este marco, varias pol´ıticas de selecci´on de RAT son propuestas y evaluadas, gen´ericamente clasific´andose en pol´ıticas basadas en servicio (SB4) y basadas en balanceo de carga (LB5). Adem´as, el rendimiento de las pol´ıticas de selecci´on de RATs en escenarios de acceso limitado debido a la deficiente cobertura radio, la falta de disponibilidad de terminales multi-modo y la incompatibilidad entre RAT y servicios tambi´en es evaluada. Principios espec´ıficos para la asignaci´on de servicios a RATs ser´an provistos en los escenarios antes mencionados con el objetivo general de aumentar la capacidad de usuarios, garantizando los requisitos m´ınimos de calidad de servicio. Finalmente, la congesti´on en el acceso radio tambi´en se trata en este escenario multi-acceso/multi-servicio y el impacto de la selecci´on de RAT evaluado. Los principios para la asignaci´on inicial de RAT con tal de evitar la congesti´on radio ser´an tambi´en proporcionados. En segundo lugar, esta tesis investiga sobre la forma de maximizar el uso eficiente del espectro sujeto a licencia (o licenciado) por medio del acceso din´amicooportunista de espectro a usuarios sin licencia. En este sentido, se concibe un modelo de Markov para captar el problema del uso compartido de espectro entre usuarios con y sin licencia. Un modelo basado en sensado de espectro se propone con el fin de detectar porciones de espectro no utilizados (en ingl´es white spaces) que pueden ser usados por los usuarios sin licencia mientras este siga libre. En este marco, los beneficios obtenidos de la compartici´on del espectro son investigados y las ventajas que implican evaluadas. En concreto, se eval´ua el rendimiento obtenido al ajustar el punto de funcionamiento (en ingl´es operating point ) del mecanismo de sensado, el cual determina los errores de no-detecci´on y falsa-alarma. Por otra parte, sistemas de canalizaci´on de espectro fijos versus adaptativos ser´an propuestos y analizados bajo dos disciplinas de servicio diferentes, cuya duraci´on (o tiempo de permanencia en el sistema) esta basada en tiempo y en contenido respectivamente. / Current wireless networks exhibit heterogeneous multi-access features by means of the coexisting and cooperative deployment of several Radio Access Technologies (RATs). In this scenario, the provision of multimedia services with ensured Quality of Service (QoS) is mandatory. The overall goal of heterogeneous wireless access networks is to enable the realization of the Always Best Connected concept in which a user is seamlessly connected to the RAT best suiting its service requirements anytime, anywhere, anyhow. In this sense, Common Radio Resource Management (CRRM) strategies are devoted to provide an efficient utilization of radio resources within the heterogeneous network offering improved performances as opposed to performing stand-alone RRM in each RAT. In addition, allocated spectrum resources to each RAT must be efficiently utilized since it is a scarce and expensive resource. In this respect, cognitive radio concepts and methodologies have been applied to spectrum management by enabling dynamic/opportunistic spectrum sharing. In these scenarios, licensed spectrum is opened towards unlicensed access provided a non-harmful operation is guaranteed. This dissertation discusses both radio resource and spectrum management strategies to provide an utmost and efficient use of scarce radio/spectrum resources with the overall goal of maximizing user capacity while guaranteeing QoS constraints.Specifically, the thesis is first focused on how to select an appropriate RAT upon call/session initiation (henceforth, initial RAT selection) in a heterogeneous access network. A Markovian framework is developed to such extent supporting the allocation of multiple service-type users (multi-service) on multiple RATs (multi-access). Under this framework, several RAT selection policies are proposed and evaluated, broadly categorized into service-based (SB) and load-balancing (LB). In addition, the performance of RAT selection policies in access-limited scenarios due to poor radio coverage, non multi-mode terminal availability and RAT-service incompatibility is also evaluated. Specific guiding principles for the allocation of services on several RATs are provided in the abovementioned scenarios with the overall goal of increasing user capacity while guaranteeing minimum QoS requirements. Finally, radio access congestion is also addressed in this multi-access/multi-service scenario and the impact RAT selection assessed. Suitable allocation principles avoiding congestion are also provided.Secondly, this dissertation investigates on how to efficiently maximize the use of licensed spectrum by means of dynamic/opportunistic unlicensed spectrum access. Hereof, a Markovian framework is also devised to capture the problem of licensed spectrum sharing towards unlicensed users. A sensing-based spectrum awareness model is proposed in order to detect unused spectrum (so-called white spaces) which may be accessed by unlicensed users while remaining unused. Under this framework, the benefits of spectrum sharing are investigated and the involved gains assessed. Specifically, the sensing-throughput tradeoff and the adjustment of the sensing mechanism’s operating point, which tradeoffs missed-detection and false-alarm errors, is evaluated. Moreover, fixed vs. adaptive spectrum channelization schemes are proposed and analyzed under two different service disciplines considering time-based and volume-based content delivery.

No description available.

Probabilistic model checking mainly concentrates on techniques for reasoning about the probabilities of certain path properties or expected values of certain random variables. For the quantitative system analysis, however, there is also another type of interesting performance measure, namely quantiles. A typical quantile query takes as input a lower probability bound p ∈ ]0,1] and a reachability property. The task is then to compute the minimal reward bound r such that with probability at least p the target set will be reached before the accumulated reward exceeds r. Quantiles are well-known from mathematical statistics, but to the best of our knowledge they have not been addressed by the model checking community so far. In this paper, we study the complexity of quantile queries for until properties in discrete-time finite-state Markov decision processes with nonnegative rewards on states. We show that qualitative quantile queries can be evaluated in polynomial time and present an exponential algorithm for the evaluation of quantitative quantile queries. For the special case of Markov chains, we show that quantitative quantile queries can be evaluated in pseudo-polynomial time.

Hierarchical Markovian Models (HMMs) are composed of multiple low level models (LLMs) and high level model (HLM) that defines the interaction among LLMs. The essence of the HMM approach is to model the system at hand in the form of interacting components so that its (larger) underlying continous-time Markov chain (CTMC) is not generated but implicitly represented as a sum of Kronecker products of (smaller) component matrices. The Kronecker structure of an HMM induces nested block partitionings in its underlying CTMC. These partitionings may be used in block versions of classical iterative methods based on splittings, such as block SOR (BSOR), to solve the underlying CTMC for its stationary vector. Therein the problem becomes that of solving multiple nonsingular linear systems whose coefficient matrices are the diagonal blocks of a particular partitioning. This paper shows that in each HLM state there may be diagonal blocks with identical off-diagonal parts and diagonals differing from each other by a multiple of the identity matrix. Such diagonal blocks are named candidate blocks. The paper explains how candidate blocks can be detected and how the can mutually benefit from a single real Schur factorization. It gives sufficient conditions for the existence of diagonal blocks with real eigenvalues and shows how these conditions can be checked using component matrices. It describes how the sparse real Schur factors of candidate blocks satisfying these conditions can be constructed from component matrices and their real Schur factors. It also demonstrates how fill in- of LU factorized (non-candidate) diagonal blocks can be reduced by using the column approximate minimum degree algorithm (COLAMD). Then it presents a three-level BSOR solver in which the diagonal blocks at the first level are solved using block Gauss-Seidel (BGS) at the second and the methods of real Schur and LU factorizations at the third level. Finally, on a set of numerical experiments it shows how these ideas can be used to reduce the storage required by the factors of the diagonal blocks at the third level and to improve the solution time compared to an all LU factorization implementation of the three-level BSOR solver.

Kronecker structured representations are used to cope with the state space explosion problem in Markovian modeling and analysis. Currently an open research problem is that of devising strong preconditioners to be used with projection methods for the computation of the stationary vector of Markov chains (MCs) underlying such representations. This paper proposes a block SOR (BSOR) preconditioner for hierarchical Markovian Models (HMMs) that are composed of multiple low level models and a high level model that defines the interaction among low level models. The Kronecker structure of an HMM yields nested block partitionings in its underlying continuous-time MC which may be used in the BSOR preconditioner. The computation of the BSOR preconditioned residual in each iteration of a preconditioned projection method becoms the problem of solving multiple nonsingular linear systems whose coefficient matrices are the diagonal blocks of the chosen partitioning. The proposed BSOR preconditioner solvers these systems using sparse LU or real Schur factors of diagonal blocks. The fill-in of sparse LU factorized diagonal blocks is reduced using the column approximate minimum degree algorithm (COLAMD). A set of numerical experiments are presented to show the merits of the proposed BSOR preconditioner.

Probabilistic model checking mainly concentrates on techniques for reasoning about the probabilities of certain path properties or expected values of certain random variables. For the quantitative system analysis, however, there is also another type of interesting performance measure, namely quantiles. A typical quantile query takes as input a lower probability bound p ∈ ]0,1] and a reachability property. The task is then to compute the minimal reward bound r such that with probability at least p the target set will be reached before the accumulated reward exceeds r. Quantiles are well-known from mathematical statistics, but to the best of our knowledge they have not been addressed by the model checking community so far. In this paper, we study the complexity of quantile queries for until properties in discrete-time finite-state Markov decision processes with nonnegative rewards on states. We show that qualitative quantile queries can be evaluated in polynomial time and present an exponential algorithm for the evaluation of quantitative quantile queries. For the special case of Markov chains, we show that quantitative quantile queries can be evaluated in pseudo-polynomial time.

Kronecker structured representations are used to cope with the state space explosion problem in Markovian modeling and analysis. Currently an open research problem is that of devising strong preconditioners to be used with projection methods for the computation of the stationary vector of Markov chains (MCs) underlying such representations. This paper proposes a block SOR (BSOR) preconditioner for hierarchical Markovian Models (HMMs) that are composed of multiple low level models and a high level model that defines the interaction among low level models. The Kronecker structure of an HMM yields nested block partitionings in its underlying continuous-time MC which may be used in the BSOR preconditioner. The computation of the BSOR preconditioned residual in each iteration of a preconditioned projection method becoms the problem of solving multiple nonsingular linear systems whose coefficient matrices are the diagonal blocks of the chosen partitioning. The proposed BSOR preconditioner solvers these systems using sparse LU or real Schur factors of diagonal blocks. The fill-in of sparse LU factorized diagonal blocks is reduced using the column approximate minimum degree algorithm (COLAMD). A set of numerical experiments are presented to show the merits of the proposed BSOR preconditioner.

Hierarchical Markovian Models (HMMs) are composed of multiple low level models (LLMs) and high level model (HLM) that defines the interaction among LLMs. The essence of the HMM approach is to model the system at hand in the form of interacting components so that its (larger) underlying continous-time Markov chain (CTMC) is not generated but implicitly represented as a sum of Kronecker products of (smaller) component matrices. The Kronecker structure of an HMM induces nested block partitionings in its underlying CTMC. These partitionings may be used in block versions of classical iterative methods based on splittings, such as block SOR (BSOR), to solve the underlying CTMC for its stationary vector. Therein the problem becomes that of solving multiple nonsingular linear systems whose coefficient matrices are the diagonal blocks of a particular partitioning. This paper shows that in each HLM state there may be diagonal blocks with identical off-diagonal parts and diagonals differing from each other by a multiple of the identity matrix. Such diagonal blocks are named candidate blocks. The paper explains how candidate blocks can be detected and how the can mutually benefit from a single real Schur factorization. It gives sufficient conditions for the existence of diagonal blocks with real eigenvalues and shows how these conditions can be checked using component matrices. It describes how the sparse real Schur factors of candidate blocks satisfying these conditions can be constructed from component matrices and their real Schur factors. It also demonstrates how fill in- of LU factorized (non-candidate) diagonal blocks can be reduced by using the column approximate minimum degree algorithm (COLAMD). Then it presents a three-level BSOR solver in which the diagonal blocks at the first level are solved using block Gauss-Seidel (BGS) at the second and the methods of real Schur and LU factorizations at the third level. Finally, on a set of numerical experiments it shows how these ideas can be used to reduce the storage required by the factors of the diagonal blocks at the third level and to improve the solution time compared to an all LU factorization implementation of the three-level BSOR solver.