The verification of linear systems has been extensively studied through reachability analysis to determine the set of states reachable from initial conditions. While traditional methods focus on qualitative safety checks, this work extends verification to quantitative analysis using probabilistic star sets (ProbStars), which incorporate Gaussian-distributed variables for probabilistic reachability. To handle large-scale linear systems, we use Krylov subspace methods (e.g., Arnoldi and Lanczos iterations), incorporating numerical simulation for efficiently approximating the exponential matrix to get simulation equivalent reachable sets. We also introduce a verification framework based on ProbStar Temporal Logic (ProbStarTL) for specifying and analyzing complex temporal properties. Experiments on benchmarks up to 10,000 dimensions show the scalability and effectiveness of our approach.