Validation of liveness for 1-safe hybrid Petri nets using network unfolding

This paper presents sufficient conditions validating the liveness of hybrid systems modeled by 1-safe hybrid Petri nets. Hybrid Petri nets provide a convenient model for hybrid dynamical systems. These network models isolate the discrete-event dynamics of the hybrid system to the Petri network, thereby allowing the validation problem to be decoupled into two steps. The first step involves verifying that the Petri network is live and the second step computes overbounding approximations to the viability sets associated with cycles within the Petri network´s output language.