基于SOS的非确定性概率过程的模态分解
摘要：用于关于具有非确定性和概率的进程上的模态公式分解的方法。目的是将对进程公式的满足问题减少到验证其子进程是否满足从分解中获得的特定公式。为了处理进程的概率行为，并因此处理表征它的公式的分解，我们引入了一个类似SOS的机制，允许对开放分布项的行为进行规定。通过我们的分解，我们获得了与概率双最大性、就绪相似性和相似性有关的(pre)congruence格式。
作者：Valentina Castiglioni, Daniel Gebler and Simone Tini
论文ID：1701.08330
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22