文献类型：期刊文献

英文题名：Logical characterization of branching bisimilarity over random processes

作者：Xu, Xian[1];Zhang, Wenbo[2]

机构：[1]East China Univ Sci & Technol, Shanghai, Peoples R China;[2]Shanghai Ocean Univ, Shanghai, Peoples R China

年份：2026

卷号：191

外文期刊名：INFORMATION PROCESSING LETTERS

收录：;EI(收录号：20253018832643);WOS:【SCI-EXPANDED(收录号:WOS:001540561600001)】；

基金：This research is supported by National Natural Science Foundation of China (61872142, 62072299, 62102243) , Shanghai Sailing Program (21YF1417000) , and Shanghai "Science and Technology Innovation Action Plan" (24BC3200500, 24BC3200300) .

语种：英文

外文关键词：Logical characterization; Probabilistic processes; Uniformly randomized; CCS; Branching bisimulation

摘要：Quantitative aspects like probabilities play an important role in concurrent processes. Providing a (modal) logic for a randomized concurrency model can augment the toolbox of analyzing probabilistic processes, and thus is a frequent topic in the field. In this paper, we are interested in logically characterizing uniformly randomized processes, whose semantical behavior is defined in a model-independent manner. Specifically, we present two modal logics for the uniformly randomized version of finite-state CCS (RCCSfsfor short). Our logics extend the Hennessy-Milner logic, and one of them is equipped with the mu operator. Indeed, we prove that both logics characterize the branching bisimilarity for RCCSfs, i.e., two RCCSfsprocesses are branching bisimilar if and only if they are logically equivalent. To facilitate the proof, we also develop for RCCSfsan up-to proof method, which may be of independent interest.