概率条件系统不变式的贝叶斯推理
Probabilistic Conditional System Invariant Generation with Bayesian Inference
摘要：
不变量是程序属性上的一组属性，这些属性在程序执行期间被期望为真。由于手动开发这些不变量可能成本高昂且具有挑战性，因此有无数方法支持从程序跟踪等源自动挖掘可能的不变量。然而，现有的方法，没有配备捕捉条件自主移动机器人的行为，或管理与这些系统中的许多变量的不确定性丰富的国家。这意味着只有在特定状态下才出现的有价值的不变量仍然没有被发现。在这项工作中，我们介绍了一种方法来推断条件概率不变量，以协助在这种丰富的状态，随机系统的行为的特征。这些概率不变量可以编码一系列的条件模式，使用贝叶斯推理来利用观察到的跟踪数据来对抗从先前的经验和专家知识中收集的先验，并根据它们的惊喜值和信息内容进行排名。我们对两个半自主移动机器人系统的研究表明，所提出的方法是如何能够产生有价值的和以前隐藏的状态不变量。
英文摘要：
Invariants are a set of properties over program attributes that are expected to be true during the execution of a program. Since developing those invariants manually can be costly and challenging, there are a myriad of approaches that support automated mining of likely invariants from sources such as program traces. Existing approaches, however, are not equipped to capture the rich states that condition the behavior of autonomous mobile robots, or to manage the uncertainty associated with many variables in these systems. This means that valuable invariants that appear only under specific states remain uncovered. In this work we introduce an approach to infer conditional probabilistic invariants to assist in the characterization of the behavior of such rich stateful, stochastic systems. These probabilistic invariants can encode a family of conditional patterns, are generated using Bayesian inference to leverage observed trace data against priors gleaned from previous experience and expert knowledge, and are ranked based on their surprise value and information content. Our studies on two semi-autonomous mobile robotic systems show how the proposed approach is able to generate valuable and previously hidden stateful invariants.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
