Recently, we have developed a new verification technique which can be used to verify infinite state systems. A manuscript: Verification of Dynamic Linear Lists for All Numbers of Processes in PostScript format can be obtained through my webpage: http://www.iis.sinica.edu.tw/~farn/index.html#quo A preliminary report can also be found in TR-IIS-98-019 published last year. Thank you for reading this email. Best wishes, Farn ABSTRACT: In real-world design and verification of concurrent systems with many identical processes, the number of processes is never a factor in the system correctness. This paper embodies such an engineering reasoning to propose an almost automatic method to safely verify safety properties of such systems. The central idea is to construct a finite collective quotient structure (CQS) which collapses state-space representations for all system implementations with all numbers of processes. The problem is presented as safety bound problem which ask if the number of processes satisfying a certain property exceeds a given bound. Our method can be applied to systems with dynamic linear lists of unknown number of processes. Processes can be deleted from or inserted at any position of the linear list during transitions. We have used our method to develop CQS constructing algorithms for two classes of concurrent systems : (1) untimed systems with a global waiting queue and (2) dense-time systems with one local timer per process. We show that our method is both sound and complete in verifying the first class of systems. The verification problem for the second class systems is undecidable even with only one global binary variable. However, our method can still automatically generate a CQS of size no more than 1512 nodes to verify that an algorithm in the class: Fischer's timed algorithm indeed preserves mutual exclusion for any number of processes.