Structural conditions for model-checking of parameterized networks

被引:0
作者
Nazari, Siamak [1 ]
Thistle, John [1 ]
机构
[1] Univ Waterloo, Waterloo, ON N2L 3G1, Canada
来源
SEVENTH INTERNATIONAL CONFERENCE ON APPLICATION OF CONCURRENCY TO SYSTEM DESIGN, PROCEEDINGS | 2007年
关键词
D O I
10.1109/ACSD.2007.32
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
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.
引用
收藏
页码:187 / +
页数:2
相关论文
共 17 条
  • [11] NILSSON M, 2005, THESIS UPPSALA U
  • [12] SISTLA AP, 1999, FORM ASP COMPUT, V11, P402
  • [13] Stirling C., 2001, MODAL TEMPORAL PROPE
  • [14] THISLE JG, 2005, 44 IEEE C DEC CONTR
  • [15] THISTLE JG, 2004, 16 INT S MATH THEOR
  • [16] VANGLABBEK RJ, 1990, LNCS, V458, P278
  • [17] WOLPER P, 1990, LECT NOTES COMPUT SC, V407, P68