The toolset heavily relies on boolean equation systems, which are the workhorse

to solve modal formulas. Boolean equation systems only permit truth values as solutions for

variables. It would be nice to also extract quantitative information using modal formulas,

such as probabilities, durations, or yields. For this purpose it would be nice to have

real equation systems, i.e. equation systems where the fixed point variables represent

reals. In this talk I present how I look at them, and show a systematic way to solve

them manually. The work being presented is far from finished.