  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.
