检测连续随机逻辑与量子连续时间马尔可夫链。
摘要：验证量子系统在过去几十年中引起了很大的关注。本文研究了量子连续时间马尔可夫链（quantum CTMCs）的量化模型检查。量子CTMC的分支时间属性由连续随机逻辑（CSL）指定，该逻辑以验证实时系统（包括经典CTMCs）而闻名。检查CSL公式的核心在于解决多相直到公式。我们利用适当的投影、矩阵指数和确定性积分开发了一种代数方法，以符号化计算路径公式的概率测度。因此，CSL的可决定性得到了建立。为了高效，数值方法被纳入以确保时间复杂度在输入模型的编码大小中是多项式的，并且在输入公式的大小中是线性的。进一步提供了一个Apollonian网络的运行示例来演示我们的方法。
作者：Jingyi Mei, Ming Xu, Ji Guan, Yuxin Deng, Nengkun Yu
论文ID：2202.05412
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-07-03