User: Guest  Login
Title:

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

Document type:
Technical Report
Author(s):
Richard Mayr
Abstract:
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...     »
Keywords:
temporal logic; mu-calculus; Petri nets; model checking; tableau systems
Year:
1996
Year / month:
1996-10-01 00:00:00
Pages:
26
 BibTeX