Discrete time process algebra with silent step

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].

• Type: Conference
• Year: 2000
• Where: BIRTHDAY
• Authors: Jos C. M. Baeten, Jan A. Bergstra, Michel A. Reniers
• Keywords: Applied Computing, BIRTHDAY 2000, Bisimulation Semantics, Discrete Time, Weak Bisimulation Semantics