Extra material for the analysis of asynchronous systems

You can find a more general explanation of histories in the Andrews book. Pages 42-43. Here histories are defined as a sequence of actions to record the state of a concurrent execution. This is different from the histories that we have seen during the lectures, where histories are sequences of communication events. You can find some explanations about communication events in the Andrews book, page 452.

If you are interested in the topic, and want to read more, you can have a look to these two references:

• Modular Reasoning for Message-passing Programs ( Technical Report ). Jinjiang Lei, Zongyan Qiu
• A sound and complete reasoning system for asynchronous communication with shared futures. Crystal Chang Din, Olaf Owe