TY - JOUR
T1 - A rewriting logic semantics for the analysis of P programs
AU - Durán, Francisco
AU - Ramírez, Carlos
AU - Rocha, Camilo
AU - Pozas, Nicolás
N1 - Publisher Copyright:
© 2025 Elsevier Inc.
PY - 2025/3
Y1 - 2025/3
N2 - 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.
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.
KW - Equational abstraction
KW - LTL model checking
KW - Maude
KW - Model checking
KW - P
KW - Reachability analysis
KW - Statistical model checking
UR - http://www.scopus.com/inward/record.url?scp=85217893084&partnerID=8YFLogxK
U2 - 10.1016/j.jlamp.2025.101048
DO - 10.1016/j.jlamp.2025.101048
M3 - Article
AN - SCOPUS:85217893084
SN - 2352-2208
VL - 144
JO - Journal of Logical and Algebraic Methods in Programming
JF - Journal of Logical and Algebraic Methods in Programming
M1 - 101048
ER -