TY - GEN
T1 - Executable tile specifications for process calculi
AU - Bruni, Roberto
AU - Meseguer, José
AU - Montanari, Ugo
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 1999.
PY - 1999
Y1 - 1999
N2 - Tile logic extends rewriting logic by taking into account sideeffects and rewriting synchronization. These aspects are very important when we model process calculi, because they allow us to express the dynamic interaction between processes and “the rest of the world”. Since rewriting logic is the semantic basis of several language implementation efforts, we can define an executable specification of tile systems by mapping tile logic back into rewriting logic. In particular, this implementation requires the development of a metalayer to control rewritings, i.e., to discard computations that do not correspond to any deduction in tile logic. Our methodology is applied to term tile systems that cover and extend a wide-class of SOS formats for the specification of process calculi. The case study of full CCS, where the term tile format is needed to deal with recursion (in the form of the replicator operator), is discussed in detail.
AB - Tile logic extends rewriting logic by taking into account sideeffects and rewriting synchronization. These aspects are very important when we model process calculi, because they allow us to express the dynamic interaction between processes and “the rest of the world”. Since rewriting logic is the semantic basis of several language implementation efforts, we can define an executable specification of tile systems by mapping tile logic back into rewriting logic. In particular, this implementation requires the development of a metalayer to control rewritings, i.e., to discard computations that do not correspond to any deduction in tile logic. Our methodology is applied to term tile systems that cover and extend a wide-class of SOS formats for the specification of process calculi. The case study of full CCS, where the term tile format is needed to deal with recursion (in the form of the replicator operator), is discussed in detail.
UR - https://www.scopus.com/pages/publications/84947906227
UR - https://www.scopus.com/pages/publications/84947906227#tab=citedBy
U2 - 10.1007/978-3-540-49020-3_5
DO - 10.1007/978-3-540-49020-3_5
M3 - Conference contribution
AN - SCOPUS:84947906227
SN - 3540657185
SN - 9783540657187
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 60
EP - 77
BT - Fundamental Approaches to Software Engineering - 2nd Intrnational Conference, FASE 1999 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 1999, Proceedings
A2 - Finance, Jean-Pierre
PB - Springer
T2 - 2nd International Conference on Fundamental Approaches to Software Engineering, FASE 1999 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 1999
Y2 - 22 March 1999 through 28 March 1999
ER -