Model Checking the Quantitative mu-Calculus on Infinite Transition Systems

Prelegent(ci)

Łukasz Kaiser

Afiliacja

LIAFA, Paris

Termin

26 października 2011 14:15

Pokój

p. 5870

Seminarium

Seminarium „Teoria automatów”

---

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.

---