RT Journal Article
T1 A rewriting logic semantics for the analysis of P programs
A1 Durán-Muñoz, Francisco Javier
A1 Ramírez, Carlos
A1 Rocha, Camilo
A1 Pozas, Nicolás
K1 Lenguajes de programación lógicos
K1 Semántica lógica
AB 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.
PB Elsevier
SN 2352-2208
YR 2025
FD 2025-02-15
LK https://hdl.handle.net/10630/38528
UL https://hdl.handle.net/10630/38528
LA eng
NO Durán, F., Ramírez, C., Rocha, C., & Pozas, N. (2025). A rewriting logic semantics for the analysis of P programs. Journal of Logical and Algebraic Methods in Programming, 144, 101048.
NO Funding for open access charge: Universidad de Málaga / CBUA
DS RIUMA. Repositorio Institucional de la Universidad de Málaga
RD 5 mar 2026