Improving time bounded reachability computations in interactive Markov chains. Hatefi, H. & Hermanns, H. Science of Computer Programming.
Improving time bounded reachability computations in interactive Markov chains [link]Paper  doi  abstract   bibtex   
Interactive Markov Chains (IMCs) are compositional behaviour models extending both Continuous Time Markov Chain (CTMC) and Labelled 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 IMCs, with time bounded reachability probabilities playing a pivotal role. This paper addresses the accuracy and efficiency of approximating time bounded reachability probabilities in IMCs, improving over the state-of-the-art in both efficiency of computation and tightness of approximation. Moreover, a stable numerical approach, which provides an effective framework for implementation of the theory, is proposed. Experimental evidence demonstrates the efficiency of the new approach.
@article{ hatefi_improving_????,
  title = {Improving time bounded reachability computations in interactive {Markov} chains},
  issn = {0167-6423},
  url = {http://www.sciencedirect.com/science/article/pii/S0167642315000994},
  doi = {10.1016/j.scico.2015.05.003},
  abstract = {Interactive Markov Chains (IMCs) are compositional behaviour models extending both Continuous Time Markov Chain (CTMC) and Labelled 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 IMCs, with time bounded reachability probabilities playing a pivotal role. This paper addresses the accuracy and efficiency of approximating time bounded reachability probabilities in IMCs, improving over the state-of-the-art in both efficiency of computation and tightness of approximation. Moreover, a stable numerical approach, which provides an effective framework for implementation of the theory, is proposed. Experimental evidence demonstrates the efficiency of the new approach.},
  urldate = {2015-08-05TZ},
  journal = {Science of Computer Programming},
  author = {Hatefi, Hassan and Hermanns, Holger},
  keywords = {Discretisation, Interactive Markov chains, Root finding, Time bounded reachability}
}
Downloads: 0