Improving time bounded reachability computations in interactive Markov chains

详细信息    查看全文

• 作者：Hassan Hatefi ; ^{hhatefi@cs.uni-saarland.de" class="auth_mail" title="E-mail the corresponding author} ; Holger Hermanns ^{hermanns@cs.uni-saarland.de" class="auth_mail" title="E-mail the corresponding author}
• 关键词：Interactive Markov chains ; Time bounded reachability ; Discretisation ; Root finding
• 刊名：Science of Computer Programming
• 出版年：2015
• 出版时间：15 November 2015
• 年：2015
• 卷：112
• 期：part_P1
• 页码：58-74
• 全文大小：509 K

文摘

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.