2020/08/31 by Rob van Glabbeek
Computer Science · #cs.LO
paper · pdf · doi:10.4204/eptcs.322.6
published as EPTCS 322, 2020, pp. 51-68 · In Proceedings EXPRESS/SOS 2020, arXiv:2008.12414
arxiv created 2020/08/31 · arxiv updated 2020/09/01
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.