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 language | English |
---|---|
Title of host publication | 27th International Workshop on Expressiveness in Concurrency 7th Workshop on Structural Operational Semantics, 31 August 2020 |
Editors | O. Dardha, J. Rot |
Publisher | Open Publishing Association |
Pages | 51-68 |
Number of pages | 18 |
Volume | 322 |
DOIs | |
Publication status | Published - 31 Aug 2020 |
Event | 31st International Conference on Concurrency Theory - Vienna, Vienna, Austria Duration: 1 Sept 2020 → 4 Sept 2020 https://concur2020.forsyte.at/ |
Publication series
Name | Electronic Proceedings in Theoretical Computer Science |
---|---|
Publisher | Open Publishing Association |
Volume | 322 |
ISSN (Electronic) | 2075-2180 |
Conference
Conference | 31st International Conference on Concurrency Theory |
---|---|
Abbreviated title | CONCUR 2020 |
Country/Territory | Austria |
City | Vienna |
Period | 1/09/20 → 4/09/20 |
Internet address |