%0 Conference Proceedings
%T Improving Time Bounded Reachability Computations in Interactive Markov Chains
%+ Max-Planck-Institut für Informatik (MPII)
%+ Saarland University [Saarbrücken]
%A Hatefi, Hassan
%A Hermanns, Holger
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 5th International Conference on Fundamentals of Software Engineering (FSEN)
%C Tehran, Iran
%Y Farhad Arbab
%Y Marjan Sirjani
%I Springer Berlin Heidelberg
%3 Fundamentals of Software Engineering
%V LNCS-8161
%P 250-266
%8 2013-04-24
%D 2013
%R 10.1007/978-3-642-40213-5_16
%Z Computer Science [cs]Conference papers
%X Interactive Markov Chains ($\text {IMCs}$) are compositional behaviour models extending both Continuous Time Markov Chain (CTMC) and Labeled Transition System (LTS). They are used as semantic models in different engineering contexts ranging from ultramodern satellite designs to industrial system-on-chip manufacturing. Different approximation algorithms have been proposed for model checking of $\text {IMC}$, with time bounded reachability probabilities playing a pivotal role. This paper addresses the accuracy and efficiency of approximating time bounded reachability probabilities in $\text {IMC}$, improving over the state-of-the-art in both efficiency of computation and tightness of approximation. Experimental evidence is provided by applying the new method on a case study.
%G English
%2 https://inria.hal.science/hal-01514669/document
%2 https://inria.hal.science/hal-01514669/file/978-3-642-40213-5_16_Chapter.pdf
%L hal-01514669
%U https://inria.hal.science/hal-01514669
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-TC2
%~ IFIP-WG2-2
%~ IFIP-FSEN
%~ IFIP-LNCS-8161