Proving temporal properties of Petri nets

Research output: Chapter in Book/Report/Conference proceedingChapter


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.
Original languageEnglish
Title of host publicationAdvances in Petri Nets 1991
EditorsGrzegorz Rozenberg
PublisherSpringer Berlin Heidelberg
Number of pages19
ISBN (Electronic)978-3-540-47600-9
ISBN (Print)978-3-540-54398-5
Publication statusPublished - 1991

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg


  • Petri nets
  • temporal logic
  • tableau systems
  • model-checking

Fingerprint Dive into the research topics of 'Proving temporal properties of Petri nets'. Together they form a unique fingerprint.

Cite this