马尔可夫种群模型的CSL模型检验
Model Checking CSL for Markov Population Models
AI总结：
针对无限状态连续时间马尔可夫链的马尔可夫种群模型，提出了一种完整的连续随机逻辑（CSL）模型检验算法，能够有效验证概率可达性、生存性、振荡等生物系统关键性质。
摘要：
马尔可夫种群模型（MPMs）是计算生物学及相关领域中广泛使用的建模形式。MPM的语义是无限状态的连续时间马尔可夫链。在本文中，我们使用已建立的连续随机逻辑（CSL）来表达马尔可夫种群模型的性质。这使我们能够表达生物系统的重要度量，例如概率可达性、生存性、振荡、吸引子区域之间的切换时间等。由于状态空间无限，现有的分析技术仅适用于非常受限的CSL性质子集。我们提出了一种针对MPM的CSL模型检验的完整算法，并提供了实验证据表明我们的方法是有效的。
英文摘要：
Markov population models (MPMs) are a widely used modelling formalism in the area of computational biology and related areas. The semantics of a MPM is an infinite-state continuous-time Markov chain. In this paper, we use the established continuous stochastic logic (CSL) to express properties of Markov population models. This allows us to express important measures of biological systems, such as probabilistic reachability, survivability, oscillations, switching times between attractor regions, and various others. Because of the infinite state space, available analysis techniques only apply to a very restricted subset of CSL properties. We present a full algorithm for model checking CSL for MPMs, and provide experimental evidence showing that our method is effective.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
