کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
434920 | 1441640 | 2015 | 17 صفحه PDF | دانلود رایگان |
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.
Journal: Science of Computer Programming - Volume 112, Part 1, 15 November 2015, Pages 58–74