TY - GEN
T1 - Weak stochastic comparisons for performability verification
AU - Castel-Taleb, Hind
AU - Pekergin, Nihal
PY - 2009/8/20
Y1 - 2009/8/20
N2 - The probabilistic model checking provides a precise formalism for the performance and reliability verification of telecommunication systems modeled by Markov chains. We study a queueing system similar to a Jackson network except that queues have a finite capacity. We propose to study in this paper (state and path) formulas from the Continuous Stochastic Logic (CSL), in order to verify performability properties. Unfortunately, transient and stationary analysis is very complex for multidimensional Markov processes. So we propose to use the stochastic comparisons in the sense of weak orderings to define bounding processes. Bounding processes are represented by independent M/M/1 queues for which transient and stationary distributions can be computed as the product of probability distributions of each queue. We use the increasing set method, and we develop an intuitive formalism based on events to establish weak stochastic comparisons.
AB - The probabilistic model checking provides a precise formalism for the performance and reliability verification of telecommunication systems modeled by Markov chains. We study a queueing system similar to a Jackson network except that queues have a finite capacity. We propose to study in this paper (state and path) formulas from the Continuous Stochastic Logic (CSL), in order to verify performability properties. Unfortunately, transient and stationary analysis is very complex for multidimensional Markov processes. So we propose to use the stochastic comparisons in the sense of weak orderings to define bounding processes. Bounding processes are represented by independent M/M/1 queues for which transient and stationary distributions can be computed as the product of probability distributions of each queue. We use the increasing set method, and we develop an intuitive formalism based on events to establish weak stochastic comparisons.
U2 - 10.1007/978-3-642-02205-0_21
DO - 10.1007/978-3-642-02205-0_21
M3 - Conference contribution
AN - SCOPUS:68749102027
SN - 3642022049
SN - 9783642022043
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 294
EP - 308
BT - Analytical and Stochastic Modeling Techniques and Applications - 16th International Conference, ASMTA 2009, Proceedings
T2 - 16th International Conference on Analytical and Stochastic Modeling Techniques and Applications, ASMTA 2009
Y2 - 9 June 2009 through 12 June 2009
ER -