流体随机Petri网的行为等价关系
计算机科学中的逻辑
2017-06-09 v1
摘要
我们提出流体等价关系，用于在保持标记流体随机Petri网(LFSPNs)的离散与连续性质的同时，比较并约简其行为。我们定义了线性时间关系流体迹等价(fluid trace equivalence)及其分支时间对应物流体互模拟等价(fluid bisimulation equivalence)。这两种流体关系均考虑了LFSPNs行为的本质特征：功能活动、随机时序与流体流动。我们考虑了这样一类LFSPNs：其连续标记对离散标记无影响，且其离散部分是连续时间随机Petri网。LFSPNs离散部分的基础随机模型是连续时间马尔可夫链(CTMCs)。LFSPNs连续部分的性能分析通过关联的随机流体模型(SFMs)完成。我们证明了流体迹等价保持了每个特定长度的转移序列的平均潜在流体变化量。我们证明了流体互模拟等价保持了聚合概率函数：底层CTMC的平稳概率质量，以及关联SFM的平稳流体缓冲空概率、流体密度与分布。因此，该等价保证了大量离散与连续性能度量的一致性。随后，流体互模拟等价被用于通过商化离散可达图与底层CTMC来简化LFSPNs的定性与定量分析。为描述商化后的关联SFM，定义了概率函数的商。我们借助两种基于Hennessy-Milner逻辑(HML)的新型流体模态逻辑和，从逻辑上刻画了流体迹等价与互模拟等价。一个文档准备系统的应用示例展示了通过流体互模拟等价进行商化的行为分析。
引用
@article{arxiv.1706.02641,
title = {Behavioural equivalences for fluid stochastic Petri nets},
author = {Igor V. Tarasyuk and Peter Buchholz},
journal= {arXiv preprint arXiv:1706.02641},
year = {2017}
}