A symbolic reachability graph and associated Markov process for a class of dynamic Petri nets