Real Equation Systems with Alternating Fixed-points (full version with proofs)
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.
Cite
@article{arxiv.2307.07455,
title = {Real Equation Systems with Alternating Fixed-points (full version with proofs)},
author = {Jan Friso Groote and Tim A. C. Willemse},
journal= {arXiv preprint arXiv:2307.07455},
year = {2023}
}
Comments
25 pages. 2 Figures. 1 Table. This paper is published at Concur 2023, September 2023, Antwerp, Belgium