Model Checking the Quantitative mu-Calculus on Infinite Transition Systems

We consider the model-checking problem for a quantitative
extension of the modal mu-calculus on two classes of infinite
quantitative transition systems. The first class, initialized linear
hybrid systems, is motivated by verification of systems which
exhibit continuous dynamics. We show that the value of a formula
of the quantitative mu-calculus can be approximated with arbitrary
precision on initialized linear hybrid systems. The other class,
increasing tree rewriting systems, is motivated by efforts to allow
counting formulas in discrete verification. On such systems, we
show that the value of a quantitative formula can be computed
exactly. For both these classes of systems, the problem in the end
reduces to solving a new form of parity games with counters.