This study proposes a hierarchical probabilistic computationtreelogic, HpCTL, which is an extension of the standard probabilistic computationtreelogic pCTL, as a theoretical basis for hierarchical probabilistic CT...
详细信息
ISBN:
(纸本)9789897583506
This study proposes a hierarchical probabilistic computationtreelogic, HpCTL, which is an extension of the standard probabilistic computationtreelogic pCTL, as a theoretical basis for hierarchical probabilistic CTL model checking. hierarchical probabilistic model checking is a new paradigm that can appropriately verify hierarchical randomized (or stochastic) systems. Furthermore, a probability-measure-independent translation from HpCTL into pCTL is defined, and a theorem for embedding HpCTL into pCTL is proved using this translation. Finally, the relative decidability of HpCTL with respect to pCTL is proved using this embedding theorem. These embedding and relative decidability results allow us to reuse the standard pCTL-based probabilistic model checking algorithms to verify hierarchical randomized systems that can be described using HpCTL.
暂无评论