[pancsta]

> It captures the nondeterminism in the order of delivery of communications. The Subsequent transition captures fairness arising from the guarantee of delivery. We provide a denotational semantics for our minimal actor language in terms of the transition relations.

Juicy paper, not to mention the declassification. It really reminds me of asyncmachine.dev which has actors, relations, transitions, and embraces non-determinism.