Sciweavers

Share
CAV
2005
Springer

Syntax-Driven Reachable State Space Construction of Synchronous Reactive Programs

10 years 1 months ago
Syntax-Driven Reachable State Space Construction of Synchronous Reactive Programs
We consider in the current paper the issue of exploiting the structural form of Esterel programs [BG92] to partition the algorithmic RSS (reachable state space) fix-point construction used in modelchecking techniques [CGP99]. 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 local transition relation part. Here a brute-force symbolic breadth-first search would have mixed the exploration of P
Eric Vecchié, Robert de Simone
Added 26 Jun 2010
Updated 26 Jun 2010
Type Conference
Year 2005
Where CAV
Authors Eric Vecchié, Robert de Simone
Comments (0)
books