English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

We introduce the notion of a Real Equation System (RES), which lifts BooleanEquation Systems (BESs) to the domain of extended real numbers. Our RESs allowarbitrary nesting of least and greatest fixed-point operators. We show thateach RES can be rewritten into an equivalent RES in normal form. These normalforms provide the basis for a complete procedure to solve RESs. This employsthe elimination of the fixed-point variable at the left side of an equationfrom its right-hand side, combined with a technique often referred to asGau{\ss}-elimination. We illustrate how this framework can be used to verifyquantitative modal formulas with alternating fixed-point operators interpretedover probabilistic labelled transition systems.

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