First posted on Sep 2, 1997.
Last revised on Oct 5, 1999.
1997 (C) Copyright by Atsushi Ohta.
All rights reserved.
ohta@ist.aichi-pu.ac.jp
This paper treats computational complexity of bounded asymmetric choice (AC) net. AC net is a subclass of Petri net that properly includes the class of well-known extended free choice net. It is shown that satisfiability problem of Boolean expressions is polynomial time reducible to liveness problem of bounded AC nets. This implies that the problem is NP-hard.
Petri net is a mathematical model for concurrent systems. Liveness is one of important properties of Petri net. Liveness problem of general Petri net is of exponential space complexity and subclasses are suggested with less computational complexity. It is well known that liveness problem of bounded (extended) free choice net is solved in deterministic polynomial time. This paper treats liveness problem of AC/DC nets. AC/DC net is a subclass of Petri net that exhibits no confusion (mixture of concurrency and conflict). This class properly includes the class of free choice nets. It is shown that every minimal siphon of an AC/DC net is trap if and only if every strongly connected siphon is a trap. This result shows that monotone liveness of bounded AC/DC net is solved in deterministic polynomial time. It is shown that this result is true of bounded \textcolor{ref1}{time} AC/DC net with static fair condition.
Petri net is a mathematical model for concurrent systems. Petri net is known to have less modeling power than that of Turing machine. Lack of zero testing ability is the main reason of this fact. Indeed, every extended Petri net model that can perform zero testing is equivalent to Turing machine. Time Petri net is one of the models with ability of zero testing. It is of theoretical interest what structure enables zero testing. This paper shows that time asymmetric choice net can simulate register machines. The result implies reachability problem of this subclass of time Petri net is undecidable.
This paper treats analysis problems of time Petri nets. In this model, a minimal and a maximal firing delays are assigned to each transition. If a transition is `enabled' it can fire after minimal delay has passed and must fire before maximal delay has elapsed. Since time Petri net can simulate register machines, it has equivalent modeling power to that of Turing machine. It means, however, that most of the analysis problems of time Petri nets with general net structures are undecidable. In this paper, net structures are restricted to a subclass called partially ordered condition (POC) nets and dissynchronous choice (DC) nets. Firing delays are also restricted to satisfy `static fair condition' which assures chance to fire for all transitions enabled simultaneously. First, a sufficient condition of liveness of time POC net with the static fair condition is derived. Then it is shown that liveness of time DC net with static fair condition is equivalent to liveness of the underlying nontime net. This means that liveness problem of this class is decidable. Lastly, liveness problem of extended free choice (EFC) net is shown to be decidable.
Silva et al has suggested a criterion based on incidence matrix to verify if a given extended free choice net has a live and bounded marking. This paper shows that this criterion is a necessary and sufficient condition that a given net is a state machine allocatable (SMA) net. This result gives a polynomial algorithm to verify SMA net.
This paper treats analysis problems for Petri nets under the earliest firing rule. First, some relations in analysis problems between the earliest and the normal firing systems are discussed. Then, relation among three types of reachability are considered from the viewpoint of the earliest firing rule. Since earliest firing systems can simulate register machines, they have equivalent modeling powers to Turing machines. In this paper, net structures are restricted to a subclass called dissynchronous choice (DC) nets. It is shown that the reachability problem from an initial marking to dead markings (markings where no transition can fire) in earliest firing DC systems is equivalent to the usual reachability problem of the same systems under the normal firing rule.
In this paper we discuss the liveness of extended subclasses of Petri net, that is, strongly connected marked graphs and strongly connected state machines in which permission or inhibitor arcs are added in restricted structures. The addition of these arcs facilitate modeling of practical discrete event systems by the net. The necessary and/or sufficient conditions for liveness are derived for above subclasses. The the computational complexities to verify liveness of these nets are discussed and it is shown that liveness of the above subclasses can be verified in deterministic polynimial time by the applications of the obtained criteria.
Petri net is a model for discrete event systems which has modeling power more than finite automaton and less than Turing machine. We show that Petri net with single-weighted arcs can simulate Turing machine under free firng rule.
We treat liveness problems of the timed Petri nets which have shared resource places and obey the earliest firing rule. In general, liveness of a usual Petri net is neither necessary nor sufficient condition for liveness of the Petri net with sahred resource under the earliest firing rule. The relations between above two cases are clarified for some subclasses.
This paper clarifies a relation between `normal' liveness of Petri nets and liveness of the net under the earliest firing rule. POC nets, a subclass of Petri nets where normal liveness is a sufficient condition for liveness under the earliest firing rule are proposed. The conditions for necessity are investigated, considering the two rules for multiple firing of a single transition, that is, single servers and infinite servers. This provides a subclass where the two forementioned livenesses are equivalent to each other. Finally, computational complexity for liveness problem is considered.
This paper suggests a new subclass of Petri net, POC nets, as a superclass of AC nets and DC nets. For this subclass, the equivalence between liveness and place-liveness is shown and a sufficient condition for liveness for this POC net is derived. Then the results are extended to liveness problem of timed Petri nets which have transitions with finite firing durations and the earliest firing rule. Although liveness of a non-timed Petri net is neither necessary nor sufficient condition for liveness of a timed Petri net, it is shown that liveness is preserved if the net has POC structure.
Petri net is a powerful tool for modeling, analysis and performance evaluation of dicrete event systems. Liveness is one of the most important properties in Petri net analysis. It is not always true that liveness is monotone with respect to the increase of the initial token count. In this paper, a necessary condition for monotonicity of liveness is derived. Furthermore, subclasses in which this condition is also a sufficient one are investigated.
It was shown that computational complexity of reachbility problem of marked graph is nondeterministic logarithmic space hard, which gives a lower bound of the complexity. Based on Murata's results on marked graphs, this paper shows that this problem can be solved in deterministic polynomial time to show a good upper bound. Moreover reachability problem in which initial or target marking is unbounded is considered.
Job-shop type, time optimal scheduling problems for repetitive processes are modeled by the Petri net with timed places. Assuming the stationary periodic solution, the optimal or the sub-optimal solution is obtained by linear programming and the brance and bound method.
In this paper, we investigate a time optimal job shop type scheduling problem including jobs with uncertain processing times. Modeling the problem by the stochastic time Petri net in which some transitions have statistically varying firing times, we derived the stocastically suboptimal (non-delayed) schedule. The approach is illustrated by two examples and the results are compared with those of Monte Carlo simulations.
Petri net is an effective tool to model and evaluate concurrent systems. Colored Petri net has been proposed to model large scale systems more effectively. Among analysis tools for colored Petri nets, such as reachability tree, to net invariants, to unfolded equivalent noncolored net, we use underlying noncolored Petri net. This method requires restriction on binding of the arc expression. In this report, some analysis properties of colored Petri net are studied using its underlying noncolored net. Sufficient conditions for boundedness and persistency are derived. Some restrictions on structure and binding are used to obtain a necessary condition for liveness.
Petri net is a mathematical model for concurrent systems. Liveness is one of important properties of Petri net. Siphon and trap are effective tools for liveness analysis. Existence of a token free siphon is a sufficient condition for nonliveness. Authors has suggested insufficiently marked siphon as an extension of token free siphon. On the other hand, siphon and trap are also used to derive necessary condition for liveness monotonicity. In this report we show stronger necessary condition using insufficiently marked siphons.
Petri net is an effective model for concurrent systems. State space of a general Petri net is infinite. Even if it is finite, its size grows exponentially as the size of the net does. This problem, called state space explosion, makes Petri net analysis hard. Unfolding is suggested to give a compact description of the state space of a bounded Petri net. This is extended to unbounded net using symbol ω used in the coverability tree generating algorithm. However, using ω causes lack of information. On the other hand, if unbounded Petri net has a semilinear state space, it can be expressed without lack of information with extended coverability tree. This paper suggests an extension of unfolding of Petri net with semilinear state space without lack of information.
Petri net is a mathematical model for concurrent systems. Liveness is one of important properties of Petri net. A live Petri net exhibits no local deadlocks. Siphon is a subset of places useful for liveness analysis. Token-free siphon implies non-liveness of Petri net. In this report, we suggest an insufficiently marked siphon as an extended token-free siphon. More general necessary condition for liveness is obtained using this new status of siphons. Two methods are proposed to obtain an insufficiently marked siphon.
This report considers the relation between analysis problems of Merlin's time Petri net and nontime Petri net with the identical structure. A necessary and sufficient condition for liveness of time free choice net is derived. Lastly, subclasses where timed liveness problem can be solved in deterministic polynomial time are shown.
This paper studies analysis of Petri net extended with batch processing arcs. If a batch processing arc is connected from a place p to a transition t,firing of t removes all tokens in p. Turing machine equivalence and liveness condition of subclasses of batch Petri net are shown.
Fuzzy timing Petri net has been suggested to introduce time without spoiling concurrency. This paper shows a formal definition of fuzzy timing Petri net. Then some problem concerning concurrency in fuzzy timing Petri net is pointed out and modification is suggested to cope with the problem.
Petri net is an effective modeling tool for concurrent systems. Liveness problem is one of analysis problems in Petri net theory verifying whether the system is free from any local deadlocks. It is well-known that computational complexity of liveness problem of general Petri net is deterministic exponential space. This paper studies reduction method of Petri net that preserves liveness property to cope with computational complexity. The reduction is done by deletion of a place. This result also derives a subclass of Petri net of which liveness problem is NP-complete.
Petri net is an effective modeling tool for concurrent systems. Liveness problem is one of analysis problems in Petri net theory verifying whether the system is free from any local deadlocks. It is well known that computational complexity of liveness problem of general Petri net is deterministic exponential space. Some subclasses, such as marked graph and free choice net, are suggested where liveness problem is verified in less complexity. This paper studies liveness of siphon containing circuit (SCC) net. Liveness condition based on algebraic inequalities is shown. Then polynomial time decidability of liveness of SCC net is derived, if the given net is known to be an SCC net a priori.
Petri net is an effective modeling tool for concurrent systems. Liveness problem is one of analysis problems in Petri net theory verifying whether the system is free from any local deadlocks. It is well known that computational complexity of liveness problem of general Petri net is deterministic exponential space. Some subclasses, such as marked graph and free choice net, are suggested where liveness problem is verified in less complexity. This paper studies liveness of ESAC net. ESAC net is a super class of free choice net suggested by Li et al. It is shown that liveness problem is NP-complete for ESAC systems where every place has at most two output transitions.
This paper studies coverability tree and reachability set of Petri net under the earliest firing rule. Conventional algorithm for coverability tree for `normal' Petri net is not good for Petri net under the earliest firing rule. Moreover, it is shown that there exists no coverability graph for general class of earliest firing Petri net. Some subclasses are studied where coverability graph can be constructed.
Petri is an efficient modeling tool for discrete event systems. Liveness is one of analysis problems of Petri nets, which concerns with potential possibility of occurrence of events. Some subclasses of Petri net are suggested with their liveness conditions. In this report, liveness of a subclass named extended partially ordered condition (EPOC) nets is studied. First, equivalence of liveness and place-liveness is proved under the normal firing rule. Then a necessary and sufficient condition of liveness is derived. These results are true for the earliest firing rule and this gives a sufficient condition of an earliest firing EPOC net.
This report treats the reachability problem of controlled earliest firing Petri nets. In the controlled Petri net, some transitions are controllable and they have their external input place. The firings of these transitions are controlled by putting token(s) in these places. `Strict reachability problem' is to verify whether the target marking is reachable with some appropriate control from every reachable state. In this report strict reachability problems of some subclasses are considered.
This paper treats reachability problems of time Petri nets. In this model, a minimal and a maximal firing delays are assigned to each transition. It is known that time Petri net has equivalent modeling power to that of Turing machine. It means, however, that most of the analysis problems of time Petri nets with general net structures are undecidable. In this paper, net structures are restricted to a subclass called dissynchronous choice (DC) nets. Firing delays are also restricted to satisfy `static fair condition' which ensures chance to fire for all transitions enabled simultaneously. It is shown that if the target marking is a dead one, reachability of time DC net with static fair condition is equivalent to that of the underlying nontime net. This result can applied to controlled DC net and EFC net.
We suggest two subclasses of Petri nets, DOSI net and DISO net, and investigate liveness of timed Petri nets with these structures.
We consider the conditions for the liveness of some subclasses of Petri nets with limitation of token capacities on places. Then the computational complexity to verify the liveness is discussed, and it is shown that under this limitation, liveness of state machine, marked graph, strongly connected conflict-free net and non-decreasing cycle net can be decided in deterministic polynomial time.
Job-shop type scheduling problems, where tasks are processed by several processors in their own orders and the aim is to assign the tasks to the processors in order to minimize (or maximize) given objective functions, have wide range of applications. In this paper, we use timed marked graphs to model repetitive job-shop type scheduling problems and suggest an approximate algorithm to minimize period.
Although boundedness of a Petri net under the `normal' firing rule is a sufficient condition for boundedness of the net under the earliest firing rule, it is not a necessary condition. Furthermore, the boundedness problem of Petri nets under the earliest firing rule is undecidable. We consider boundedness problems of some subclasses of Petri nets under the earliest firing rule.
Addition of permission or inhibitor arcs to a Petri net enhances its modeling power but affects its liveness property. Following our previous reports on the liveness of extended subclasses of strongly connected marked graphs and strongly connected state machines (SCSM) which have permission arcs or inhibitor arcs in restricted structures, we study in this paper the liveness problem of combined systems which consist of nets of the above extended subclasses.
Timed Petri net is an effective tool to evaluate discrete event systems. This report treats the reachability problem of timed Petri nets. The problem aims to find the firing sequence which drives the initial marking to the target marking in minimal execution time. First, we consider the subclass in which the earliest firing rule gives the optimal solution. Then, an algorithm is proposed to solve the minimal time reachability problem of timed state machines.
Performance evaluation of timed marked graphs is a well-studied problem of timed Petri nets. This paper extends the problem to marked graphs with permission arcs. Two approximate algorithms are presented concerning the minimal initial marking problem that enables an admissible periodic behavior of the net.
Silva et al. has suggested a criterion based on incidence matrix to verify given extended free choice net has a live and bounded marking. This paper shows that this criterion is a necessary and sufficient condition that given net is a state machine allocatable (SMA) net. This result gives a polynomial algorithm to verify SMA net.
Monotonicity of liveness is considered, which assures liveness when one adds arbitrary numbers of tokes to the live net. We have suggested a necessary condition for monotonicity of liveness so far. In this report, we show a sufficient condition for this property, applying a new method based on the release of arcs.
The reachability problem and the liveness problem of Petri nets are equivalent, in the sense that they are reducible to each other. They are known to be decidable. The earliest firing Petri nets, where transitions must fire as soon as they become enabled, have equivalent modeling powers to that of Turing machines. This implies that analysis problems as reachability and liveness are undecidable. In this report, mutual reducibility of analysis ploblems of earliest firing Petri nets is investigated.
This report treats a liveness problem of Merlin's time Petri net, where transitions have minimum and maximum time delays for firing. This net has equivalent modeling powers to that of Turing machine. Necessary and sufficient conditions for liveness are derived for the nets with restricted structures.
A siphon is said to be controlled if it has taoke(s) at every reachable state. If a Petri net is live, every siphon is controlled. This report extends the results on controlled siphons. A sufficient condition using invariants is extended, so that is it necessary for extended free choice nets. An algorithm to obtain partition to check uncontrollable siphon is suggested.
This report treats the liveness problem of Merlin's time Petri nets, where each transition has minimal and maximal firing delays after it is enabled. This time Petri net is proved to be equivalent to Turing machines. That means analysis problems of this extended net are undecidable. This report shows that time POC(partially ordered condition) net is live under some restriction of firing delays of transitions, if the corresponding non-timed net is live .
This report suggests an algorithm to minimize the period in the given repetitive job-shop type scheduling problem. The problem is modeled with a timed marked graph and is reduced to minimal initial marking problem of the net. The approximate algorithm proposed by Laftit et al is used to avoid the combinatorial explosion. A method to specifying the input initial marking to the above algorithm is also considered to reduce the computational complexity. A computational experiment is shown to demonstrate the effectiveness of the algorithms in comparison with the strict algorithm.
This report shows that time partially ordered condition net is live under some restriction of firing delays of transitions, if the corresponding non-timed net is live.
This paper treats liveness problem of colored Petri net. We point out that in general liveness of colored Petri net is neither necessary condition nor sufficient condition of liveness of underlying noncolored net. Then we show some subclasses of colored Petri net where liveness of colored net is a sufficient condition for liveness of underlying noncolored net.
Most analysis problems of Petri net are decidable, however, need enormous computational complexity. It has been pointed out that exploding size of state space of Petri net is one of the reason of the complexity. Binary decision diagram has been used to describe the state space of Petri net in relatively small size. This report suggests a procedure to describe the state space of the earliest firing Petri net using a binary decision diagram.