Eric VECCHIÉ

INRIA Sophia Antipolis

2004 Route des Lucioles BP93, 06902 Sophia Antipolis, FRANCE

Eric.Vecchie@sophia.inria.fr

** 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)