A complete axiomatization of process temporal logic

被引：0

作者：

Kacprzak, M ^{[1
]}

机构：

[1] Bialystok Tech Univ, Inst Math, PL-15950 Bialystok, Poland

来源：

FUNDAMENTA INFORMATICAE | 2002年 / 50卷 / 01期

关键词：

temporal logic; a complete axiomatization;

D O I：

暂无

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

In this paper is introduced a proof system for branching time temporal logic, called PTL. It allows to verify static and dynamic properties of nondeterministic programs, which are expressed as a temporal formulas of PTL language. The strong completeness theorem of this system is presented.

引用

页码：15 / 31

页数：17

共 12 条

[1]

BOLC L, 1995, WNIOSKOWANIE LOGIKAC

[2]

Emerson EA., 1985, J COMPUTER SYSTEM SC, V30

[3] Verification of temporal properties [J].

Fix, L ;

Grumberg, O .

JOURNAL OF LOGIC AND COMPUTATION, 1996, 6 (03) :343-361

[4]

HAREL D, 1984, HDB PHILOS LOGIC, V2, P497, DOI [DOI 10.1007/978-94-009-6259-0_10, 10.1007/978-94-009-6259-010, DOI 10.1007/978-94-009-6259-010]

[5] A GENERALIZED NEXTTIME OPERATOR IN TEMPORAL LOGIC [J].

KROGER, F .

JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 1984, 29 (01) :80-98

[6]

Manna Z., 1992, TEMPORAL LOGIC REACT, DOI DOI 10.1007/978-1-4612-0931-7

[7]

MIRKOWSKA G, 1987, ALGORITHMIC LOGIC

[8]

Penczek W., 1996, Fundamenta Informaticae, V25, P183

[9]

Penczek W., 1988, Fundamenta Informaticae, V11, P297

[10]

RASIOWA H, 1970, MATH METAMATHEMATICS

← 1 2 →