Quasi-Equal Clock Reduction On-the-Fly

For timed automata, there is the notion of quasi-equal clocks. Two clocks are quasi-equal if, in each reachable configuration, they are equal or at least one has value 0. There are approaches to exploit quasi-equality of clocks to speed up reachability checking for timed automata. There is a procedure to detect quasi-equal clocks and a syntactical transformation of networks of timed automata where quasi-equal clocks are encoded by one representative clock and one boolean token per clock.