A rewriting logic semantics for the analysis of <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" altimg="si1.svg"> <mml:mtext mathvariant="sans-serif">P</mml:mtext> </mml:math> programs

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 using rewriting logic, extending the language's verification capabilities. Implemented in Maude, a rewriting logic language, this semantics enables automated analysis of P programs, including reachability analysis, LTL model checking, and statistical model checking. Through illustrative examples, this paper demonstrates how this formalization significantly enhances P 's verification capacities in practical scenarios.