Description and Analysis of Fairness on Temporal Logic of Actions

被引：2

作者：

Li, Juntao ^{[1
]}

Tang, Zhengyi ^{[1
]}

Li, Xiang ^{[1
]}

机构：

[1] Guizhou Univ, Inst Comp Software & Theory, Guiyang 550003, Peoples R China

来源：

2009 INTERNATIONAL CONFERENCE ON NETWORKING AND DIGITAL SOCIETY, VOL 1, PROCEEDINGS | 2009年

关键词：

Transition System; TLA; Fairness; Model checking;

D O I：

10.1109/ICNDS.2009.17

中图分类号：

TP39 [计算机的应用];

学科分类号：

081203 ; 0835 ;

摘要：

TLA(Temporal Logic of Actions) and it's specifying language TLA+ have become an efficient and convenient approach for model checking, and fairness is a vital property in TLA. We try to analyze the definitions of fairness based on TLA, point out a fallible question on the definition of fairness in cited literature [5], improve it more clearly and prove the consistency of syntax and semantics of fairness, and subdivide the fairness in the end.

引用

页码：41 / 44

页数：4

共 11 条

[1] [Anonymous], 1980, POPL 80 PROC 7 ACM S, DOI DOI 10.1145/567446.567462
[2] CHOU CT, 1993, LNCS, V780, P310
[3] EERZ S, 1987, ESCUELA VERANO, V73, P207
[4] FRANCEZ N, 1986, TEXTS MONOGRAPHS COM
[5] Fairness and hyperfairness
Lamport, L
[J]. DISTRIBUTED COMPUTING, 2000, 13 (04) : 239 - 245
[6] THE TEMPORAL LOGIC OF ACTIONS
LAMPORT, L
[J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1994, 16 (03): : 872 - 923
[7] Lamport L., 2002, Specifying Systems
[8] LAMPORT L, 1993, AM MATH MON IN PRESS
[9] THE TEMPORAL SEMANTICS OF CONCURRENT PROGRAMS
PNUELI, A
[J]. THEORETICAL COMPUTER SCIENCE, 1981, 13 (01) : 45 - 60
[10] Prawitz D., 1965, ACTA U STOCKHOLMIENS, V3

← 1 2 →