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 Plus

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

Zendy Tools

Zendy Open

In this paper, we propose an efficient algorithm for the parameter synthesisof PLTL formulas with respect to parametric Markov chains. The PLTL formula istranslated to an almost fully partitioned B\"uchi automaton which is thencomposed with the parametric Markov chain. We then reduce the problem tosolving an optimisation problem, allowing to decide the satisfaction of theformula using an SMT solver. The algorithm works also for interval Markovchains. The complexity is linear in the size of the Markov chain, andexponential in the size of the formula. We provide a prototype and show theefficiency of our approach on a number of benchmarks.

An Efficient Synthesis Algorithm for Parametric Markov Chains Against Linear Time Properties