定量最弱超前置：通过谓词变换器统一正确性与不正确性超属性
Quantitative Weakest Hyper Pre: Unifying Correctness and Incorrectness Hyperproperties via Predicate Transformers
AI总结：
本文提出面向非确定性与概率程序的定量最弱超前置演算，支持初始状态集和概率分布上的超量推理，并揭示多种谓词变换器间的新对偶性。
摘要：
我们提出了一种新颖的最弱前置演算，用于对非确定性和概率程序上的定量超属性进行推理。现有演算仅支持从单个初始状态出发，推理某个量在程序终止后所取的期望值，而我们则针对初始状态集合或初始概率分布进行此类推理。因此，我们（i）获得了用于超 Hoare 逻辑的最弱前置演算，并（ii）支持对所谓超量进行推理，这些超量不仅包括期望值，还包括先前工作范围之外的量（例如方差）。作为副产品，我们获得了面向加权程序的新颖最强后置，它扩展了现有最强后置演算和最强自由后置演算。我们的框架揭示了前向与后向变换器、正确性与不正确性，以及非终止与不可达性之间的新颖对偶性。
英文摘要：
We present a novel \emph{weakest pre calculus} for \emph{reasoning about quantitative hyperproperties} over \emph{nondeterministic and probabilistic} programs. Whereas existing calculi allow reasoning about the expected value that a quantity assumes after program termination from a \emph{single initial state}, we do so for \emph{initial sets of states} or \emph{initial probability distributions}. We thus (i)~obtain a weakest pre calculus for hyper Hoare logic and (ii)~enable reasoning about so-called \emph{hyperquantities} which include expected values but also quantities (e.g. variance) out of scope of previous work. As a byproduct, we obtain a novel strongest post for weighted programs that extends both existing strongest and strongest liberal post calculi. Our framework reveals novel dualities between forward and backward transformers, correctness and incorrectness, as well as nontermination and unreachability.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
