2026-07-19T20:52:18Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:19022 2024-03-06T11:03:18Z ddc:004 open_access

Real Equation Systems with Alternating Fixed-Points Groote, Jan Friso Willemse, Tim A. C. Real Equation System Solution method Gauß-elimination Model checking Quantitative modal mu-calculus 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ß-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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Jan Friso Groote and Tim A. C. Willemse 2023 Is Part Of LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2023.28 urn:nbn:de:0030-drops-190225 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.28 eng https://creativecommons.org/licenses/by/4.0/legalcode