论文标题
使用HyperPCTL*对多代理系统检查贝叶斯统计模型*
Bayesian Statistical Model Checking for Multi-agent Systems using HyperPCTL*
论文作者
论文摘要
在本文中，我们提出了一种用于在离散时间马尔可夫链（DTMC）上指定的概率超普通统计模型检查（SMC）的贝叶斯方法。尽管使用顺序概率比测试（SPRT）的HyperPCTL*的SMC曾经探索过，但我们基于贝叶斯假设检验开发了一种替代SMC算法。与PCTL*相比，由于它们在DTMC的多个路径上同时解释，验证HyperPCTL*公式是复杂的。此外，由于SMC无法返回Subformulae的满足性问题，因此扩展非稳定设置的自下而上的模型检查算法并不直截了当，因此，它仅在高信性的情况下返回正确的答案。我们根据修改后的贝叶斯测试，提出了一种递归SMC*的递归算法，该测试因递归满意度结果的不确定性而导致。我们已经在Python工具箱Hyprover中实现了算法，并将我们的方法与基于SPRT的SMC进行了比较。我们的实验评估表明，我们的贝叶斯SMC算法在验证时间和推断给定HyperPCTL*公式的满意度所需的样品数量方面的性能更好。
In this paper, we present a Bayesian method for statistical model checking (SMC) of probabilistic hyperproperties specified in the logic HyperPCTL* on discrete-time Markov chains (DTMCs). While SMC of HyperPCTL* using sequential probability ratio test (SPRT) has been explored before, we develop an alternative SMC algorithm based on Bayesian hypothesis testing. In comparison to PCTL*, verifying HyperPCTL* formulae is complex owing to their simultaneous interpretation on multiple paths of the DTMC. In addition, extending the bottom-up model-checking algorithm of the non-probabilistic setting is not straight forward due to the fact that SMC does not return exact answers to the satisfiability problems of subformulae, instead, it only returns correct answers with high-confidence. We propose a recursive algorithm for SMC of HyperPCTL* based on a modified Bayes' test that factors in the uncertainty in the recursive satisfiability results. We have implemented our algorithm in a Python toolbox, HyProVer, and compared our approach with the SPRT based SMC. Our experimental evaluation demonstrates that our Bayesian SMC algorithm performs better both in terms of the verification time and the number of samples required to deduce satisfiability of a given HyperPCTL* formula.
