反应系统的精化计算
Refinement Calculus of Reactive Systems
摘要：
精化演算是一个强大的和表达的工具，推理顺序程序的组合方式。在本文中，我们提出了一个反应系统的精化演算的扩展。精化演算是基于单调谓词Transformers，它将后状态集转换为前状态集。为了对反应系统进行建模，我们引入了单调属性Transformers，它将输出轨迹集变换为输入轨迹集。我们将展示如何在这种语义细化，顺序组合，恶魔的选择，以及其他语义反应系统上的操作模型。我们主要使用高阶逻辑来表达我们的结果，但我们也展示了如何使用其他形式主义更适合自动化，如线性时序逻辑（适用于规范）和符号转换系统（适用于实现）的属性Transformers器可以定义。最后，我们展示了这个框架如何推广以前的工作关系接口，以便能够表达系统的无限行为和活性属性。
英文摘要：
Refinement calculus is a powerful and expressive tool for reasoning about sequential programs in a compositional manner. In this paper we present an extension of refinement calculus for reactive systems. Refinement calculus is based on monotonic predicate transformers, which transform sets of post-states into sets of pre-states. To model reactive systems, we introduce monotonic property transformers, which transform sets of output traces into sets of input traces. We show how to model in this semantics refinement, sequential composition, demonic choice, and other semantic operations on reactive systems. We use primarily higher order logic to express our results, but we also show how property transformers can be defined using other formalisms more amenable to automation, such as linear temporal logic (suitable for specifications) and symbolic transition systems (suitable for implementations). Finally, we show how this framework generalizes previous work on relational interfaces so as to be able to express systems with infinite behaviors and liveness properties.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
