Jan Friso Groote: Numerically solving Real Equation Systems


Event Details


The quantitative modal mu-calculus is equal to the modal mu-calculus except that formulas yield real values including (-)infinity instead of true or false. Quantitative modal formulas can be translated to parameterised real equation systems (PRESs), and subsequently to real equation systems (RESs), which is quite similar as translating to PBESs and BESs in case of ordinary formula.

Gauss elimination is a complete method to solve RESs, but it is so inefficient that only small RESs can be solved. There is a numerical algorithm, which will be explained, which appears very efficient. However, the algorithm cannot deal with situations where solutions go to infinity.

During this presentation I will elaborate on this and indicate where I got stuck.