Interval Temporal Logic Model Checking Based on Track Bisimilarity and Prefix Sampling