| Property | Meaning | How to verify | |----------|---------|----------------| | | Places don’t accumulate infinite tokens | Maximum token count per place is finite | | Liveness | No deadlock; every transition can eventually fire | Check for circular dependencies | | Reachability | Can a certain marking be reached? | Reachability graph | | Safeness | Special case of boundness (max 1 token per place) | Inspect initial marking and firing rules | | Home state | Can return to initial marking? | Look for cycles in reachability graph |