Is it vacuous to check redundancy, or is it redundant to check vacuity?

What the paper says

We present an automatic method to detect the existence of redundant requirements. A requirement is redundant if it does not represent an additional restriction on the intended behaviour of the specified system. If unintended, a redundancy may hint at a defect. The method applies to real-time requirements formalized in a particular kind of real-time logic formalism. The method uses techniques derived from real-time model checking. In particular, we use Phase Event Automata, a variant of timed automata. We introduce a novel determinism-preserving totalisation procedure for Phase Event Automata for the purpose of the automata-theoretic operation of complementation. The method is complete in the sense that it detects every redundancy in a given set of requirements. We have implemented the method. Preliminary experiments on industrial benchmarks indicate its scalability and its usefulness for discovering previously unknown defects. In spirit, redundancy is closely related to the property of vacuity. We show, however, that checking redundancy does not make checking vacuity redundant, and vice versa. This means that none of the two checks is superseeded by the other one. This article is the extension of a previous conference paper.