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

Couplings are a powerful mathematical tool for reasoning about pairs ofprobabilistic processes. Recent developments in formal verification identify aclose connection between couplings and pRHL, a relational program logicmotivated by applications to provable security, enabling formal construction ofcouplings from the probability theory literature. However, existing work usingpRHL merely shows existence of a coupling and does not give a way to provequantitative properties about the coupling, which are need to reason aboutmixing and convergence of probabilistic processes. Furthermore, pRHL isinherently incomplete, and is not able to capture some advanced forms ofcouplings such as shift couplings. We address both problems as follows.  First, we define an extension of pRHL, called xpRHL, which explicitlyconstructs the coupling in a pRHL derivation in the form of a probabilisticproduct program that simulates two correlated runs of the original program.Existing verification tools for probabilistic programs can then be directlyapplied to the probabilistic product to prove quantitative properties of thecoupling. Second, we equip pRHL with a new rule for while loops, wherereasoning can freely mix synchronized and unsynchronized loop iterations. Ourproof rule can capture examples of shift couplings, and the logic is relativelycomplete for deterministic programs.  We show soundness of xpRHL and use it to analyze two classes of examples.First, we verify rapid mixing using different tools from coupling: standardcoupling, shift coupling, and path coupling, a compositional principle forcombining local couplings into a global coupling. Second, we verify(approximate) equivalence between a source and an optimized program for severalinstances of loop optimizations from the literature.

Coupling proofs are probabilistic product programs