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

Variability models allow effective building of many custom model variants forvarious configurations. Lifted model checking for a variability model iscapable of verifying all its variants simultaneously in a single run byexploiting the similarities between the variants. The computational cost oflifted model checking still greatly depends on the number of variants (the sizeof configuration space), which is often huge.  One of the most promising approaches to fighting the configuration spaceexplosion problem in lifted model checking are variability abstractions. Inthis work, we define a novel game-based approach for variability-specificabstraction and refinement for lifted model checking of the full CTL,interpreted over 3-valued semantics. We propose a direct algorithm for solvinga 3-valued (abstract) lifted model checking game. In case the result of modelchecking an abstract variability model is indefinite, we suggest a new notionof refinement, which eliminates indefinite results. This provides an iterativeincremental variability-specific abstraction and refinement framework, whererefinement is applied only where indefinite results exist and definite resultsfrom previous iterations are reused.

Variability Abstraction and Refinement for Game-based Lifted Model Checking of full CTL (Extended Version)