enumerated during reachability analysis of a concurrent system, while preserving crucial
concurrency properties in the reduced state space. Here we extend the method to the
analysis of certain timed models. We also prove that timing properties of interest, such as
minimum and maximum delays between events, are preserved in the reduced model.
Finally, we report on some experimental results that we have obtained with our extension …