Upper approximating probabilities of convergence in probabilistic coherence spaces

Ranking and Repulsing Supermartingales for Reachability in Probabilistic Programs

Computing reachability probabilities is a fundamental problem in the analysis of probabilistic programs. This paper aims at a comprehensive and comparative account on various martingale-based methods for over- and under-approximating reachability probabilities. Based on the existing works that stretch across different communities (formal verification, control theory, etc.), we offer a unifying account. In particular, we emphasize the role of order-theoretic fixed points---a classic topic in computer science---in the analysis of probabilistic programs. This leads us to two new martingale-based …

Probabilistic Stable Functions on Discrete Cones are Power Series (long version)

We study the category Cstabm of measurable cones and measurable stable functions, which is a denotational model of an higher-order language with continuous probabilities and full recursion. We look at Cstabm as a model for discrete probabilities, by showing the existence of a cartesian closed, full and faithful functor which embeds probabilistic coherence spaces (a fully abstract denotational model of an higher-order language with full recursion and discrete probabilities) into Cstabm. The proof is based on a generalization of Bernstein's theorem from real analysis allowing to see stable funct…

通过哈希和随机化近似求解随机多目标优化中的帕累托前沿

Approximating Pareto Frontiers in Stochastic Multi-Objective Optimization via Hashing and Randomization

本文提出XOR-SMOO算法，通过多项式对数次调用SAT oracle，在概率1-δ下获得γ-近似帕累托前沿，提升随机多目标优化求解的实用性和可靠性。