Synthesis of Control Policies for Lossy Controlled Petri Nets

摘要

The forbidden state problem is to synthesize a control policy for preventing a Petri net from reaching any state in its forbidden set. In this paper, we address a liveness preserving version of the forbidden state problem for lossy Petri nets. During the process of keeping Petri nets out of the set of their forbidden states, a control policy does not disable a live marking. We present a method to solve the above problem based on fixed point computations. We show that for lossy Petri nets, the problem is decidable. From a practical viewpoint, the problem associated with our fixed point approach is 'state explosion.' In order to overcome this problem, we propose a symbolic approach, which uses Boolean functions for implicitly representing the set of states. We use Boolean functions for representing reachable markings. Thus OBDDs, compact representations of Boolean functions, can reduce the time and space involved in solving the forbidden state problem described in this paper.