We introduce the concept of *Runtime Verification with State
Estimation* and show how this concept can be applied to estimate the
probability that a temporal property is satisfied by a run of a
program when monitoring overhead is reduced by sampling. In such
situations, there may be *gaps* in the observed program
executions, thus making accurate estimation challenging. To deal with
the effects of sampling on runtime verification, we view event
sequences as observation sequences of a Hidden Markov Model (HMM), use
an HMM model of the monitored program to "fill in" sampling-induced
gaps in observation sequences, and extend the classic forward
algorithm for HMM state estimation (determine the probability of a
state sequence, given an observation sequence) to compute the
probability that the property is satisfied by an execution of the program.
To validate our approach, we present a case study based on the mission
software for a Mars rover. The results of our case study demonstrate
high prediction accuracy for the probabilities computed by our
algorithm. They also show that our technique is much more accurate
than simply evaluating the temporal property on the given observation
sequences, ignoring the gaps.