随机进程代数IMCs的性能评价

摘要

将马尔可夫路径概率计算方法推广到随机进程代数:交互式马尔科夫链(IMCs)模型上.由于IMCs中存在动作转移和概率转移,两种不同性质的转移破坏了系统的稳定性,因此在IMCs的性能刻画中,去掉系统的稳态性刻画,给出动作和概率转移共存的IMCs模型的路径定义和基于概率转移率的路径转移发生的概率计算方法,解决了Until算子的描述.使用基于动作的逻辑aCSL给出IMCs的性能评价.证明该方法的正确性,它是纯马尔可夫链模型中性能评价方法的扩展.