Model checking aims to give exact answers to queries about a model's execution but, in probabilistic model checking, ensuring exact answers might be difficult. Numerical iterative methods are heavily used in probabilistic model checking and errors caused by truncation may affect correctness. To tackle truncation errors, we investigate the bounding semantics of continuous stochastic logic for Markov chains. We first focus on analyzing truncation errors for model-checking the time-bounded or unbounded Until operator and propose new algorithms to generate lower and upper bounds. Then, we study the bounding semantics for a subset of nested CSL formulas. We demonstrate result on two models.
展开▼
