Reducing quasi-equal clocks in networks of timed automata

Abstract. We introduce the novel notion of quasi-equal clocks and use it to improve the verification time of networks of timed automata. Intu-itively, two clocks are quasi-equal if, during each run of the system, they have the same valuation except for those points in time where they are reset. We propose a transformation that takes a network of timed au-tomata and yields a network of timed automata which has a smaller set of clocks and preserves properties up to those not comparing quasi-equal clocks. Our experiments demonstrate that the verification time in three transformed real world examples is much lower compared to the original.