Given a requirement like
if A and B and not C then D must happen within 10ms
That can clearly be tested albeit at the cost of some pain proving the 10ms bit, but what happens if the requirement was instead
if and only if A and B and not C then D.....
It seems to me that the only if likely requires an exhaustive exploration of the programs state space, and that is clearly infeasible given a reasonably large amount of state (And may be the sort of thing that Turing had things to say about). This is very much the kind of condition that applies to such things as firing airbags and other such things concerned with harm mitigation.
Is my suspicion about the difficulty of testing such things correct, and what are the strategies to reduce the size of the state space that must be explored to achieve coverage of such a requirement?