One of the prominent methods for program verification is that of
[CES86,QS82]. In the last decade there has been an extensive research effort in order to extend the applicability of model checking to systems with infinite state spaces. There are at least two reasons why a system may be infinite-state:
– A system may operate on data structures with unbounded domains. Examples include real-valued clocks in timed automata [AD94], stacks in push-down automata [BEM97], queues in communicating processes [AJ96], counters in counter machines, etc.
– A system can also be infinite-state because it is
. This means that the description of the system is parameterized by the number of components inside the system. In such a case, we would like to verify correctness of the system regardless of the number of processes.
We consider systems which contain both sources of infiniteness; namely parameterized systems of processes each of which behaves as a timed automaton.