Duplication of constants in process algebra

J.C.M. Baeten, M.A. Reniers

Research output: Contribution to journalArticleAcademicpeer-review

1 Citation (Scopus)


The constant 0 (or d, nil) has different roles in process algebra: on the one hand, it serves as the identity element of alternative composition, on the other hand, it stands for a blocked atomic action or for livelock. When extensions with timing are considered, these roles diverge. We argue that it is better to use two separate constants 0¿ and 0 for the different usages. With respect to the termination constant 1 (or , skip), the situation is comparable: on the one hand, it serves as the identity element of sequential composition, on the other hand, it serves as the identity element of parallel composition, and stands for a skipped atomic action. We have separate constants 1¿ and 1 for the different usages. We set up a theory of process algebra, starting out from these four constants in their respective roles. We do this first for the untimed theory, and work out the extension to discrete timing and relative timing in detail. We indicate how extensions involving dense timing or absolute timing are to be handled. All extensions are conservative.
Original languageEnglish
Pages (from-to)151-171
JournalJournal of Logic and Algebraic Programming
Issue number2
Publication statusPublished - 2007


Dive into the research topics of 'Duplication of constants in process algebra'. Together they form a unique fingerprint.

Cite this