Syntax-driven Behavior Partitioning for Model-checking of Esterel Programs

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

• Type: Journal
• Year: 2006
• Where: ENTCS
• Authors: Eric Vecchié, Robert de Simone
• Keywords: ENTCS 2006, Relevant Transition Relation, State Spaces, Transition Relation