This paper presents a novel method for optimal control of timed Petri nets, introducing a novel temporal logic based constraint called a generalized mutual exclusion temporal constraint (GMETC). The GMETC is described by a metric temporal logic (MTL) formula where each atomic proposition represents a generalized mutual exclusion constraint (GMEC). We formulate an optimal control problem of the timed Petri nets under a given GMETC and solve the problem by transforming it into an integer linear programming problem where the MTL formula is encoded by linear inequalities. We show the effectiveness of the proposed approach by a numerical simulation.

This paper proposes a Petri net based mathematical programming approach to combinatorial optimization, in which we generate integer linear programming problems from Petri net models instead of the direct mathematical formulation. We treat two types of combinatorial optimization problems, ordinary problems and time-dependent problems. Firstly, we present autonomous Petri net modeling for ordinary optimization problems, where we obtain fundamental constraints derived from Petri net properties and additional problem-specific ones. Secondly, we propose a colored timed Petri net modeling approach to time-dependent problems, where we generate variables and constraints for time management and for resolving conflicts. Our Petri net approach can drastically reduce the difficulty of the mathematical formulation in a sense that (1) the Petri net modeling does not require deep knowledge of mathematical programming and technique of integer linear model formulations, (2) our automatic formulation allows us to generate large size of integer linear programming problems, and (3) the Petri net modeling approach is flexible for input parameter changes of the original problem.

This paper proposes a scheme for automatic generation of mixed-integer programming problems for scheduling with multiple resources based on colored timed Petri nets. Our method reads Petri net data modeled by users, extracts the precedence and conflict relations among transitions, information on the available resources, and finally generates a mixed integer linear programming for exactly solving the target scheduling problem. The mathematical programing problems generated by our tool can be easily inputted to well-known optimizers. The results of this research can extend the usability of optimizers since our tool requires just simple rules of Petri nets but not deep mathematical knowledge.

In this paper, we proposed reduction operators of timed Petri net for efficient model checking. Timed Petri nets are used widely for modeling and analyzing systems which include time concept. Analysis of the system can be done comprehensively with model checking, but there is a state-space explosion problem. Therefore, previous researchers proposed reduction methods and translation methods to timed automata to perform efficient model checking. However, there is no reduction method which consider observability and there is a trade-off between the amount of description and the size of state space. In this paper, first, we have defined a concept of timed behavioral inheritance. Next, we have proposed reduction operators of timed Petri nets based on timed behavioral inheritance. Then, we have applied our proposed operators to an artificial timed Petri net. Moreover, the results show that the reduction operators which consider observability can reduce the size of state space of the original timed Petri nets within the experiment.

A timed Petri net, an extended model of an ordinary Petri net with introduction of discrete time delay in firing activity, is practically useful in performance evaluation of real-time systems and so on. Unfortunately though, it is often too difficult to solve (efficiently) even most basic problems in timed Petri net theory. This motivates us to do research on analyzing complexity of Petri net problems and on designing efficient and/or heuristic algorithms. The minimum initial marking problem of timed Petri nets (TPMIM) is defined as follows: “Given a timed Petri net, a firing count vector X and a nonnegative integer π, find a minimum initial marking (an initial marking with the minimum total token number) among those initial ones M each of which satisfies that there is a firing scheduling which is legal on M with respect to X and whose completion time is no more than π, and, if any, find such a firing scheduling.” In a production system like factory automation, economical distribution of initial resources, from which a schedule of job-processings is executable, can be formulated as TPMIM. The subject of the paper is to propose two pseudo-polynomial time algorithms TPM and TMDLO for TPMIM, and to evaluate them by means of computer experiment. Each of the two algorithms finds an initial marking and a firing sequence by means of algorithms for MIM (the initial marking problem for non-timed Petri nets), and then converts it to a firing scheduling of a given timed Petri net. It is shown through our computer experiments that TPM has highest capability among our implemented algorithms including TPM and TMDLO.

In our privious paper, we proposed an algorithm that determines delay times of a timed Petri net from the structural information of a signaling pathway, but Petri net structures containing cycles and inhibitory arcs were not considered. This paper provides conditions for cycle-contained Petri nets to have reasonable delay times. Furthermore, handling of inhibitory arcs are discussed in terms of the reaction rate of inhibitory interaction in signaling pathway, especially the conversion process of Petri net with inhibitory arc to the one without inhibitory arc is given.

There are various existing methods translating timed Petri nets to timed automata. However, there is a trade-off between the amount of description and the size of state space. The amount of description and the size of state space affect the feasibility of modeling and analysis like model checking. In this paper, we propose a new translation method from timed Petri nets to timed automata. Our method translates from a timed Petri net to an automaton with the following features: (i) The number of location is 1; (ii) Each edge represents the firing of transition; (iii) Each state implemented as clocks and variables represents a state of the timed Petri net one-to-one correspondingly. Through these features, the amount of description is linear order and the size of state space is the same order as that of the Petri net. We applied our method to three Petri net models of signaling pathways and compared our method with existing methods from the view points of the amount of description and the size of state space. And the comparison results show that our method keeps a good balance between the amount of description and the size of state space. These results also show that our method is effective when checking properties of timed Petri nets.

In computer science, concepts of resource such as data consumption and of time such as execution time are very important. Logical systems which can treat them have been applied in that field. Linear logic has been called a resource conscious logic. The expressive power is enough to describe a dynamic change in process environments. However, linear logic is not enough to treat a dynamic change in environments with the passage of time since it does not include a concept of time directly. A typical example is the relation between linear logic and Petri nets. It is well known that the reachability problem for Petri nets is equivalent to the provability for the corresponding sequent of linear logic. But linear logic cannot naturally represent timed Petri nets which are extensions of ordinary Petri nets with respect to time concept. So we extend linear logic with respect to time concept in order to introduce a resource-conscious and time-dependent logical system, that is, temporal linear logic. This system has some temporal operators "" which means a resource usable only once at the next time, "" which means a resource usable only once at anytime, and a modal storage operator "!" which means a resource usable any times at anytime. We can show that the reachability problem for timed Petri nets is equivalent to the provability for the corresponding sequent of temporal linear logic. In this paper, we also represent the description of synchronous communication model by temporal linear logic. The expressive power of temporal linear logic will be applicable to various fields of computer science.

In scheduling problem for automatic assembly, planning of task sequence is closely related with resource allocation. However, they have been separately carried out with little interaction in previous work. In assembly planning problem, there are many feasible sequences for one mechanical product. In order to find the best assembly sequence, we have to decide the cost function for each task a priori and make decision based on summation of costs in sequence. But the cost of each task depends on the machine which executes the allocated task and it becomes difficult to estimate an exact cost of each task at planning stage. Moreover, no concurrent operation is taken into account at planning stage. Therefore, we must consider the sequence planning and the machine allocation simultaneously. In this paper, we propose a new scheduling method in which sequence planning and machine allocation are considered simultaneously. First of all, we propose a modeling method for an assembly sequence including a manufacturing environment. Secondly, we show a guideline in order to determine the estimate function in A* algorithm for assembly scheduling. Thirdly, a new search method based on combination of A* algorithm and supervisor is proposed. Fourthly, we propose a new technique which can take into consider the repetitive process in manufacturing system so as to improve the calculation time. Finally, numerical experiments of proposed scheduling algorithm are shown and effectiveness of proposed algorithm is verified.

Estimating the deadline of a real-time task is a necessary prerequisite to the applications that have strict timing constraints, such as real-time systems design. This paper shows how Monte-Carlo simulation can be used as a space-efficient way of analyzing Timed Petri nets to predict whether the system specified can satisfy its real-time deadlines. For the purpose, Extended Timed Petri Net (XTPN), an extension of conventional Timed Petri net, and its execution rule, using Monte-Carlo technique, are newly defined. A simple simulation scheme with less memory space is presented as a way of estimating the deadline of a real-time task modeled in XTPN. And the comparison between the analytical and simulation results is given. The problem addressed here is to find the probabilities of meeting given deadlines.

In this paper, we show that by suitably selecting a notation to construct synchronization requirement specifications (SRS) for multimedia presentation we can express the timing characteristics at an abstract level, verify the specification, and obtain a hardware implementation through a sequence of transformations of the specification. First, we introduce the notion of a well-formed SRS and its hardware model. Second, we model an SRS as a timed Petri net and interpret the transitions of the net as hardware signals. To obtain logic functions from the SRS, we simplify the net and obtain a signal transition graph satisfying the unique state coding property. Finally, we show how to obtain a logic-level design of synchronizers.

The subject of the paper is the minimum initial marking problem for scheduling in timed Petri net PN: given a vector X of nonnegative integers, a P-invariant Y of PN and a nonnegative integer π, find an initial marking M minimizing the value YtrM among those initial marking M such that there is a scheduling σ having the total completion time τ(σ)π with respect M , X and PN (a sequence of transitions, with the first transition firable on M , such that every transition t can fire prescribed number X(t) of times). The paper shows NP-hardness of the problem and proposes two approximation algorithms with their experimental evaluation.

The subject of the paper is to propose two approximation algorithms FM_SPLA, FM_DPLA for priority-list scheduling in timed Petri nets. Their capability is compared with that of existing algorithms SPLA, DPLA through experimental results, where SPLA and DPLA have previously been proposed by the authors.