Extracting finite state models from i* models

i* models are inherently sequence agnostic. This makes the process of cross-checking i* models against temporal properties quite impossible. There is an immediate industrial need to bridge the gap between such a sequence agnostic model and a standardized model verifier so that model checking can be performed in the requirement analysis phase itself. In this paper, we first spell out the Naive Algorithm that generates all possible finite state models corresponding to a given i* model. The growth of the finite state model space can be mapped to the problem of finding the number of possible paths between the Least Upper Bound (LUB) and the Greatest Lower Bound (GLB) of a k-dimensional hypercube lattice structure. The mathematics for doing a quantitative analysis of the space growth has also been presented. The Naive Algorithm has its main drawback in the hyperexponential growth of the model space. The Semantic Implosion Algorithm is proposed as a solution to the hyperexponential problem. This algorithm exploits the temporal information embedded within the i* model of an enterprise to reduce the rate of growth of the finite state model space. A comparative quantitative analysis between the two approaches concludes the superiority of the Semantic Implosion Algorithm.