Report on verification of unknown number of processes

[farn@iis.sinica.edu.tw (Farn Wang)]

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.