Model Checking CTMDP against Temporal Specifications Characterized by Regular Expressions

Continuous time Markov decision process (CTMDP) permits probabilistic and nondeterministic choices, and can be employed as the semantics model of some high-level formalisms. This paper introduces a new action-based as well as state-based temporal logic as CSRL, which can be viewed as an extension of a CSL with path-based probability operator, and includes three additional reward operators in comparison with as CSL to reason about reward structures. The path-based properties are characterized by regular expressions over actions and state formulas. Moreover, as CSRL provides more abundant means to characterize reward-based properties, and this is very useful in performance evaluation about power, bandwidth, etc. We then discuss the model checking procedure under deterministic and nondeterministic policies.