COMPLETENESS IN REAL-TIME PROCESS ALGEBRA

Recently, J.C.M. Baeten and J.A. Bergstra extended ACP with real time, resulting in a Real Time Process Algebra, called ACP-rho [BB91]. They introduced an equational theory and an operational semantics. However, their work does not contain a completeness result nor does it contain the definitions to give proofs in detail. In this paper we introduce some machinery and a completeness result. The operational semantics of [BB91] contains the notion of an idle step reflecting that a process can do nothing more then passing the time before performing a concrete action at a certain point in time. This idle step corresponds nicely to our intuition but it results in infinitary transition systems. In this paper we give a more abstract operational semantics, by abstracting from the idle step. Due to this simplification we can prove soundness and completeness easily. These results hold for the semantics of [BB91] as well, since both operational semantics induce the same equivalence relation between processes.