Is there an example of a timed automaton that requires infinite clock precision, in order to be controller so as to avoid a deadlock or bad state?
I.e. a transition system that consists of nodes connected by edges, and one or more real-values clocks. Nodes can be attributed with invariant (inequation on clock(s)), and edges (transitions) with guards (idem), labels, and the instruction to reset one or more clocks to 0. The initial state is at one node, with all clocks set to zero. The controller must take transitions along the edges whose guard is valid, such that it is always at a node (location) whose invariant is valid, while the clock values simultaneously increase. I
The system should such that the controller would have to change locations faster and faster, i.e. with the difference in clock values between transitions converging to zero.
