Partitioning State Spaces of Concurrent Transition Systems

International Arab Journal of Information Technology (IAJIT)

Maryam Madani¹  Shadpour Mallakpour² 

[1] Department of Chemistry, Isfahan University of Technology, Isfahan 84156-83111, I. R. Iran$$Department of Chemistry, Isfahan University of Technology, Isfahan 84156-83111, I. R. IranDepartment of Chemistry, Isfahan University of Technology, Isfahan 84156-83111, I. R. Iran$$;Department of Chemistry, Isfahan University of Technology, Isfahan 84156-83111, I. R. Iran$$Nanotechnology and Advanced Materials Institute, Isfahan University of Technology, Isfahan 84156-83111, I. R. Iran$$Department of Chemistry, Isfahan University of Technology, Isfahan 84156-83111, I. R. IranDepartment of Chemistry, Isfahan University of Technology, Isfahan 84156-83111, I. R. Iran$$Nanotechnology and Advanced Materials Institute, Isfahan University of Technology, Isfahan 84156-83111, I. R. Iran$$Nanotechnology and Advanced Materials Institute, Isfahan University of Technology, Isfahan 84156-83111, I. R. IranDepartment of Chemistry, Isfahan University of Technology, Isfahan 84156-83111, I. R. Iran$$Nanotechnology and Advanced Materials Institute, Isfahan University of Technology, Isfahan 84156-83111, I. R. Iran$$

关键词: Concurrent transition systems;    distributed and parallel analysis;    abstraction;    partitioning;    refinement.;   

DOI  :  

学科分类：计算机科学（综合）

来源: Zarqa University

【 摘 要 】

As the model-checking becomes increasingly used in the industry as an analysis support, there is a big need for efficient new methods to deal with the large real-size of concurrent transition systems. We propose a new algorithm for partitioning the large state space modelling industrial designs as concurrent transition systems with hundreds of millions of states and transitions. The produced partitions will be used by distributed processes for parallel system analysis. The state space is supposed to be represented by a weighted Kripke structure (this is an extension of the Kripke structure where weights are associated with the states and with the transitions). This algorithm partitions the weighted Kripke structure by performing a combination of abstraction-partition-refinement on this structure. The algorithm is designed in a way that reduces the communication overhead between the processes. The experimental results on large real designs show that this method improves the quality of partitions, the communication overhead and then the overall performance of the system analysis.Keywords: Concurrent transition systems, distributed and parallel analysis, abstraction, partitioning, refinement.Received February 6, 2004; accepted July 4, 2004Full Text

【 授权许可】

Unknown