引入异步性到概率超属性
摘要：概率超属性表达了具有不确定行为的系统的不同执行之间的概率关系。HyperPCTL允许形式化这样的属性，其中对概率调度程序的量化解决了潜在的非确定性。在本文中，我们提出了一个称为AHyperPCTL的扩展，以引入观察执行之间的异步性，通过对口吃时间食品进行量化，它可以随机决定延迟调度者决策。据我们所知，这是一个概率分支时间超逻辑的第一个异步扩展。我们展示了AHyperPCTL可以表达有趣的信息流安全策略，并提出了一个可判定片段的模型检验算法。
作者：Lina Gerlach (1), Oyendrila Dobe (2), Erika ''Abrah''am (1), Ezio Bartocci (3), Borzoo Bonakdarpour (2) ((1) RWTH Aachen University, Aachen, Germany, (2) Michigan State University, East Lansing, MI, USA, (3) Technische Universit"at Wien, Vienna, Austria)
论文ID：2307.05282
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-07-12