Discrete Time Process Algebra with Silent Step
J. C. M. Baeten, Jan Aldert Bergstra, Michel A. Reniers · The MIT Press eBooks · 2000
The axiom system ACP of [10] was extended to discrete time in [6]. Here, we proceed to define the silent step in this theory in branching bisimulation semantics [7, 15] rather than weak bisimulation semantics [11, 20]. The version using relative timing is discussed extensively, versions using absolute and parametric timing are presented in brief. A term model and a graph model are presented and soundness and completeness results are given. The time free theories BPA # and BPA # # are embedded in the discrete time theories. Examples of the use of the relative time theory are given by means of some calculations on communicating buffers. Note: Partial support received from ESPRIT Basic Research Action 7166, CONCUR2. This paper supersedes [4]. 1 Introduction Process algebra was introduced by Milner in the form of CCS [19]. The original design of CCS and of subsequent versions of process algebra such as ACP [10] and TCSP [14] involves no explicit notion of time. Time is present in the int...