Incremental State Space Construction for Coloured Petri

Abstract. State space analysis is a popular formal reasoning technique. However, it is subject to the crippling problem of state space explosion, where its application to real world models leads to unmanageably large state spaces. In this paper we present algorithms which attempt to alleviate the state space explosion problem by taking advantage of the common practice of incremental development, i.e. where the designer starts with an abstract model of the system and progressively refines it. The performance of the incremental algorithm is compared to that of the standard algorithm for some case studies, and situations under which the performance improvement can be expected are identified. 1 Introduction A major advantage of formal methods is that they allow for formal reasoning. State-based formal reasoning techniques commonly involve examining every possible state of a system. Such techniques are automatic, can be applied by less trained personnel, and can be used for analysis and error detection as well as verification. For these reasons they are seen as one of the most promising formal reasoning techniques [10]. Unfortunately the number of states of a system increases exponentially as the complexity of the system increases. This means that the total number of states is often far too large with respect to time and/or space resources to be fully generated. This growth of the state space is referred to as state space explosion, and is the primary obstacle to the practical application of state-based formal reasoning techniques