On Optimized Independence Relations For State Space Reduction

. State space reduction techniques are often conservative in the sense that the checked property is not taken into into account. The reduction method discussed in this paper tackles the problem. It is based on automata-theoretic ideas as well as on geometric intuitions and incorporates a fine-grained analysis of the interplay between the system and the checked property. Keywords. Model-checking, state space reduction, trace-closedness, trace-homotopy, temporal logic, hitting-sets. 1. Introduction Model checking of systems against specifications expressed in a variant of temporal logic is a major formal verification method for software and maybe even more so for hardware. Consequently, a considerable amount of research has been performed in the field since its beginnings in the last decade . Approaches to attenuate the impact of a potential state-space explosion due to the high memory complexity of a model-checking procedure can be roughly classified as exploiting ffl an effi..