Time Abstracted Bisimulation: Implicit Specifications and Decidability

ed Bisimulation: Implicit Specifications and Decidability Kim G. Larsen y and Yi Wang z January 8, 1997 Abstract 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 In this paper, we introduce a time--abstracting (bisimulation) equivalence, and investigate its properties with respect to the real--time process calculus of [Wan90]. 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 p..