具有独立积的概率模态$\mu$-演算

概率模态$\mu$-演算是一种定点逻辑，旨在表达概率标记转移系统 (PLTS) 的性质。针对该逻辑已研究了两种等价语义，二者均为每个状态赋予区间 [0,1] 内的一个值，表示公式所表达的性质在该状态成立的概率。一种语义是指称语义，另一种是博弈语义，由双人随机奇偶博弈指定。概率模态$\mu$-演算的一个不足之处是缺乏编码其他重要 PLTS 时序逻辑（如概率计算树逻辑 PCTL）所需的表达能力。为解决这一局限，我们扩展了该逻辑，引入了一对新算子：独立积和独立余积。所得逻辑称为具有独立积的概率模态$\mu$-演算，能够编码许多感兴趣的性质，并涵盖了 PCTL 的定性片段。本文的主要贡献是为这一扩展的概率$\mu$-演算定义了适当的博弈语义。这依赖于定义一类新的博弈，该类博弈通过允许一局博弈分裂为并发子博弈且各自独立演化，从而推广了标准的双人随机（奇偶）博弈。我们的主要技术结果是证明了两种语义的等价性。该证明在扩展了不可数基数上 Martin 公理的 ZFC 集合论中进行。