loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Seventh International Conference on Application of Concurrency to System Design (ACSD 2007)
Structural Conditions for Model-checking of Parameterized Networks
Bratislava, Slovak Republic
July 10-July 13
ISBN: 0-7695-2902-X
Siamak Nazari, University of Waterloo, Canada
John Thistle, University of Waterloo, Canada
Sufficient conditions are given for effective model-checking of parameterized ring networks of isomorphic finite-state processes. Unlike others appearing in the literature, the present sufficient conditions do not restrict the mechanism whereby processes interact with one another, but rather the structure of the processes themselves. The results provide "cutoffs" for systems of "piecewise recognizable" processes, and show that all ring networks based on a given piecewise recognizable template fall into a finite number of weak trace equivalence classes. This result is then extended to three other finer equivalence relations: complete trace equivalence, weak failure equivalence and weak possible-futures equivalence. The paper also formalizes a notion of processes whose actions affect only a bounded number of other processes, using the property of "shuffled processes"; if a ring segment is a shuffled process, then all ring networks fall into a finite number of "weak bisimilarity" classes. It is also shown that each of the above equivalence relations preserve a subset of "observable modal logic" formulas.
Citation:
Siamak Nazari, John Thistle, "Structural Conditions for Model-checking of Parameterized Networks," acsd, pp.187-196, Seventh International Conference on Application of Concurrency to System Design (ACSD 2007), 2007
Usage of this product signifies your acceptance of the Terms of Use.