Optimizing Maude Programs via Program Specialization

María Alpuente; Demis Ballis; Santiago Escobar; Jose Meseguer; Julia Sapiña

doi:10.1007/978-3-031-31476-6_2

Optimizing Maude Programs via Program Specialization

María Alpuente, Demis Ballis, Santiago Escobar, Jose Meseguer, Julia Sapiña

Research output: Chapter in Book/Report/Conference proceeding › Chapter

Abstract

We develop an automated specialization framework for rewrite theories that model concurrent systems. A rewrite theory R= (Σ, E⊎ B, R) consists of two main components: an order-sorted equational theory E= (Σ, E⊎ B) that defines the system states as terms of an algebraic data type and a term rewriting system R that models the concurrent evolution of the system as state transitions. Our main idea is to partially evaluate the underlying equational theory E to the specific calls required by the rewrite rules of R in order to make the system computations more efficient. The specialization transformation relies on folding variant narrowing, which is the symbolic operational engine of Maude’s equational theories. We provide three instances of our specialization scheme that support distinct classes of theories that are relevant for many applications. The effectiveness of our method is finally demonstrated in some specialization examples.

Original language	English (US)
Title of host publication	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Publisher	Springer
Pages	21-50
Number of pages	30
DOIs	https://doi.org/10.1007/978-3-031-31476-6_2
State	Published - 2023

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	13160 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Online availability

10.1007/978-3-031-31476-6_2

Library availability

Discover UIUC Full Text

Cite this

Alpuente, M., Ballis, D., Escobar, S., Meseguer, J., & Sapiña, J. (2023). Optimizing Maude Programs via Program Specialization. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 21-50). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 13160 LNCS). Springer. https://doi.org/10.1007/978-3-031-31476-6_2

Optimizing Maude Programs via Program Specialization. / Alpuente, María; Ballis, Demis; Escobar, Santiago et al.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer, 2023. p. 21-50 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 13160 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Chapter

Alpuente, M, Ballis, D, Escobar, S, Meseguer, J & Sapiña, J 2023, Optimizing Maude Programs via Program Specialization. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 13160 LNCS, Springer, pp. 21-50. https://doi.org/10.1007/978-3-031-31476-6_2

Alpuente M, Ballis D, Escobar S, Meseguer J, Sapiña J. Optimizing Maude Programs via Program Specialization. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer. 2023. p. 21-50. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-031-31476-6_2

Alpuente, María ; Ballis, Demis ; Escobar, Santiago et al. / Optimizing Maude Programs via Program Specialization. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer, 2023. pp. 21-50 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inbook{12edf3c46a584f6e9d1496a51827cb41,

title = "Optimizing Maude Programs via Program Specialization",

abstract = "We develop an automated specialization framework for rewrite theories that model concurrent systems. A rewrite theory R= (Σ, E⊎ B, R) consists of two main components: an order-sorted equational theory E= (Σ, E⊎ B) that defines the system states as terms of an algebraic data type and a term rewriting system R that models the concurrent evolution of the system as state transitions. Our main idea is to partially evaluate the underlying equational theory E to the specific calls required by the rewrite rules of R in order to make the system computations more efficient. The specialization transformation relies on folding variant narrowing, which is the symbolic operational engine of Maude{\textquoteright}s equational theories. We provide three instances of our specialization scheme that support distinct classes of theories that are relevant for many applications. The effectiveness of our method is finally demonstrated in some specialization examples.",

author = "Mar{\'i}a Alpuente and Demis Ballis and Santiago Escobar and Jose Meseguer and Julia Sapi{\~n}a",

note = "This work has been partially supported by the EC H2020-EU grant agreement No. 952215 (TAILOR), grants RTI2018-094403-B-C32 and PID2021-122830OB-C42 funded by MCIN/AEI/10.13039/501100011033 and by “ERDF A way of making Europe”, by Generali-tat Valenciana under grant PROMETEO/2019/098, and by the Department Strategic Plan (PSD) of the University of Udine—Interdepartmental Project on Artificial Intelligence (2021-25).",

year = "2023",

doi = "10.1007/978-3-031-31476-6_2",

language = "English (US)",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "21--50",

booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

address = "Germany",

}

TY - CHAP

T1 - Optimizing Maude Programs via Program Specialization

AU - Alpuente, María

AU - Ballis, Demis

AU - Escobar, Santiago

AU - Meseguer, Jose

AU - Sapiña, Julia

N1 - This work has been partially supported by the EC H2020-EU grant agreement No. 952215 (TAILOR), grants RTI2018-094403-B-C32 and PID2021-122830OB-C42 funded by MCIN/AEI/10.13039/501100011033 and by “ERDF A way of making Europe”, by Generali-tat Valenciana under grant PROMETEO/2019/098, and by the Department Strategic Plan (PSD) of the University of Udine—Interdepartmental Project on Artificial Intelligence (2021-25).

PY - 2023

Y1 - 2023

N2 - We develop an automated specialization framework for rewrite theories that model concurrent systems. A rewrite theory R= (Σ, E⊎ B, R) consists of two main components: an order-sorted equational theory E= (Σ, E⊎ B) that defines the system states as terms of an algebraic data type and a term rewriting system R that models the concurrent evolution of the system as state transitions. Our main idea is to partially evaluate the underlying equational theory E to the specific calls required by the rewrite rules of R in order to make the system computations more efficient. The specialization transformation relies on folding variant narrowing, which is the symbolic operational engine of Maude’s equational theories. We provide three instances of our specialization scheme that support distinct classes of theories that are relevant for many applications. The effectiveness of our method is finally demonstrated in some specialization examples.

AB - We develop an automated specialization framework for rewrite theories that model concurrent systems. A rewrite theory R= (Σ, E⊎ B, R) consists of two main components: an order-sorted equational theory E= (Σ, E⊎ B) that defines the system states as terms of an algebraic data type and a term rewriting system R that models the concurrent evolution of the system as state transitions. Our main idea is to partially evaluate the underlying equational theory E to the specific calls required by the rewrite rules of R in order to make the system computations more efficient. The specialization transformation relies on folding variant narrowing, which is the symbolic operational engine of Maude’s equational theories. We provide three instances of our specialization scheme that support distinct classes of theories that are relevant for many applications. The effectiveness of our method is finally demonstrated in some specialization examples.

UR - http://www.scopus.com/inward/record.url?scp=85159779864&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85159779864&partnerID=8YFLogxK

U2 - 10.1007/978-3-031-31476-6_2

DO - 10.1007/978-3-031-31476-6_2

M3 - Chapter

AN - SCOPUS:85159779864

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 21

EP - 50

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

PB - Springer

ER -