概率安全或活性
计算机科学中的逻辑
2014-05-19 v2
摘要
本文提出了针对全概率系统的安全性和活性性质的形式化刻画，遵循 Alpern 和 Schneider 的方法。与经典设定一样，确立了任何（概率树）性质均等价于安全性性质与活性性质的合取。提供了一种简单算法，用于获得扁平概率计算树逻辑 (PCTL) 的这种性质分解。识别出了一个 PCTL 的安全片段，该片段提供了安全性性质的可靠且完备的刻画。对于活性性质，我们提供了两个 PCTL 片段，一个是可靠的，另一个是完备的。我们表明，安全性性质仅具有有限反例，而活性性质则没有。我们将针对定性性质的刻画与 Manolios 和 Trefler 针对分支时间性质的刻画进行了比较，并提出了可靠且完备的 PCTL 片段，用于刻画 Sistla 提出的强安全性和绝对活性概念。
引用
@article{arxiv.1401.7171,
title = {Probably Safe or Live},
author = {Joost-Pieter Katoen and Lei Song and Lijun Zhang},
journal= {arXiv preprint arXiv:1401.7171},
year = {2014}
}