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.
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Copy
Yih-Kai LIN, Cheng-Hong LI, Hsu-Chun YEN, "Synthesis of Control Policies for Lossy Controlled Petri Nets" in IEICE TRANSACTIONS on Fundamentals,
vol. E86-A, no. 7, pp. 1790-1798, July 2003, doi: .
Abstract: 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.
URL: https://global.ieice.org/en_transactions/fundamentals/10.1587/e86-a_7_1790/_p
Copy
@ARTICLE{e86-a_7_1790,
author={Yih-Kai LIN, Cheng-Hong LI, Hsu-Chun YEN, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={Synthesis of Control Policies for Lossy Controlled Petri Nets},
year={2003},
volume={E86-A},
number={7},
pages={1790-1798},
abstract={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.},
keywords={},
doi={},
ISSN={},
month={July},}
Copy
TY - JOUR
TI - Synthesis of Control Policies for Lossy Controlled Petri Nets
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 1790
EP - 1798
AU - Yih-Kai LIN
AU - Cheng-Hong LI
AU - Hsu-Chun YEN
PY - 2003
DO -
JO - IEICE TRANSACTIONS on Fundamentals
SN -
VL - E86-A
IS - 7
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - July 2003
AB - 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.
ER -