AI 中文总结
本文利用随机图论创建大型标记转移系统概率模型，结合经验数据赋予现实参数值，分析其在LTL和CTL下渐近行为，得出收敛律或0-1律，讨论确定极限的理论复杂度并给出算法，为理解LTS行为及随机图论在模型检查中的应用提供基础。
AI 中文摘要
模型检查是对标记转移系统（LTS）中（用某些模态逻辑指定的）属性进行自动验证，是确保软件系统按预期运行的重要工具。软件状态空间呈指数增长，需要启发式方法确保模型检查在实际应用中可行，这又需要深入了解LTS的典型行为。本文利用随机图论创建大型LTS的概率模型，结合模型检查竞赛的经验数据赋予模型现实参数值。接着分析该模型在模型检查中常用的两种模态逻辑LTL和CTL下的渐近行为，表明随着规模趋于无穷，根据具体模型要么有收敛律（每个公式成立的概率收敛到一个极限）要么有0-1律（该极限为0或1），还讨论了确定这些极限的理论复杂度并给出算法。这些结果是深入理论理解典型LTS行为的起点，凸显了随机图论在模型检查中的应用前景。
英文摘要
Model checking is the automated verification of properties (specified in some modal logic) in labeled transition systems (LTSs); it is an essential tool in ensuring software systems function as intended. State spaces of software grow exponentially, and heuristics are needed to ensure model checking remains feasible in real-world applications. Heuristics, in turn, require a good understanding on the typical behaviour of LTSs. In this paper, we use random graph theory to create a probabilistic model of large LTSs. From a theoretical analysis of the creation of large LTSs, backed by empirical data from the Model Checking Contest, we endow these models with realistic parameter values. Then, we analyze the asymptotic behaviour of this model under LTL and CTL, two modal logics popular in model checking. We show that, depending on the precise model, as the size grows to infinity we either have a convergence law (for every formula, the probability that it holds converges to a limit) or a 0-1 law (...and this limit is 0 or 1). We also discuss the theoretical complexity of determining these limits, and give algorithms for doing so. These results are the starting point towards a deep theoretical understanding of typical LTS behaviour, and highlight the promising applicability of random graph theory to model checking. \keywords{Model checking \and Random graphs \and 0-1 laws
