A TAXONOMY OF FAIRNESS AND TEMPORAL LOGIC PROBLEMS FOR PETRI NETS

被引：22

作者：

HOWELL, RR

ROSIER, LE

YEN, HC

机构：

[1] UNIV TEXAS, DEPT COMP SCI, AUSTIN, TX 78712 USA

[2] NATL TAIWAN UNIV, DEPT ELECT ENGN, TAIPEI, TAIWAN

来源：

THEORETICAL COMPUTER SCIENCE | 1991年 / 82卷 / 02期

基金：

美国国家科学基金会;

关键词：

D O I：

10.1016/0304-3975(91)90228-T

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

In this paper, we define a temporal logic for reasoning about Petri nets. We show the model checking problem for this logic to be PTIME equivalent to the Petri net reachability problem. Using this logic and two refinements, we show the fair nontermination problem to be PTIME equivalent to reachability for several definitions of fairness. For other versions of fairness, this problem is shown to be either PTIME equivalent to the boundedness problem or highly undecidable. In all, 24 versions of fairness are examined.

引用

页码：341 / 372

页数：32

共 39 条

[1]

APT K, 1982, 2ND P C F SOFTW TECH, P146

[2] LIMITS FOR AUTOMATIC VERIFICATION OF FINITE-STATE CONCURRENT SYSTEMS [J].