Compositional Minimization Sample Clauses

Compositional Minimization. Compositional model checking is one of the proposed methods for dealing with the problem of state explosion [50, 51, 123]. In the compositional verification of a system, one seeks to verify properties of the system using the properties of its constituent modules. In general, compositional verification may be exploited more effectively when the model is naturally decomposable [128]. In particular, a model consisting of inherently independent modules is suitable for compositional verification. A special case of compositional verification is the method of equivalence based compositional reduction. In this method components of a sys- tem are reduced with respect to an equivalence relation before building the complete sys- tem [60, 50, 79, 82]. In order to be useful in model checking, the selected equivalence relation should satisfy two properties: preservation of all properties to be verified and being a congruence relation with respect to all operators that are used for composing the models. By a congruence relation we mean that the replacement of a component of a model by an equivalent one should always yield a model which is equivalent to the original one. Thus, two main criteria for selecting an equivalence relation to be used for reducing the models are the set of properties to be veri- fied and the composition operators that are used over the models. If using of an equivalence relation to reduce the size of models produces the smallest ones, we refer to the reduction procedure as minimization. For example, in the context of failure based semantic models of the process description language LOTOS, there are two equivalence relations, called chaos-free failures divergences (CFFD) and non-divergent failure divergences (NDFD), which satisfy the preservation prop- erty for two fragments of linear temporal logic. NDFD preserves all properties that are ex- pressible in linear time temporal logic without next-time operator (called LTL−X ) [86]. Also, CFFD preserves all properties that are expressible in linear temporal logic without the next- time operator but with an extra operator that distinguishes deadlocks from divergences (called LTLω) [141, 142]. Also, it has been shown that CFFD and NDFD are the weakest equiva- lence relations that preserve the above mentioned fragments of linear temporal logic. In other words, they both produce the minimized transition systems with respect to the preserved temporal logics. Moreover, it has been shown that in the case of ...