文章基本信息

标题：An Extension of the Inverse Method to Probabilistic Timed Automata
本地全文：下载
作者：Étienne André ; Jeremy Sproston ; Laurent Fribourg 等
期刊名称：Electronic Communications of the EASST
电子版ISSN：1863-2122
出版年度：2009
卷号：23
语种：English
出版社：European Association of Software Science and Technology (EASST)
摘要：Probabilistic timed automata can be used to model systems in which probabilistic and timing behavior coexist. Verification of probabilistic timed automata models is generally performed with regard to a single reference valuation of the timing parameters. Given such a parameter valuation, we present a method for obtaining automatically a constraint on timing parameters for which the reachability probabilities (1) remain invariant and (2) are equal to the reachability probabilities for the reference valuation. The method relies on parametric analysis of a non-probabilistic version of the probabilistic timed automata model using the "inverse method'". Our approach is useful for avoiding repeated executions of probabilistic model checking analyses for the same model with different parameter valuations. We provide examples of the application of our technique to models of randomized protocols.