标题： 运行时顾问 显示英文标题

标题： Runtime Consultants

摘要： 在本文中，我们引入了运行时顾问的概念。 运行时顾问是相对于无限字上的某个值函数定义的。 类似于运行时监视器，它与系统的执行并行运行，并在运行的每一步提供输入。 虽然运行时监视器在发生违反时发出警报，但顾问的思路是主动提供建议，指出下一步应采取的动作以避免违反（或获得定量目标的最大值）。 假设运行时控制器可以考虑这些建议。 运行时顾问不假设其建议总是被遵循。 相反，它会根据实际采取的动作进行调整（类似于车辆导航系统）。 我们展示了如何为验证中常用的值函数计算运行时顾问，并且几乎所有的值函数都有一个在常数时间内运行的运行时顾问。 我们还开发了针对 $\omega$-正则性质的顾问，在它们的经典布尔语义和最近提出的定量解释下都适用。 显示英文摘要

摘要： In this paper we introduce the notion of a runtime consultant. A runtime consultant is defined with respect to some value function on infinite words. Similar to a runtime monitor, it runs in parallel to an execution of the system and provides inputs at every step of the run. While a runtime monitor alerts when a violation occurs, the idea behind a consultant is to be pro-active and provide recommendations for which action to take next in order to avoid violation (or obtain a maximal value for quantitative objectives). It is assumed that a runtime-controller can take these recommendations into consideration. The runtime consultant does not assume that its recommendations are always followed. Instead, it adjusts to the actions actually taken (similar to a vehicle navigation system). We show how to compute a runtime consultant for common value functions used in verification, and that almost all have a runtime consultant that works in constant time. We also develop consultants for $\omega$-regular properties, under both their classical Boolean semantics and their recently proposed quantitative interpretation.