PASS

PASS is an analysis tool for infinite-state probabilistic models. It is based on predicate abstraction and automatic abstraction refinement. Models are specified in a variant of the PRISM language. PASS computes the probability of reaching a set of goal states specified by the user. PASS has two sisters, PARAM and INFAMY, that accept virtually the same language, but have different strengths.