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/

Zendy Pro

Presents the zaia usage as premium feature

ZAIA

Presents AI Discovery search usage as a premium feature

AI Discovery

Presents AI Discovery explain and summary usage as a premium feature

Content Analysis

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Presents the pdf analysis as premium feature

PDF Analysis

1500 Top-up

3000 Top-up

Zendy Basic

2500 Top-up

Zendy Unlimited

Presents the access of premium content as premium feature

Premium Content

The coalgebraic μ-calculus is a generic framework for fixpoint logics with varying branching types that subsumes, besides the standard relational μ-calculus, such diverse logics as the graded μ-calculus, the monotone μ-calculus, the probabilistic μ-calculus, and the alternating-time μ-calculus. In the present work, we give a local model checking algorithm for the coalgebraic μ-calculus using a coalgebraic variant of parity games that runs, under mild assumptions on the complexity of the so-called one-step satisfaction problem, in time p where p is a polynomial in the formula and model size and where k is the alternation depth of the formula. We show moreover that under the same assumptions, the model checking problem is in NP ∩ coNP, improving the complexity in all mentioned non-relational cases. If one-step satisfaction can be solved by means of small finite games, we moreover obtain standard parity games, ensuring quasi-polynomial run time. This applies in particular to the monotone μ-calculus, the alternating-time μ-calculus, and the graded μ-calculus with grades coded in unary. 2012 ACM Subject Classification Theory of computation → Modal and temporal logics; Theory of computation → Verification by model checking

Game-Based Local Model Checking for the Coalgebraic mu-Calculus