The accurate and efficient timing verification of interacting finite state machines