马尔可夫链上双相似距离的完整定量演绎系统

The Zhou Ordinal of Labelled Markov Processes over Separable Spaces

There exist two notions of equivalence of behavior between states of a Labelled Markov Process (LMP): state bisimilarity and event bisimilarity. The first one can be considered as an appropriate generalization to continuous spaces of Larsen and Skou's probabilistic bisimilarity, while the second one is characterized by a natural logic. C. Zhou expressed state bisimilarity as the greatest fixed point of an operator $\mathcal{O}$, and thus introduced an ordinal measure of the discrepancy between it and event bisimilarity. We call this ordinal the "Zhou ordinal" of $\mathbb{S}$, $\mathfrak{Z}(\ma…

On-the-Fly Computation of Bisimilarity Distances

We propose a distance between continuous-time Markov chains (CTMCs) and study the problem of computing it by comparing three different algorithmic methodologies: iterative, linear program, and on-the-fly. In a work presented at FoSSaCS'12, Chen et al. characterized the bisimilarity distance of Desharnais et al. between discrete-time Markov chains as an optimal solution of a linear program that can be solved by using the ellipsoid method. Inspired by their result, we propose a novel linear program characterization to compute the distance in the continuous-time setting. Differently from previous…

On Natural Deduction for Herbrand Constructive Logics II: Curry-Howard Correspondence for Markov's Principle in First-Order Logic and Arithmetic

Intuitionistic first-order logic extended with a restricted form of Markov's principle is constructive and admits a Curry-Howard correspondence, as shown by Herbelin. We provide a simpler proof of that result and then we study intuitionistic first-order logic extended with unrestricted Markov's principle. Starting from classical natural deduction, we restrict the excluded middle and we obtain a natural deduction system and a parallel Curry-Howard isomorphism for the logic. We show that proof terms for existentially quantified formulas reduce to a list of individual terms representing all possi…

Bisimilarity Distances for Approximate Differential Privacy

Differential privacy is a widely studied notion of privacy for various models of computation. Technically, it is based on measuring differences between probability distributions. We study $ε,δ$-differential privacy in the setting of labelled Markov chains. While the exact differences relevant to $ε,δ$-differential privacy are not computable in this framework, we propose a computable bisimilarity distance that yields a sound technique for measuring $δ$, the parameter that quantifies deviation from pure differential privacy. We show this bisimilarity distance is always rational, the associated t…

概率互模拟距离的连续性

On the Continuity of the Probabilistic Bisimilarity Distance

本文证明鲁棒概率互拟是概率互拟距离在零距离处连续性的充要条件，并扩展到非互拟状态对以刻画连续性，提出多项式时间判定算法。

Bisimulation of Labelled State-to-Function Transition Systems Coalgebraically

Labeled state-to-function transition systems, FuTS for short, are characterized by transitions which relate states to functions of states over general semirings, equipped with a rich set of higher-order operators. As such, FuTS constitute a convenient modeling instrument to deal with process languages and their quantitative extensions in particular. In this paper, the notion of bisimulation induced by a FuTS is addressed from a coalgebraic point of view. A correspondence result is established stating that FuTS-bisimilarity coincides with behavioural equivalence of the associated functor. As ge…

带标记马尔可夫链中的扰动等价性

Perturbation equivalence in labelled Markov chains

针对转移概率不确定的带标记马尔可夫链，提出普遍与存在扰动等价性，证明状态情形可多项式时间判定，分布情形分别达NL与NP完全，并实现鲁棒模型缩减算法。

Continuous Markovian Logics - Axiomatization and Quantified Metatheory

Continuous Markovian Logic (CML) is a multimodal logic that expresses quantitative and qualitative properties of continuous-time labelled Markov processes with arbitrary (analytic) state-spaces, henceforth called continuous Markov processes (CMPs). The modalities of CML evaluate the rates of the exponentially distributed random variables that characterize the duration of the labeled transitions of a CMP. In this paper we present weak and strong complete axiomatizations for CML and prove a series of metaproperties, including the finite model property and the construction of canonical models. CM…

为行为距离的下界构造见证

Constructing Witnesses for Lower Bounds on Behavioural Distances

本文研究带标 Markov 链行为距离的下界问题，提出了一种归纳推导系统以证明状态间距离至少为某值，并建立了该系统与定量语义模态逻辑公式的构造性对应关系，能生成更小的见证公式。

带标记马尔可夫过程的半拉回

Semipullbacks of labelled Markov processes

本文扩展了带标记马尔可夫过程在解析Borel空间上行为等价与互模拟一致的结果，利用Strassen定理将其推广到普遍可测子集空间，并证明所得半拉回图可交换。