论文标题
马尔可夫模型中的参数合成：温和的调查
Parameter Synthesis in Markov Models: A Gentle Survey
论文作者
论文摘要
本文调查了参数马尔可夫模型的分析，其过渡在有限的参数集上标记了函数。这些模型是无数概率模型的符号表示，每个模型都通过实例化参数而获得。我们考虑给定逻辑规范$φ$的各种分析问题：参数值的给定区域内的所有参数实例是否满足$φ$？？，哪些实例满足$φ$，哪些实例不满意？我们解决了理论上的复杂性结果，并描述了最新算法的主要思想，这些算法在过去的十年中建立了令人印象深刻的飞跃，从而实现了对具有数百万个州和数千个参数的模型的完全自动化分析。
This paper surveys the analysis of parametric Markov models whose transitions are labelled with functions over a finite set of parameters. These models are symbolic representations of uncountable many concrete probabilistic models, each obtained by instantiating the parameters. We consider various analysis problems for a given logical specification $φ$: do all parameter instantiations within a given region of parameter values satisfy $φ$?, which instantiations satisfy $φ$ and which ones do not?, and how can all such instantiations be characterised, either exactly or approximately? We address theoretical complexity results and describe the main ideas underlying state-of-the-art algorithms that established an impressive leap over the last decade enabling the fully automated analysis of models with millions of states and thousands of parameters.
