  We consider the problem of monitoring a Linear Time Logic (LTL) specification
that is defined on infinite paths, over finite traces. For example, we may need
to draw a verdict on whether the system satisfies or violates the property "p
holds infinitely often." The problem is that there is always a continuation of
a finite trace that satisfies the property and a different continuation that
violates it.
  We propose a two-step approach to address this problem. First, we introduce a
counting semantics that computes the number of steps to witness the
satisfaction or violation of a formula for each position in the trace. Second,
we use this information to make a prediction on inconclusive suffixes. In
particular, we consider a good suffix to be one that is shorter than the
longest witness for a satisfaction, and a bad suffix to be shorter than or
equal to the longest witness for a violation. Based on this assumption, we
provide a verdict assessing whether a continuation of the execution on the same
system will presumably satisfy or violate the property.
