Decidability of model checking for infinite-state concurrent systems

被引：79

作者：

Esparza, J

机构：

[1] Institut für Informatik, Technische Universitat Munchen, D-80290 München

来源：

ACTA INFORMATICA | 1997年 / 34卷 / 02期

关键词：

D O I：

10.1007/s002360050074

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

We study the decidability of the model checking problem for linear and branching time logics, and two models of concurrent computation, namely Petri nets and Basic Parallel Processes.

引用

页码：85 / 107

页数：23

共 37 条

[11]

DAM M, 1992, LECT NOTES COMPUT SC, V652, P39

[12] BRANCHING TIME TEMPORAL LOGIC [J].

EMERSON, EA ;

SRINIVASAN, J .

LECTURE NOTES IN COMPUTER SCIENCE, 1989, 354 :123-172

[13]

EMERSON EA, 1991, P FOCS 91

[14]

ESPARZA J, 1994, B EATCS, V52, P245

[15]

ESPARZA J, 1994, LNCS, V787, P115

[16]

ESPARZA J, 1995, LNCS, V965, P221

[17]

FISCHER MJ, 1974, P SIAM AMS S APPL MA

[18]

HIRSHFELD Y, 1994, LECT NOTES COMPUTER, V832, P165

[19] PROBLEMS CONCERNING FAIRNESS AND TEMPORAL LOGIC FOR CONFLICT-FREE PETRI NETS [J].

HOWELL, RR ;

ROSIER, LE .

THEORETICAL COMPUTER SCIENCE, 1989, 64 (03) :305-329

[20] A TAXONOMY OF FAIRNESS AND TEMPORAL LOGIC PROBLEMS FOR PETRI NETS [J].

HOWELL, RR ;

ROSIER, LE ;

YEN, HC .

THEORETICAL COMPUTER SCIENCE, 1991, 82 (02) :341-372

← 1 2 3 4 →