Efficient State Space Reduction Using Trace Spaces
State-space reduction techniques, used primarily in model-checkers in order to verify programs, all rely on the idea that some actions are independent, hence could be taken in any (respective) order while put in parallel, without changing the semantics. It is thus not necessary to consider all execution paths in the interleaving semantics of a concurrent program, but rather some equivalence classes. We describe a new algorithm to compute such equivalence classes, and a representative per class, which is based on ideas originating in algebraic topology. We introduce a geometric semantics of concurrent languages, where programs are interpreted as directed topological spaces, and study its properties in order to devise an algorithm for computing dihomotopy classes of execution paths. We will also report on a preliminary implementation, showing promising results towards efficient methods to analyze concurrent programs, with better results than state of the art partial-order reduction techniques.