Reactive temporal logic

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

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.
Original languageEnglish
Title of host publication27th International Workshop on Expressiveness in Concurrency 7th Workshop on Structural Operational Semantics, 31 August 2020
EditorsO. Dardha, J. Rot
PublisherOpen Publishing Association
Pages51-68
Number of pages18
Volume322
DOIs
Publication statusPublished - 31 Aug 2020
Event31st International Conference on Concurrency Theory - Vienna, Vienna, Austria
Duration: 1 Sept 20204 Sept 2020
https://concur2020.forsyte.at/

Publication series

NameElectronic Proceedings in Theoretical Computer Science
PublisherOpen Publishing Association
Volume322
ISSN (Electronic)2075-2180

Conference

Conference31st International Conference on Concurrency Theory
Abbreviated titleCONCUR 2020
Country/TerritoryAustria
CityVienna
Period1/09/204/09/20
Internet address

Fingerprint

Dive into the research topics of 'Reactive temporal logic'. Together they form a unique fingerprint.

Cite this