论文标题
用于验证连续时间马尔可夫链的概率逻辑
A Probabilistic Logic for Verifying Continuous-time Markov Chains
论文作者
论文摘要
连续时间马尔可夫链（CTMC）执行是状态上连续的概率分布类别。本文提出了一种概率线性时间逻辑，即连续时间线性逻辑（CLL），以理解CTMC的概率分布执行。我们在概率分布空间上定义了CLL的语法。 CLL的语法包括到公式的多相时间，CLL的语义允许时间重置以研究相对时间的特性。我们为CLL公式提供了相应的模型检查算法。模型检查算法的正确性取决于Schanuel的猜想，这是先验数理论中的一个核心开放问题。此外，我们提供了CTMC的运行示例，以说明我们的方法。
A continuous-time Markov chain (CTMC) execution is a continuous class of probability distributions over states. This paper proposes a probabilistic linear-time temporal logic, namely continuous-time linear logic (CLL), to reason about the probability distribution execution of CTMCs. We define the syntax of CLL on the space of probability distributions. The syntax of CLL includes multiphase timed until formulas, and the semantics of CLL allows time reset to study relatively temporal properties. We derive a corresponding model-checking algorithm for CLL formulas. The correctness of the model-checking algorithm depends on Schanuel's conjecture, a central open problem in transcendental number theory. Furthermore, we provide a running example of CTMCs to illustrate our method.
