Markov 自动机的定时与长期目标分析
计算机科学中的逻辑
2015-07-01 v2 形式语言与自动机理论
摘要
Markov 自动机（MAs）通过引入随机延迟和概率分支扩展了标号迁移系统。动作标号迁移是瞬时的，并产生一个状态上的分布；而定时迁移则施加一个由指数分布控制的随机延迟。因此，MAs 是连续时间 Markov 链的非确定性变体。MAs 具有组合性，并用于为工程框架提供语义，例如（动态）故障树、（广义）随机 Petri 网以及架构分析与设计语言（AADL）。本文考虑 MAs 的定量分析。我们考虑三个目标：期望时间、长期平均和定时（区间）可达性。期望时间目标侧重于确定到达一组状态的最小（或最大）期望时间。长期目标确定在无限时间范围内处于一组状态的时间比例。定时可达性目标涉及计算在给定时间区间内到达一组状态的概率。本文给出了算法的基础、细节及其正确性证明。我们报告了使用 MAPA 建模语言驱动的算法原型工具实现所进行的若干案例研究，以高效生成 MAs。
关键词
引用
@article{arxiv.1407.7356,
title = {Analysis of Timed and Long-Run Objectives for Markov Automata},
author = {Dennis Guck and Hassan Hatefi and Holger Hermanns and Joost-Pieter Katoen and Mark Timmer},
journal= {arXiv preprint arXiv:1407.7356},
year = {2015}
}
备注
arXiv admin note: substantial text overlap with arXiv:1305.7050