  We investigate the decidability of model-checking logics of time, knowledge
and probability, with respect to two epistemic semantics: the clock and
synchronous perfect recall semantics in partially observed discrete-time Markov
chains. Decidability results are known for certain restricted logics with
respect to these semantics, subject to a variety of restrictions that are
either unexplained or involve a longstanding unsolved mathematical problem. We
show that mild generalizations of the known decidable cases suffice to render
the model checking problem definitively undecidable. In particular, for a
synchronous perfect recall, a generalization from temporal operators with
finite reach to operators with infinite reach renders model checking
undecidable. The case of the clock semantics is closely related to a monadic
second order logic of time and probability that is known to be decidable,
except on a set of measure zero. We show that two distinct extensions of this
logic make model checking undecidable. One of these involves polynomial
combinations of probability terms, the other involves monadic second order
quantification into the scope of probability operators. These results explain
some of the restrictions in previous work.
