A Tableau System for Model Checking Petri Nets with a Fragment of the Linear Time $\mu$-Calculus

We present a tableau system for model checking Petri nets with a fragment of the linear time $\mu$-calculus (without the strong nexttime operator). The model checking problem is already known to be decidable for the full linear time $\mu$-calculus, but the algorithm has non-elementary complexity and gives no insight into the proof process. In contrast to this, tableau systems give a good intuition why a property holds. Although the tableau system is sound and complete and yields a decision procedure, it is not intended to be used as such, but rather as a method for proving and understanding properties expressed in this calculus.     «

We present a tableau system for model checking Petri nets with a fragment of the linear time $\mu$-calculus (without the strong nexttime operator). The model checking problem is already known to be decidable for the full linear time $\mu$-calculus, but the algorithm has non-elementary complexity and gives no insight into the proof process. In contrast to this, tableau systems give a good intuition why a property holds. Although the tableau system is sound and complete and yields a decision proce...     »