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 Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Properties of Kripke structures can be expressed by formulas of the modal µ-calculus. Despite its strong expressive power, the validity problem of the modal µ-calculus is decidable, and so are some of its variants enriched by inverse programs, graded modalities, and nominals. In this study, we show that the pre- and post-conditions of transformations of Kripke structures, such as addition/deletion of states and edges, can be expressed using variants of the modal µ-calculus. Combined with decision procedures we have developed for those variants, the properties of sequences of transformations on Kripke structures can be deduced. We show that these techniques can be used to verify the properties of pointer-manipulating programs.

Pre- and Post-Conditions Expressed in Variants of the Modal .MU.-Calculus