一句话：提出基于结构操作语义的模态公式分解方法，并为概率互模拟与相似性建立同余格式。
该论文研究非确定性概率进程上模态公式的分解问题，目标是将进程满足某公式的问题归约为其子进程满足由分解得到的公式。为刻画进程的概率行为及相应公式的分解，作者引入一种类SOS机制，用于规定开放分布项的行为。基于该分解方法，论文给出了概率互模拟、就绪相似性和相似性的（前）同余格式。工作以结构操作语义为统一框架，将模态逻辑分解与概率进程等价关系的形式化条件联系起来，为概率并发系统的组合式推理提供语义基础。
We propose a method for the decomposition of modal formulae on processes with nondeterminism and probability with respect to Structural Operational Semantics. The purpose is to reduce the satisfaction problem of a formula for a process to verifying whether its subprocesses satisfy certain formulae obtained from the decomposition. To deal with the probabilistic behavior of processes, and thus with the decomposition of formulae characterizing it, we introduce a SOS-like machinery allowing for the specification of the behavior of open distribution terms. By our decomposition, we obtain (pre)congruence formats for probabilistic bisimilarity, ready similarity and similarity.
@article{paperbot397,
title = {SOS-based Modal Decomposition on Nondeterministic Probabilistic Processes},
author = {Valentina Castiglioni and Daniel Gebler and Simone Tini},
journal = {Logical Methods in Computer Science},
volume = {Volume 14, Issue 2},
year = {2018},
doi = {10.23638/lmcs-14(2:18)2018}
}