Real Equation Systems with Alternating Fixed-points (full version with proofs)

TL;DR

This paper introduces Real Equation Systems (RES), extending Boolean Equation Systems to real numbers with nested fixed points, and provides a complete solving procedure applicable to probabilistic systems.

Contribution

It formalizes RES, proves they can be transformed into normal form, and develops a complete elimination-based solution method for RES.

Findings

RES can be rewritten into a normal form for easier solving

A complete elimination-based procedure for solving RES is developed

Application demonstrated in verifying probabilistic modal formulas

Abstract

We introduce the notion of a Real Equation System (RES), which lifts Boolean Equation Systems (BESs) to the domain of extended real numbers. Our RESs allow arbitrary nesting of least and greatest fixed-point operators. We show that each RES can be rewritten into an equivalent RES in normal form. These normal forms provide the basis for a complete procedure to solve RESs. This employs the elimination of the fixed-point variable at the left side of an equation from its right-hand side, combined with a technique often referred to as Gau{\ss}-elimination. We illustrate how this framework can be used to verify quantitative modal formulas with alternating fixed-point operators interpreted over probabilistic labelled transition systems.