@inbook{bcd36a9e7e0741f7abdd64e6e11c4bbd,
title = "Proving temporal properties of Petri nets",
abstract = "We present a sound and complete tableau system for proving temporal properties of Petri nets, expressed in a propositional modal mucalculus which subsumes many other temporal logics. The system separates the checking of fix-points from the rest of the logic, which allows the use of powerful reasoning, perhaps specific to a class of nets or an individual net, to prove liveness and fairness properties. Examples are given to illustrate the use of the system. The proofs of soundness and completeness are given in detail.",
keywords = "Petri nets, temporal logic, tableau systems, model-checking",
author = "J.C. Bradfield",
year = "1991",
doi = "10.1007/BFb0019967",
language = "English",
isbn = "978-3-540-54398-5",
volume = "524",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "29--47",
editor = "Grzegorz Rozenberg",
booktitle = "Advances in Petri Nets 1991",
address = "United Kingdom",
}