P is a domain-specific language designed for specifying asynchronous, event-driven systems. Its computational model is based on actors, i.e., on communicating state machines. This paper presents a formal semantics of P ...