A rewriting logic semantics for the analysis of P programs - Durán-Muñoz, Francisco Javier; Ramírez, Carlos; Rocha, Camilo; Pozas, Nicolás (Elsevier, 2025)
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.
Keywords: Lenguajes de programación lógicos; Semántica lógica; P; Maude; Model checking; Reachability analysis; Equational abstraction; LTL model checking; Statistical model checking