Discretization of Timed Automata in Timed μCRL à la Regions and Zones

This paper describes the initial steps in the discretization of a timed μCRL process equation representing a timed automaton. If the fractional parts of the time stamps of the actions are neglected, the translation results in a timed bisimilar representation with only discrete parameters and bound variables. To this end we apply “standard” techniques such as coordinate transformation and abstraction.