Abstract:
We consider the issue of exploiting the structural form of Esterel programs to partition the algorithmic RSS (reachable state space) fix-point construction used in model-checking techniques. The basic idea sounds utterly simple, as seen on the case of sequential composition: in "P;Q", first compute entirely the states reached in "P", and then only carry on to "Q", each time using only the relevant transition relation part. Here a brute-force symbolic breadth-first search would have mixed the exploration of "P" and "Q" instead, in case "P" had different behaviors of various lengths, and that would result in irregular BBD representation of temporary state spaces, a major cause of complexity in symbolic model-checking.

Slides (.ppt)