Time-Abstracted Bisimulation: Implicit Specifications and Decidability

In the last few years a number of real-time process calculi have emerged with the purpose of capturing important quantitative aspects of real-time systems. In addition, a number of process equivalences sensitive to time-quantities have been proposed, among these the notion of timed (bisimulation) equivalence. In this paper, we introduce a time-abstracting (bisimulation) equivalence and investigate its properties with respect to the real-time process calculus of Wang (Real-time behaviour of asynchronous agents, in "Proceedings of CONCUR90," Lecture Notes in Computer Science, Vol. 458, Springer-Verlag, Berlin/New York, 1990). Seemingly, such an equivalence would yield very little information (if any) about the timing properties of a process. However, time-abstracted reasoning about a composite process may yield important information about the relative timing-properties of the components of the system. In fact, we show as a main theorem that such implicit reasoning will reveal all timing aspects of a process. More precisely, we prove that two processes are interchangeable in any context up to time-abstracted equivalence precisely if the two processes are themselves timed equivalent. As our second main theorem, we prove that time-abstracted equivalence is decidable for the calculus of Wang, using classical methods based on a finite-state symbolic, structured operational semantics.