Characterization and computation of infinite-horizon specifications over Markov processes (Q386604)

This paper considers the verification of probabilistic CTL (PCTL, for short) formulas on discrete-time Markov processes that have uncountable state spaces. Two relevant questions are considered: how to verify nested PCTL formulas, and how to verify infinite-horizon PCTL formulas. The first question is addressed by considering sub- and super-satisfaction sets for PCTL formulas (i.e., subsets and supersets of the set of states satisfying a given PCTL formula) and proving that these sets for nested sub-formulas propagate to such sets for the overall PCTL formula. These results rely on monotonicity properties of corresponding value functions. For the latter question, the authors show that existing sufficient conditions for the existence of a unique solution of a Bellman equation are only satisfied if the solution is ``trivial''. For Markov processes exhibiting some continuity property, a necessary and sufficient condition is provided. In particular, the paper discussed the relationship between the existence of absorbing sets over the state space and the existence of a unique solution.