Model Checking Branching Time Properties for Incomplete Markov Chains

Abstract

In this work, we discuss a numerical model checking algorithm for analyzing incompletely specified models of stochastic systems, specifically, Discrete Time Markov Chains (DTMC). Models of a system could be incompletely specified for several reasons. For example, they could still be under development or, there could be some doubt about the correctness of some components. We restrict ourselves to cases where incompleteness can be captured by expanding the logic of atomic propositions to a three valued logic that includes an unknown truth value. We seek to answer meaningful model checking queries even in such circumstances. The approach we adopt in this paper is to develop the model checking algorithm from first principles. We develop a tool based on the algorithm and compare the performance of this approach with the indirect approach of invoking a binary model checker.