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.

Effective emergency resource allocation is essential to guarantee a successful emergency disposal, and it has become a research focus in the area of emergency management. Emergency event logs are accumulated in modern emergency management systems and can be analyzed to support effective resource allocation. This paper proposes a novel approach for efficient emergency resource allocation by mining emergency event logs. More specifically, an emergency event log with various attributes, e.g., emergency task name, emergency resource type (reusable and consumable ones), required resource amount, and timestamps, is first formalized. Then, a novel algorithm is presented to discover emergency response process models, represented as an extension of Petri net with resource and time elements, from emergency event logs. Next, based on the discovered emergency response process models, the minimum resource requirements for both reusable and consumable resources are obtained, and two resource allocation strategies, i.e., the Shortest Execution Time (SET) strategy and the Least Resource Consumption (LRC) strategy, are proposed to support efficient emergency resource allocation decision-making. Finally, a chlorine tank explosion emergency case study is used to demonstrate the applicability and effectiveness of the proposed resource allocation approach.

Business process similarity measure is required by many applications, such as business process query, improvement, redesign, and etc. Many process behavior similarity measures have been proposed in the past two decades. However, to the best of our knowledge, most existing work only focuses on the direct causality transition relations and totally neglect the concurrent and transitive transition relations that are proved to be equally important when measuring process behavior similarity. In this paper, we take the weakness of existing process behavior similarity measures as a starting point, and propose a comprehensive approach to measure the business process behavior similarity based on the so-called Extended Transition Relation set, ETR-set for short. Essentially, the ETR-set is an ex-tended transition relation set containing direct causal transition relations, minimum concurrent transition relations and transitive causal transition relations. Based on the ETR-set, a novel process behavior similarity measure is defined. By constructing a concurrent reachability graph, our approach finds an effective technique to obtain the ETR-set. Finally, we evaluate our proposed approach in terms of its property analysis as well as conducting a group of control experiments.

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.

For a service-oriented architecture based system, the problem of synthesizing a concrete model, i.e., behavioral model, for each service configuring the system from an abstract specification, which is referred to as choreography, is known as the choreography realization problem. In this paper, we assume that choreography is given by an acyclic relation. We have already shown that the condition for the behavioral model is given by lower and upper bounds of acyclic relations. Thus, the degree of freedom for behavioral models increases; developing algorithms of synthesizing an intelligible model for users becomes possible. In this paper, we introduce several metrics for intelligibility of state machines, and study the algorithm of synthesizing Pareto efficient state machines.

This paper presents the formal analysis of the feature negotiation and connection management procedures of the Datagram Congestion Control Protocol (DCCP). Using state space analysis we discover an error in the DCCP specification, that result in both ends of the connection having different agreed feature values. The error occurs when the client ignores an unexpected Response packet in the OPEN state that carries a valid Confirm option. This provides an evidence that the connection management procedure and feature negotiation procedures interact. We also propose solutions to rectify the problem.

In the classical computation theory, the language of a system features the computational behavior of the system but it does not distinguish the determinism and nondeterminism of actions. However, Milner found that the determinism and nondeterminism affect the interactional behavior of interactive systems and thus the notion of language does not features the interactional behavior. Therefore, Milner proposed the notion of (weak) bisimulation to solve this problem. With the development of internet, more and more interactive systems occur in the world, such as electronic trading system. Security is one of the most important topics for these systems. We find that different security policies can also affect the interactional behavior of a system, which exactly is the reason why a good policy can strengthen the security. In other words, two interactive systems with different security policies are not of an equivalent behavior although their functions (or business processes) are identical. However, the classic (weak) bisimulation theory draws an opposite conclusion that their behaviors are equivalent. The notion of (weak) bisimulation is not suitable for these security-oriented interactive systems since it does not consider a security policy. This paper proposes the concept of secure bisimulation in order to solve the above problem.

Time performance optimization and resource conflict resolution are two important challenges in multiple project management contexts. Compared with traditional project management, multi-project management usually suffers limited and insufficient resources, and a tight and urgent deadline to finish all concurrent projects. In this case, time performance optimization of the global project management is badly needed. To our best knowledge, existing work seldom pays attention to the formal modeling and analyzing of multi-project management in an effort to eliminate resource conflicts and optimizing the project execution time. This work proposes such a method based on PRT-Net, which is a Petri net-based formulism tailored for a kind of project constrained by resource and time. The detailed modeling approaches based on PRT-Net are first presented. Then, resource conflict detection method with corresponding algorithm is proposed. Next, the priority criteria including a key-activity priority strategy and a waiting-short priority strategy are presented to resolve resource conflicts. Finally, we show how to construct a conflict-free PRT-Net by designing resource conflict resolution controllers. By experiments, we prove that our proposed priority strategy can ensure the execution time of global multiple projects much shorter than those without using any strategies.

A service-oriented architecture builds the entire system using a combination of independent software components. Such an architecture can be applied to a wide variety of computer systems. The problem of synthesizing service implementation models from choreography representing the overall specifications of service interaction is known as the choreography realization problem. In automatic synthesis, software models should be simple enough to be easily understood by software engineers. In this paper, we discuss a semi-formal method for synthesizing hierarchical state machine models for the choreography realization problem. The proposed method is evaluated using metrics for intelligibility.

Petri nets are a kind of formal language that are widely applied in concurrent systems associated with resource allocation due to their abilities of the natural description on resource allocation and the precise characterization on deadlock. Weighted System of Simple Sequential Processes with Resources (WS3PR) is an important subclass of Petri nets that can model many resource allocation systems in which 1) multiple processes may run in parallel and 2) each execution step of each process may use multiple units from a single resource type but cannot use multiple resource types. We first prove that the liveness problem of WS3PR is co-NP-hard on the basis of the partition problem. Furthermore, we present a necessary and sufficient condition for the liveness of WS3PR based on two new concepts called Structurally Circular Wait (SCW) and Blocking Marking (BM), i.e., a WS3PR is live iff each SCW has no BM. A sufficient condition is also proposed to guarantee that an SCW has no BM. Additionally, we show some advantages of using SCW to analyze the deadlock problem compared to other siphon-based ones, and discuss the relation between SCW and siphon. These results are valuable to the further research on the deadlock prevention or avoidance for WS3PR.

A Boolean network model is one of the models of gene regulatory networks, and is widely used in analysis and control. Although a Boolean network is a class of discrete-time nonlinear systems and expresses the synchronous behavior, it is important to consider the asynchronous behavior. In this paper, using a Petri net, a new modeling method of asynchronous Boolean networks with control inputs is proposed. Furthermore, the optimal control problem of Petri nets expressing asynchronous Boolean networks is formulated, and is reduced to an integer programming problem. The proposed approach will provide us one of the mathematical bases of control methods for gene regulatory networks.

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.

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.

Many Petri nets-based methods have been developed and applied to analyze cryptographic protocols. Most of them offer the analysis of one attack trace only. Only a few of them provide the analysis of multiple attack traces, but they are rather inefficient. Similarly, the limitation of the analysis of one attack trace occurs in most model checking methods for cryptographic protocols. Recently, we proposed a simple but practical Petri nets-based model checking methodology for the analysis of cryptographic protocols, which offers an efficient analysis of all attack traces. In our previous analysis, we assume that the underlying cryptographic algorithms are black boxes, and attackers cannot learn anything from cipher text if they do not have a correct key. In this paper, we relax this assumption by considering some algebraic properties of the underlying encryption algorithm. Then, we apply our new method to TMN authenticated key exchange protocol as a case study. Surprisingly, we obtain a very efficient analysis when the numbers of attack traces and states are large, and we discover two new attacks which exploit the algebraic properties of the encryption.

The marking construction problem (MCP) of Petri nets is defined as follows: “Given a Petri net N, an initial marking Mi and a target marking Mt, construct a marking that is closest to Mt among those which can be reached from Mi by firing transitions.” MCP includes the well-known marking reachability problem of Petri nets. MCP is known to be NP-hard, and we propose two schemas of heuristic algorithms: (i) not using any algorithm for the maximum legal firing sequence problem (MAX LFS) or (ii) using an algorithm for MAX LFS. Moreover, this paper proposes four pseudo-polynomial time algorithms: MCG and MCA for (i), and MCHFk and MC_feideq_a for (ii), where MCA (MC_feideq_a, respectively) is an improved version of MCG (MCHFk). Their performance is evaluated through results of computing experiment.

Interrupt service routines are a key technology for embedded systems. In this paper, we introduce the standard approach for using Generalized Stochastic Petri Nets (GSPNs) as a high-level model for generating CTMC Continuous-Time Markov Chains (CTMCs) and then use Markov Reward Models (MRMs) to compute the performance for embedded systems. This framework is employed to analyze two embedded controllers with low cost and high performance, ARM7 and Cortex-M3. Cortex-M3 is designed with a tail-chaining mechanism to improve the performance of ARM7 when a nested interrupt occurs on an embedded controller. The Platform Independent Petri net Editor 2 (PIPE2) tool is used to model and evaluate the controllers in terms of power consumption and interrupt overhead performance. Using numerical results, in spite of the power consumption or interrupt overhead, Cortex-M3 performs better than ARM7.

Invariants of Petri nets are fundamental algebraic characteristics of Petri nets, and are used in various situations, such as checking (as necessity of) liveness, boundedness, periodicity and so on. Any given Petri net N has two kinds of invariants: a P-invariant is a |P|-dimensional vector Y with Yt A = and a T-invariant is a |T|-dimensional vector X with A X = for the place-transition incidence matrix A of N. T-invariants are nonnegative integer vectors, while this is not always the case with P-invariants. This paper deals only with nonnegative integer invariants (invariants that are nonnegative vectors) and shows results common to the two invariants. For simplicity of discussion, only P-invariants are treated. The Fourier-Motzkin method is well-known for computing all minimal support integer invariants. This method, however, has a critical deficiency such that, even if a given Perti net N has any invariant, it is likely that no invariants are obtained because of an overflow in storing intermediate vectors as candidates for invariants. The subject of the paper is to give an overview and results known to us for efficiently computing minimal-support nonnegative integer invariants of a given Petri net by means of the Fourier-Motzkin method. Also included are algorithms for efficiently extracting siphon-traps of a Petri net.

The minimum initial marking problem of Petri nets (MIM) is defined as follows: "Given a Petri net and a firing count vector X, find an initial marking M0, with the minimum total token number, for which there is a sequence δ of transitions such that each transition t appears exactly X(t) times in δ, the first transition is enabled at M0 and the rest can be fired one by one subsequently." 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 MIM. AAD is known to produce best solutions among existing algorithms. Although solutions by AMIM+ is worse than those by AAD, it is known that AMIM+ is very fast. This paper proposes new heuristic algorithms AADO and AMDLO, improved versions of existing algorithms AAD and AMIM+, respectively. Sharpness of solutions or short CPU time is the main target of AADO or AMDLO, respectively. It is shown, based on computing experiment, that the average total number of tokens in initial markings by AADO is about 5.15% less than that by AAD, and the average CPU time by AADO is about 17.3% of that by AAD. AMDLO produces solutions that are slightly worse than those by AAD, while they are about 10.4% better than those by AMIM+. Although CPU time of AMDLO is about 180 times that of AMIM+, it is still fast: average CPU time of AMDLO is about 2.33% of that of AAD. Generally it is observed that solutions get worse as the sizes of input instances increase, and this is the case with AAD and AMIM+. This undesirable tendency is greatly improved in AADO and AMDLO.

Communication-free Petri nets provide a net semantics for Basic Parallel Processes, which form a subclass of Milner's Calculus of Communicating Systems (CCS) a process calculus for the description and algebraic manipulation of concurrent communicating systems. It is known that the reachability problem for communication-free Petri nets is NP-complete. Lacking the synchronization mechanism, the expressive power of communication-free Petri nets is somewhat limited. It is therefore importance to see whether the power of communication-free Petri nets can be enhanced without sacrificing their analytical capabilities. As a first step towards this line of research, in this paper our main concern is to investigate, from the decidability/complexity viewpoint, the reachability problem for a number of variants of communication-free Petri nets, including communication-free Petri nets augmented with 'static priorities,' 'dynamic priorities,' 'states,' 'inhibitor arcs,' and 'timing constraints.'

Petri nets are known as a modeling language for concurrent and distributed systems. In recent years, various object-oriented Petri nets were proposed, and we are proposing a kind of object-oriented Petri nets, called multi agent nets (MANs). In this letter, we consider the reachability analysis of MANs. We propose an algorithm for generating an abstract state space of a multi agent net, and report results of computational experiments.