An effective axiomatization for real time ACP

Baeten and Bergstra added real time to ACP, and introduced the notion of integration, which expresses the possibility of an action happening within a time interval. In order to axiomatize this feature, they needed an `uncountable' axiom. This paper deals with prefix integration, and integration is parametrized by conditions, which are inequalities between linear expressions of variables. We present an axiomatization for process terms, and propose a strategy to decide bisimulation equivalence between process terms, by means of this axiomatization.