MINIMAL STATE GRAPH GENERATION

被引：32

作者：

BOUAJJANI, A

FERNANDEZ, JC

HALBWACHS, N

RAYMOND, P

RATEL, C

机构：

[1] INST MATH APPL GRENOBLE,LGI,CNRS,UA 398,F-38041 GRENOBLE,FRANCE

[2] MERLIN GERIN,SES,F-38050 GRENOBLE,FRANCE

来源：

SCIENCE OF COMPUTER PROGRAMMING | 1992年 / 18卷 / 03期

关键词：

D O I：

10.1016/0167-6423(92)90018-7

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

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.

引用

页码：247 / 269

页数：23

共 15 条

[1]

BERRY G, 1985, INRIA327 TECH REP

[2]

BILLON JP, 1988, IFIP WG 10 2 INT WOR

[3]

BOUAJJANI A, 1990, P WORKSHOP COMPUTER

[4]

BRYANT RE, 1986, IEEE T COMPUT, V35

[5]

BURCH JR, 1989, SYMBOLIC MODEL CHECK

[6]

CASPI P, 1987, 14TH P ACM S PRINC P

[7]

CLARKE EM, 1986, T PROGRAMMING LANGUA, V8

[8]

COUDERT O, 1989, LECTURE NOTES COMPUT, V407

[9] AN IMPLEMENTATION OF AN EFFICIENT ALGORITHM FOR BISIMULATION EQUIVALENCE [J].

FERNANDEZ, JC .

SCIENCE OF COMPUTER PROGRAMMING, 1990, 13 (2-3) :219-236

[10]

HALBWACHS N, 1991, 3RD P INT S PROGR LA

← 1 2 →