Continuous-time Markov chains (CTMCs) have received considerable attentions in network performance analysis, model checking, and system biology. In this paper, we consider the model-checking problem of continuous-time Markov chains with respect to Conditional Continuous Stochastic Logic (CCSL). CCSL extends the logic CSL introduced by Aziz et al. with a conditional probabilistic operator, which allows us to express a richer class of properties for CTMCs. Based on a parameterized product construction, we propose an approximate model checking algorithm with complexity analysis. After that, we present CCMC (Conditional CSL Model Checker), a model checker for CTMCs with respect to formulas specified in CCSL. Existing CTMC model checkers such as PRISM or MRMC handle only binary CSL until path formulas. CCMC is the first tool that supports algorithms for analyzing nested until path formulas. Moreover, CCMC supports conditional CSL formulas. Some case studies are given showing the efficiency of the tool.
修改评论