Timing assumptions and verification of finite-state concurrent systems

We have described a scheme that allows timing assumptions to be incorporated into automatic proofs of arbitrary finite-state temporal properties. The obvious extension is to be able to prove timing properties, not just assume them. This would provide a verification framework for finite-state hard real-time systems. We conjecture that the method presented can, in fact, be extended in this way.Another major question is practicality. We believe that, with some simple program optimizations, the proposed method can be useful for certain small but tricky systems, such as asynchronous control circuits. For larger systems, approximate and heuristic methods will be needed.