A taxonomy of fairness and temporal logic problems for Petri nets
Resource
Theoretical Computer Science 82 (2): 341-372
Journal
Theoretical Computer Science
Journal Volume
82
Journal Issue
2
Pages
341-372
Date Issued
1991
Date
1991
Author(s)
Abstract
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. © 1991.
Other Subjects
Automata Theory - Computability and Decidability; Mathematical Techniques - Petri Nets; Fairness; Nontermination; PTIME Equivalence; Temporal Logic; Computer Metatheory
Type
journal article
File(s)![Thumbnail Image]()
Loading...
Name
04.pdf
Size
3.4 MB
Format
Adobe PDF
Checksum
(MD5):708a094c973d78f8ceccbd2ec14f507e