通过固定延迟连续时间马尔可夫链中最优超时综合扩展PRISM
计算机科学中的逻辑
2016-03-11 v1 性能
摘要
我们提出了一种实用且吸引人的概率模型检测器PRISM的扩展，使其能够处理带回报的固定延迟连续时间马尔可夫链（fdCTMCs），其等价于确定与随机Petri网（DSPNs）。fdCTMCs在传统具有指数速率的转移之上，允许具有固定延迟（或超时）的转移。我们的扩展支持在到达给定目标状态集之前评估期望回报。主要贡献在于，将固定延迟视为参数，我们实现了一个综合算法，计算最小化期望回报的固定延迟的ε最优值。我们给出了该综合在实际例子上的性能评估。
引用
@article{arxiv.1603.03252,
title = {Extension of PRISM by Synthesis of Optimal Timeouts in Fixed-Delay CTMC},
author = {Ľuboš Korenčiak and Vojtěch Řehák and Adrian Farmadin},
journal= {arXiv preprint arXiv:1603.03252},
year = {2016}
}