Generalized stochastic Petri nets (GSPN), with immediate transitions, are extensively used to model concurrent systems in a wide range of application domains, particularly including software and hardware aspects of computer systems, and their interactions. These models are typically used for system specification, logical and performance analysis, or automatic code generation. In order to keep modeling separate from the analysis and to gain in efficiency and robustness of the modeling process, the complete specification of the stochastic process underlying a model should be guaranteed at the net level, without requiring the generation and exploration of the state space. In this paper, we propose a net-level method that guides the modeler in the task of defining the priorities (and weights) of immediate transitions in a GSPN model, to deal with confusion and conflict problems. The application of this method ensures well-definition without reducing modeling flexibility or expressiveness.

Scheduling problems are very important in order to optimise the behaviour of discrete events dynamic systems. Nevertheless, the computation of scheduling policies turns out to be NP-hard in most interesting cases in practice. The purpose of the paper is to apply transformation/reduction rules to the solution of the scheduling problem. These kind of rules have already been applied to the analysis of autonomous Petri nets or to program coding optimisation by means of time Petri nets. Here, reduction is intended to preserve the existence of at least one optimal solution for the scheduling problem. In many practical cases, transformation/reduction allows us to alleviate the computational problem of synthesising an optimal schedule. We show its usefulness by means of an illustrative example.

Deterministically synchronized sequential processes (DSSP) are a subclass of Petri nets, well suited for the methodical construction of models of concurrent systems where several agents cooperate through asynchronous message passing, In this paper, DSSP are presented, illustrating their usability in manufacturing systems. They are compared to other more restrictive subclasses of Petri nets used for similar purposes. In spite of being more expressive, DSSP still enjoy many strong analytical results, some of which are derived and illustrated in the paper.

Among discrete event systems, those exhibiting concurrency are especially challenging, requiring the use of formal methods to deal with them. Petri nets are a well-established such formalism. The structure theory aims at overcoming the state space explosion problem, inherent to the analysis of concurrent systems, by bridging structural and behavioral properties. To date, this has been successfully achieved mainly for some subclasses of ordinary nets. However weights are a modeling convenience in many situations. In this paper we study a formal model for a subclass of concurrent systems with bulk services and arrivals which structurally avoids conflicts. Structural results and techniques for dealing with them are introduced. These include structural conditions on properties of correct behavior and a unified framework for checking general behavioral properties by reasoning solely on the structure.