交替固定点的实数方程系统（具有证明的完整版本）
摘要：实数方程系统的概念（RES）将布尔方程系统（BESs）提升到扩展实数域。我们的RES允许任意嵌套的最小值和最大值不动点运算符。我们展示每个RES都可以重写成等价的正规形式RES。这些正规形式为解决RES提供了完整的过程。该过程利用将方程的左侧的不动点变量在其右侧消除的技术，结合一种通常称为高斯消元的技术。我们说明了如何利用这个框架来验证在概率标记转换系统上解释的具有交替不动点运算符的定量模态公式。
作者：Jan Friso Groote and Tim A.C. Willemse
论文ID：2307.07455
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-07-17