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.

翻译：我们引入实数值方程组（Real Equation System, RES）的概念，将布尔方程组（BES）扩展到扩展实数域。RES允许最小与最大不动点算子的任意嵌套。我们证明每个RES均可重写为等价的正规形RES。这些正规形为求解RES的完整过程奠定了理论基础，该过程通过消除方程左侧的不动点变量（从右侧表达式中消除），并结合一种常被称为高斯消元法的技术实现。我们进一步阐释如何利用该框架验证概率标记转移系统上带有交替不动点算子的定量模态公式。