Analysis space reduction with state merging for ensuring safety properties of self-adaptive systems

Analyzing guaranteeable safety properties in a running environment aids the decision making of self-adaptive systems. Our previous work generates and updates an analysis space with respect to environmental changes for identifying guaranteeable safety properties efficiently. However, our work cannot use the existing technique for reducing the analysis space, which means that its analysis space has a state explosion problem. In this paper, we propose a new reduction method that merges states while preserving information required for the safety properties analysis. We prove that our technique satisfies the condition for identifying guaranteeable safety properties. In addition, we evaluate the reduction in gives by using a production cell example and confirm that, in the best case, our proposal reduces the analysis space as much as that of a reachability analysis technique that cannot be applied to safety properties analysis.