From mboxrd@z Thu Jan  1 00:00:00 1970
X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/1069
Path: news.gmane.org!not-for-mail
From: farn@iis.sinica.edu.tw (Farn Wang)
Newsgroups: gmane.science.mathematics.categories
Subject: Report on verification of unknown number of processes
Date: Wed, 10 Mar 1999 14:29:03 +0800 (CST)
Message-ID: <199903100629.OAA24756@ccs1.iis.sinica.edu.tw>
NNTP-Posting-Host: main.gmane.org
X-Trace: ger.gmane.org 1241017543 29350 80.91.229.2 (29 Apr 2009 15:05:43 GMT)
X-Complaints-To: usenet@ger.gmane.org
NNTP-Posting-Date: Wed, 29 Apr 2009 15:05:43 +0000 (UTC)
To: categories@mta.ca
Original-X-From: cat-dist Thu Mar 11 21:32:12 1999
Original-Received: (from Majordom@localhost)
	by mailserv.mta.ca (8.9.3/8.9.3) id UAA30544
	for categories-list; Thu, 11 Mar 1999 20:49:24 -0400 (AST)
X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f
Original-Sender: cat-dist@mta.ca
Precedence: bulk
Original-Lines: 49
Xref: news.gmane.org gmane.science.mathematics.categories:1069
Archived-At: <http://permalink.gmane.org/gmane.science.mathematics.categories/1069>


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.