Linear constraints in probabilistic model checking