Algebraic-co-algebraic specification in CoCASL (bibtex)

by Till Mossakowski, Lutz Schröder, Markus Roggenbach and Horst Reichel

Abstract:

We introduce CoCASL as a light-weight but expressive coalgebraic extension of the algebraic specification language CASL. CoCASL allows the nested combination of algebraic datatypes and coalgebraic process types. Moreover, it provides syntactic sugar for an observer-indexed modal logic that allows e.g. expressing fairness properties. This logic includes a generic definition of modal operators for observers with structured equational result types. We prove existence of final models for specifications in a format that allows the use of certain initial datatypes, as well as modal axioms. The use of CoCASL is illustrated by specifications of the process algebras CSP and CCS.

View PDF

Reference:

Till Mossakowski, Lutz Schröder, Markus Roggenbach and Horst Reichel: Algebraic-co-algebraic specification in CoCASL, In Journal of Logic and Algebraic Programming, 67(1-2), pp. 146–197, 2006. Extends (Mossakowski et al. 2003) [preprint]

Bibtex Entry:

@Article{MossakowskiEA04,
  author = {Till Mossakowski and Lutz Schr{\"o}der and Markus Roggenbach and Horst Reichel},
  title = {Algebraic-co-algebraic specification in {CoCASL}},
  year = {2006},
  journal = {Journal of Logic and Algebraic Programming},
  volume = {67},
  pages = {146-197},
  number = {1-2},
  keywords = {Algebraic specification coalgebra process algebra CASL CCS CSP.},
  url = {http://dx.doi.org/10.1016/j.jlap.2005.09.006},
  comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/cocasl.pdf"> [preprint] </a>},
  psurl = {http://www8.informatik.uni-erlangen.de/~schroeder/papers/cocasl.ps},
  abstract = {We introduce CoCASL as a light-weight but expressive coalgebraic extension of the algebraic specification language CASL. CoCASL allows the nested combination of algebraic datatypes and coalgebraic process types.  Moreover, it provides syntactic sugar for an observer-indexed modal logic that allows e.g. expressing fairness properties. This logic includes a generic definition of modal operators for observers with structured equational result types. We prove existence of final models for specifications in a format that allows the use of certain initial datatypes, as well as modal axioms. The use of CoCASL is illustrated by specifications of the process algebras CSP and CCS.},
  note = {Extends (Mossakowski et al. 2003)},
}