Time abstraction in timed /spl mu/CRL a la regions

We present the first step towards combining the best parts of the real-time verification methods based on timed automata (the use of regions and zones), and of the process-algebraic approach of languages like LOTOS and muCRL. This could provide with additional verification possibilities for real-time systems, not available in existing timed-automata-based tools like UPPAAL. We aim to transfer the successful techniques of regions and zones as used for the analysis of timed automata to the realm of timed muCRL. First, we aim at replacing all parameters of sort time occurring in the resulting process equation by parameters of discrete sorts. To achieve this goal we apply process-algebraic transformations and abstraction techniques to the given process equation. As a result we obtain a process equation that is closely related to the given one in the following sense. If we abstract from the fractional parts of the time stamps in the actions, both of the equations will be timed bisimilar