凸抽象概率互模拟的 SOS 规则格式

$nt \mu f\theta / nt\mu x\theta$ 格式的概率转移系统规约（Probabilistic transition system specifications, PTSSs）为同时表现出概率和非确定性行为的 Segala 型系统提供了结构化操作语义，并保证互模拟性是所有以该格式定义的操作符的同余关系。从 $nt \mu f\theta / nt\mu x\theta$ 格式出发，我们获得了保证三种更粗的互模拟等价为同余关系的受限格式。我们关注于： Segala 考虑组合转移的互模拟变体，我们在此称之为“凸互模拟”； 考虑在通常剥离概率转移系统（转换为标号转移系统）上的 Park & Milner 互模拟所得到的互模拟等价，我们在此称之为“概率抹除互模拟”； “概率抽象互模拟”，它像互模拟一样保留分布的结构，但忽略概率值。此外，我们比较了这些互模拟等价，并为它们各自提供了逻辑刻画。