microCRL(ID:4971/mic011)

Algebraic specification 

Algebraic specification language from CWI

According to Bruns 1991, process part based on ACP
Related languages
ACP => microCRL   Based on
iCRL => microCRL   Extension of
microCRL => pCRL   Extension of
References:
  • Bruns, Glenn "A Language for value-passing CCS" LFCS report ECS-LFCS-91-175 view details Abstract: Milner has defined an extension to CCS, called value-passing CCS, which allows parameterized agents and actions, and conditional expressions. This notation leaves open the problems of describing data and of associating sets of values with actions. We define a language for value-passing CCS in which sets, sequences, and tuples are built from natural number, boolean, and string constants. Only finite values can be constructed. Our language also contains declarations to associate set-valued expressions with actions. This paper contains a definition of the language and a description of a translator to basic CCS.


    External link: Online copy
  • Groote, J.F. and A. Ponse. muCRL: A base for analysing processes with data. In E. Best and G. Rozenberg, editors, Proceedings 3rd Workshop on Concurrency and Compositionality, Goslar, GMD-Studien Nr. 191, pages 125-130. Universität Hildesheim, May 1991 view details
  • Groote, F. and Ponse, A. "Proof theory for muCRL: a language for processes with data" pp232-251 view details Abstract: A proof theory for the specification language muCRL (micro-CRL) is
    proposed.  muCRL consists of process algebra extended with abstract
    data types. The proof theory is meant to formalize the interaction
    between processes and data. Furthermore it provides the means to prove
    properties about these in a precise way. The proof theory has been
    designed such that automatic proof checking is feasible.

    A simple language is defined in which basic properties of processes and
    of data can be expressed. A proof system is presented for this property
    language, comprising a rule for induction, the Recursive Specification
    Principle, and process algebra axioms. The proof theory is illustrated
    with small examples, and a case study about a bag.

          in Andrews, D.J. ; J.F. Groote, and C.A. Middelburg, editors, Proceedings IWSSL (International Workshop on Semantics of Specification Languages), Workshops in Computing, Springer-Verlag, 1994 view details
  • Groote, J.F. and A. Ponse. The syntax and semantics of muCRL. A. Ponse, C. Verhoef, and S.F.M. van Vlijmen, editors. Algebra of Communicating Processes, Utrecht 1994. Workshops in Computing, Springer-Verlag, pages 26-62, 1995. view details
          in Andrews, D.J. ; J.F. Groote, and C.A. Middelburg, editors, Proceedings IWSSL (International Workshop on Semantics of Specification Languages), Workshops in Computing, Springer-Verlag, 1994 view details