IEEE Robotics & Automation Magazine - June 2015 - 91

T20

T10
P11

P21

R1

T11

P10

P12

T21

P22

R2

T12

P13

P20

T22

P23

R3

T13

T23
(b)

Figure 6. (continued) Computing the maximally permissive DAP for the RAS of Figure 1 through the incremental synthesis approach
that is presented in [34]. The approach starts with the solution of a MIP formulation that assesses the presence of minimal empty
siphons in the dynamics of the original process-resource net of Figure 5. The solution of this formulation could detect either of
the two minimal deadlocks corresponding to the RAS states q 16 and q 17. Each of these two deadlocks can be eliminated from
the dynamics of the process-resource net by enforcing upon these dynamics the respective inequalities M (p 12) + M (p 21) # 1 and
M (p 11) + M (p 22) # 1. It is also important to notice that each of these inequalities does not eliminate only the corresponding deadlock
state, but also any other state that includes the considered deadlock; in this figure, the state subsets that are eliminated by each
of these two inequalities, are respectively indicated by the blue and the green blobs in the depicted STD. The two aforementioned
inequalities are enforced on the dynamics of the original process-resource net through the corresponding blue and green monitor
places that can be constructed using the theory in [35]. The augmented net that is obtained from the addition of these monitor
places remains an ordinary process-resource net, and therefore, its liveness and reversibility can still be tested through the absence of
empty siphons. The solution of the relevant MIP formulation reveals an empty siphon that corresponds to the unsafe state q 15, which
in the dynamics of the augmented process-resource net has turned into a policy-induced deadlock. This new empty siphon can be
eliminated through the imposition of the marking inequality M (p 11) + M (p 21) # 1, that is implemented by the red monitor place of
the depicted net. The evaluation of this new process-resource net through the corresponding MIP formulation reveals the absence of
any further empty siphons, and establishes its liveness and reversibility. It is also important to notice that the constructed monitors
eliminate all the unsafe states of the net while retaining all of its safe states. Hence, the augmented net depicted in the figure
constitutes a PN-based representation of the maximally permissive DAP for the RAS of Figure 1.

deadly marked siphons, then the assessment of the policy correctness can be performed automatically through the corresponding MIP formulation. The literature also avails of endeavors for an incremental synthesis of a correct DAP for a given
RAS, through: 1) the employment of the aforementioned MIPs
for the detection of deadly marked siphons in the relevant
reachability space (also known as potential deadlocks), 2) the
elimination of the identified potential deadlocks from the net
dynamics through a set of pertinent inequalities enforced on the
net marking by a set of monitor places, and 3) the (re)

assessment of the augmented net for absence of such badly
marked siphons. Clearly, if successful, such an approach can
provide a correct DAP for the considered RAS while avoiding
any explicit enumeration/exploration of the underlying state
space. In the case of disjunctive/conjunctive RAS with no
cycling in their process types and binary state spaces, such an
incremental synthesis has been shown to be capable of computing even the maximally permissive DAP [34]. In fact, the results
in [34] are applicable even in the case of disjunctive/conjunctive
RAS with binary state spaces and cyclic behavior for the RAS
June 2015

*

IEEE ROBOTICS & AUTOMATION MAGAZINE

*

91
Table of Contents for the Digital Edition of IEEE Robotics & Automation Magazine - June 2015
