Skip to Main content Skip to Navigation
Conference papers

Improving Time Bounded Reachability Computations in Interactive Markov Chains

Abstract : 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [25 references]  Display  Hide  Download

https://hal.inria.fr/hal-01514669
Contributor : Hal Ifip <>
Submitted on : Wednesday, April 26, 2017 - 3:22:13 PM
Last modification on : Thursday, September 20, 2018 - 7:54:02 AM
Long-term archiving on: : Thursday, July 27, 2017 - 12:53:31 PM

File

978-3-642-40213-5_16_Chapter.p...
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Hassan Hatefi, Holger Hermanns. Improving Time Bounded Reachability Computations in Interactive Markov Chains. 5th International Conference on Fundamentals of Software Engineering (FSEN), Apr 2013, Tehran, Iran. pp.250-266, ⟨10.1007/978-3-642-40213-5_16⟩. ⟨hal-01514669⟩

Share

Metrics

Record views

204

Files downloads

538