Verification of initial-state opacity in Petri nets