论文标题
反应性时间逻辑
Reactive Temporal Logic
论文作者
论文摘要
虽然时间逻辑的标准处理对于封闭的系统来说足够，但与环境没有运行时相互作用，但它们因反应性系统而缺乏，通过动作同步与环境相互作用。本文介绍了反应性时间逻辑，这是一种适用于反应性系统的时间逻辑的形式。我通过应用它来制定公平调度程序的定义和正确的相互排除协议来说明其使用。这些概念的先前定义在概念上的参与度更高或更精确，导致关于给定协议是否满足隐式要求的辩论。
Whereas standard treatments of temporal logic are adequate for closed systems, having no run-time interactions with their environment, they fall short for reactive systems, interacting with their environments through synchronisation of actions. This paper introduces reactive temporal logic, a form of temporal logic adapted for the study of reactive systems. I illustrate its use by applying it to formulate definitions of a fair scheduler, and of a correct mutual exclusion protocol. Previous definitions of these concepts were conceptually much more involved or less precise, leading to debates on whether or not a given protocol satisfies the implicit requirements.
