Minimal state graph generation

Abstract:
We address the problem of generating a minimal state graph from a program, without building the whole state graph. Minimality is considered here with respect to bisimulation. A generation algorithm is derived and illustrated. Applications concern program verification and control synthesis in reactive program compilation.

Reference:

   @ARTICLE{bouajjani92,
      AUTHOR = {A. Bouajjani and J.-C. Fernandez and
               N. Halbwachs and P. Raymond and C. Ratel},
      TITLE = {Minimal state graph generation},
      JOURNAL = {Science of Computer Programming},
      VOLUME = 18,
      PAGES={247--269},
      YEAR = 1992
   }

Postscript file