Reactive Temporal Logic

TL;DR

Reactive temporal logic is introduced as a new framework for analyzing reactive systems, enabling precise definitions of concepts like fair schedulers and mutual exclusion protocols, which were previously more ambiguous.

Contribution

The paper develops reactive temporal logic, extending traditional temporal logic to better model and specify reactive systems with environment interactions.

Findings

Formal definitions of fair scheduler and mutual exclusion protocol using reactive temporal logic

Reactive temporal logic provides more precise and less ambiguous specifications

Application demonstrates improved clarity over previous conceptual approaches

Abstract

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.