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

Probabilistic hyperproperties specify quantitative relations between theprobabilities of reaching different target sets of states from differentinitial sets of states. This class of behavioral properties is suitable forcapturing important security, privacy, and system-level requirements. Wepropose a new approach to solve the controller synthesis problem for Markovdecision processes (MDPs) and probabilistic hyperproperties. Our specificationlanguage builds on top of the logic HyperPCTL and enhances it with structuralconstraints over the synthesized controllers. Our approach starts from a familyof controllers represented symbolically and defined over the same copy of anMDP. We then introduce an abstraction refinement strategy that can relatemultiple computation trees and that we employ to prune the search spacedeductively. The experimental evaluation demonstrates that the proposedapproach considerably outperforms HyperProb, a state-of-the-art SMT-based modelchecking tool for HyperPCTL. Moreover, our approach is the first one that isable to effectively combine probabilistic hyperproperties with additionalintra-controller constraints (e.g. partial observability) as well asinter-controller constraints (e.g. agreements on a common action).

Deductive Controller Synthesis for Probabilistic Hyperproperties