On the Reachability Space and Deadlock-Freeness in Flexible Nets

Deadlock-freeness is a basic property of dynamical systems that ensures that at least one process of the system can operate indefinitely. Given that a system is deadlock-free if at any reachable state there is at least one process that can operate, the reachability space, i.e. the set of states that can be reached, and deadlock-freeness are closely related. This paper focuses on some fundamental properties of the reachability space of Flexible Nets, a modeling formalism that can easily account for uncertain parameters. After showing that the reachability space is convex, a sufficient condition for deadlock-freeness is derived.