Existing model checking tools for infinite state systems, such as UPPAAL, HYTECH and KRONOS, use symbolic forward analysis,
a possibly nonterminating procedure. We give termination criteria that allow us to reason compositionally about systems defined
with asynchronous parallel composition; we can prove the termination of symbolic forward analysis for a composed system from
the syntactic conditions satisfied by the component systems.
Our results apply to nonlinear hybrid systems; in particular to rectangular hybrid systems, timed automata and o-minimal systems.
In the case of integer-valued systems we give negative results: forward analysis is not well-suited for this class of infinite-state
systems.
Support from the grants NSF award CCR99-70925, SRC award 99-TJ-688, and DARPA ITO Mobies award F33615-00-C-1707 is gratefully
acknowledged