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 条

[1]

BALCAZAR JL, 1988, EATCS MONOGRAPHS THE, V11

[2] THE TEMPORAL LOGIC OF BRANCHING TIME [J].

BENARI, M ;

PNUELI, A ;

MANNA, Z .

ACTA INFORMATICA, 1983, 20 (03) :207-226

[3]

Boolos GS., 1989, COMPUTABILITY LOGIC

[4]

BRADFIELD JC, 1991, VERIFYING TEMPORAL P

[5]

BURKART O, 1992, LECT NOTES COMPUT SC, V630, P123

[6]

Burkart O, 1994, LECT NOTES COMPUT SC, V836, P98

[7]

CHRISTENSEN S, 1992, LECT NOTES COMPUT SC, V630, P138

[8]

Christensen S., 1993, THESIS U EDINBURGH

[9]

Christensen S., 1993, LECTURE NOTES COMPUT, V715, P143

[10] AUTOMATIC VERIFICATION OF FINITE-STATE CONCURRENT SYSTEMS USING TEMPORAL LOGIC SPECIFICATIONS [J].

CLARKE, EM ;

EMERSON, EA ;

SISTLA, AP .

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1986, 8 (02) :244-263

← 1 2 3 4 →