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 discrete event 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 state transition graph, and an associated lumped Markov process.