by Till Mossakowski, Markus Roggenbach and Lutz Schröder
Abstract:
CoCASL, a recently developed coalgebraic extension of the algebraic specification language CASL, allows for modelling systems in terms of inductive datatypes as well as of co-inductive process types. Here, we demonstrate how to specify process algebras, namely CCS and CSP, within such an algebraic-coalgebraic framework. It turns out that CoCASL can deal with the fundamental concepts of process algebra in a natural way: The type system of communications, the syntax of processes and their structural operational semantics fit well in the algebraic world of CASL, while the additional coalgebraic constructs of CoCASL cover the various process equivalences (bisimulation, weak bisimulation, observational congruence, and trace equivalence) and provide fully abstract semantic domains. CoCASL hence becomes a meta-framework for studying the semantics and proof theory of reactive systems.
Reference:
Till Mossakowski, Markus Roggenbach and Lutz Schröder: CoCASL at work — Modelling Process Algebra, In Hans-Peter Gumm, ed.: Coalgebraic Methods in Computer Science, Electronic Notes in Theoretical Computer Science, vol. 82, Elsevier Science; http://www.elsevier.nl/, 2003. [preprint]
Bibtex Entry:
@InProceedings{MossakowskiEA03a,
author = {Till Mossakowski and Markus Roggenbach and Lutz Schr{\"o}der},
title = {{CoCASL} at work --- Modelling Process Algebra},
year = {2003},
editor = {Hans-Peter Gumm},
booktitle = {Coalgebraic Methods in Computer Science},
publisher = {Elsevier Science; http://www.elsevier.nl/},
series = {Electronic Notes in Theoretical Computer Science},
volume = {82},
keywords = {CASL CoCASL CSP CCS process algebra coalgebra},
comment = { <a href = "http://www.informatik.uni-bremen.de/~till/papers/process_algebra.pdf"> [preprint] </a>},
psurl = {http://www8.informatik.uni-erlangen.de/~schroeder/papers/process_algebra.ps},
abstract = {CoCASL, a recently developed coalgebraic extension of the algebraic specification language CASL, allows for modelling systems in terms of inductive datatypes as well as of co-inductive process types. Here, we demonstrate how to specify process algebras, namely CCS and CSP, within such an algebraic-coalgebraic framework. It turns out that CoCASL can deal with the fundamental concepts of process algebra in a natural way: The type system of communications, the syntax of processes and their structural operational semantics fit well in the algebraic world of CASL, while the additional coalgebraic constructs of CoCASL cover the various process equivalences (bisimulation, weak bisimulation, observational congruence, and trace equivalence) and provide fully abstract semantic domains. CoCASL hence becomes a meta-framework for studying the
semantics and proof theory of reactive systems.},
}