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

The design of evolving discrete-event systems needs for adequate modeling techniques. A Petri net-based reflective layout has been recently proposed to support dynamic discreteevent system's design. Keeping functional aspects separated from evolutionary ones, deploying changes to the (current) system configuration when necessary, results in a clean formal model preserving the ability of verifying properties typical of Petri nets. Reflective Petri nets are provided with a pseudo-symbolic statetransition graph, and an associated lumped Markov process