This paper develops a framework to support trace theoretic verification of timed circuits and systems. A theoretical foundation for classifying timed traces as either successes or failures is developed. The concept of the semimirror is introduced to allow conformance checking thus supporting hierarchical verification of timed circuits and systems. Finally, we relate our framework to those previously proposed for timing verification.

This letter 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.

In this paper, new integrated schemes of scheduling real-time traffic and cell loss control in high speed ATM networks are proposed for multiple priorities based on variable queue length thresholds for scheduling and the Partial Buffer Sharing policy for cell loss control. In our schemes, the queues for buffering arriving cells can be constructed in two ways: one individual queue for each user connection, or one physical queue for all user connections. The proposed schemes are considered to provide guaranteed QoS for each connection and cell sequence integrity for virtual channel/path characteristics. Moreover, these new schemes are quite flexible and can realize different scheduling algorithms. This paper also provides the Stochastic Petri Net models of these integrated schemes and an approximate analysis technique, which significantly reduces the complexity of the model solution and can be applied to real ATM switch models. From the numerical results, we can see that our schemes outperform those well-known schemes such as the head-of-line (HOL) priority control and the queue length threshold (QLT) policy.

Agent technology is widely recognized as a new paradigm for the design of concurrent software and systems. The aim of this paper is to give a mathematical foundation for the design and the analysis of multi-agent systems by means of a Petri-net-based model. The proposed model, called PN2, is based on place/transition nets (P/T nets), which is one of the simplest classes of Petri nets. The main difference of PN2's from P/T nets is that each token, representing an agent, is also a P/T net. PN2's are sufficiently simple for the mathematical analysis, such as invariant analysis, but have enough modeling power.

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 time AC/DC net with static fair condition.

The legal firing sequence problem of Petri nets (LFS) is one of fundamental problems in the analysis of Petri nets, because it appears as a subproblem of various basic problems. Since LFS is shown to be NP-hard, various heuristics has been proposed to solve the problem of practical size in a reasonable time. In this paper, we propose a new algorithm for this problem. It is based on the partial order verification technique, and reduces redundant branches in the search tree. Moreover, the proposed algorithm can be combined with various types of heuristics.

We consider only P-invariants that are nonnegative integer vectors in this paper. An P-invariant of a Petri net N=(P,T,E,α,β) is a |P|-dimensional vector Y with Yt A = for the place-transition incidence matrix A of N. The support of an invariant is the set of elements having nonzero values in the vector. Since any invariant is expressed as a linear combination of minimal-support invariants (ms-invariants for short) with nonnegative rational coefficients, it is usual to try to obtain either several invariants or the set of all ms-invariants. The Fourier-Motzkin method (FM) is well-known for computing a set of invariants including all ms-invariants. It has, however, critical deficiencies such that, even if invariants exist, none of them may be computed because of memory overflow caused by storing candidate vectors for invariants and such that, even when a set of invariants are produced, many non-ms invariants may be included. We are going to propose the following two methods: (1) FM1_M2 that finds a smallest possible set of invariants including all ms-invariants; (2) STFM that necessarily produces one or more invariants if they exist. Experimental results are given to show their superiority over existing ones.

A workflow is a flow of work carried out by workers, and workflow management is to automate the flow of work. In workflow management, an actual work is carried out based on the workflow, which is called case. In order to effectively meet various requirements, it is necessary to change current workflow dynamically, which is called dynamic workflow change. When the dynamic change is required, there exist cases in the workflow. In order to handle these cases and further to keep the queuing order, the dynamic change takes period of time (called transient time) until the changed workflow becomes steady state again. During the transient time, workers are forced to do irregular work, and therefore it is important to clarify if a change type takes shorter transient time. In this paper, we do the performance evaluation on transient time of dynamic workflow changes. To do so, we first give a definition of transient time, and then propose methods of computing transient time of three change types proposed by Ellis et al. Finally, we do the performance evaluation for 90 dynamic changes by computing the transient times.

This paper proposes a public-key cryptography by applying RSA and Petri nets. We introduce RSA and a Petri net based private-key cryptography and then taking the advantages of these two cryptography, we propose a new public-key cryptography, PNPKC. To compare with RSA on security as well as computation order, we do simulation experiments. As the results, the security of PNPKC is as strong as RSA cryptography, and the encryption and decryption of PNPKC are in average 239 times as fast as RSA cryptography from our experiments. Besides, to see if our current PNPKC program can be practically used, we do comparative experiment with PGP, which shows PNPKC takes computation time in average as much as 36 times of PGP cryptography. That means our PNPKC program still needs to be technically improved.

Adaptation of software components to the requirements is one of the key concerns in Component Based Software Development (CBSD). In this paper, we propose a formal approach to compose component based systems which are adaptable to the requirements. We focus on the functional aspects of software components and requirements, which are expressed in S-sorted functions. Those S-sorted functions are transformed into Colored Petri Nets (CPN) models in order to evaluate connectivity between the components, and to evaluate adaptability of composed systems to the requirements. The connectivity is measured based on colors or data types in CPN, while the adaptability is measured based on functional equivalency. We introduce simple glue codes to connect the components each other. The paper focuses on business applications, however the proposed approach can be applied to any other domains as far as the functional adaptability is concerned.

This paper proposes a new heuristic algorithm FMDB for the minimum initial marking problem MIM of Petri nets: "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 firable on M0 and the rest can be fired one by one subsequently. " Experimental results show that FMDB produces better solutions than any known algorithm.

It is one of the difficulties in enterprise modeling that we must deal with many fragmented pieces of knowledge provided by various domain-experts, which are usually based on mutually different viewpoints of them. This paper presents a formal approach to integrate those pieces into enterprise-wide model units using Rough Set Theory (RST). We focus on business processes in order to recognize and identify the constituents or units of enterprise models, which would compose the model expressing the various aspects of the enterprise. We defined five model unit types of "resource," "organization," "task," "function," and "behavior. " The first three types represent the static aspect of the enterprise, whereas the last two types represent the dynamic aspect of it. Those units are initially elicited from each domain-expert as his/her own individual model units, then they are integrated into enterprise-wide units using RST. Our approach is methodology-free, and any methodologies can include it in their early stage to identify what composes the enterprise.

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.

A workflow is a flow of work carried out in parallel and in series by people. In order to improve efficiency, it is required to change the current workflow dynamically. Since dynamic change of workflows may probably make the series of work inconsistent, it is necessary to find out consistent change of workflow. As consistent ways, three types of dynamic changes: flush, abort, and synthetic cut-over (SCO), have been proposed. However, the concrete analysis and evaluation have not been done. To do the performance evaluation for the dynamic workflow changes, comparison of the times (called change time) cost in the individual change and the methods how to obtain such times become ever important. In this paper, we first give a definition of change time and then propose the computation methods individually for each change type. Finally, we do experiments to evaluate the performance of three changes by doing the comparison of the change times.

Despite their attractive properties, networked virtual environments (net-VEs) are notoriously difficult to design, implement and test due to the concurrency, real-time and networking features in these systems. The current practice for net-VE design is basically trial and error, empirical, and totally lacks formal methods. This paper proposes to apply a Petri net formal modeling technique to a net-VE: NICE (Narrative Immersive Constructionist/Collaborative Environment), predict the net-VE performance based on simulation, and improve the net-VE performance. NICE is essentially a network of collaborative virtual reality systems called CAVE-(CAVE Automatic Virtual Environment). First, we present extended fuzzy-timing Petri net models of both CAVE and NICE. Then, by using these models and Design/CPN as the simulation tool, we have conducted various simulations to study real-time behavior, network effects and performance (latencies and jitters) of NICE. Our simulation results are consistent with experimental data.

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.

We introduce a high-level synthesis framework to automatically synthesize asynchronous circuits, especially speed-independent circuits, from a concurrent programming language called ALPEH. ALPEH is a high-level concurrent algorithmic specification that can model complex concurrent control flows, logical and arithmetic computations, and communications in easy way. This specification language has been developed to be translated into a Petri net. The major contribution of this paper is the generation of globally optimized control circuits during preserving neat formalism in the specification.

Generating state spaces is one of important and general methods in the analysis of Petri nets. There are two reasons why state spaces of Petri nets become so large. One is concurrent occurring of transitions, and the other is periodic occurring of firing sequences. This paper focuses on the second problem, and proposes a new algorithm for exploring state spaces of finite capacity Petri nets with large capacities. In the proposed algorithm, the state space is represented in the form of a tree such that a set of markings generated by periodic occurrences of firing sequences is associated with each node, and it is much smaller than the reachability graph.

This paper presents an efficient method to derive the first passage time of an extended stochastic Petri net by simple algebraic operations. The reachability graph is derived from an extended stochastic Petri net, and then converted to a timed stochastic state machine which is a semi-Markov process. The mean and the variance of the first passage time are derived by algebraic manipulations with the mean and the variance of the transition time, and the transition probability for each transition in the state machine model. For the derivation, three reduction rules are introduced on the transition trajectories in a well-formed regular expression. An efficient algorithm is provided to automate the suggested method.

This paper considers two simulation models for simple unreliable file systems with checkpointing and rollback recovery. In Model 1, the checkpoint is generated at a pre-specified time and the information on the main memory since the last checkpoint is back-uped in a secondary medium. On the other hand, in Model 2, the checkpointing is executed at the time when the number of transactions completed for processing is achieved at a pre-determined level. However, it is difficult to treat such models analytically without employing any approximation method, if queueing effects related with arrival and processing of transactions can not be ignored. We apply the generalized stochastic Petri net (GSPN) to represent the stochastic behaviour of systems under two checkpointing schemes. Throughout GSPN simulation, we evaluate quantitatively the maintainability of checkpoint models under consideration and examine the dependence of model parameters in the optimal checkpoint policies and their associated system availabilities.