This tutorial paper provides a comprehensive overview of structural analysis techniques for Petri Nets (PNs). We recall the fundamental concepts, definitions, and notations, and highlight the role of structural properties in the analysis and verification of complex Discrete-Event Systems (DESs). Beyond classical tools such as invariants, semiflows, traps, and siphons, special attention is devoted to the notions of home spaces and basis reachability graphs, which offer compact and effective alternatives to exhaustive state-space exploration. Real-world examples, including applications in telecommunications, illustrate the practical relevance and applicability of these methods. The paper aims to serve both as a reference for researchers and as an accessible entry point for graduate students interested in Petri net theory and applications.
A simple but general semantics for timed Petri nets is presented in this paper. Based on this semantics, an optimization formulation is introduced and implemented in a recently developed optimization solver, where a satisfiability (SAT) solver is integrated with constraint programming (CP). The solver, called CP-SAT, is a part of Google’s OR-Tools. The optimization formulation includes both concurrent and alternative sequences of operations, involving shared as well as alternative resources. The proposed optimization strategy is compared with the SAT/SMT-based solver Z3Opt and Gurobi’s mixed integer linear programming (MILP) solver. The conclusion is that the computation time for CP-SAT is much shorter than for Z3Opt, while MILP is able to handle deep problems, including long sequences with many transitions, with similar computational performance as CP-SAT. On the other hand, CP-SAT is much faster than MILP for wide problems, including many parallel sequences. An evaluation of an industrial-sized flexible manufacturing system, which involves uncontrollable events, also demonstrates how efficient and easy to implement the proposed strategy is compared to existing results. In addition, it is also demonstrated how basic functionality in SAT and constraint programming are related and integrated in CP-SAT. The conclusion is that the strength of CP-SAT depends on its successful integration of search, inference, and OR-based relaxation on top of a satisfiability solver.
In this paper we propose an approach for a class of dynamic task assignment problems (DTAPs) using Petri nets. A DTAP consists of two parties of agents: the customers who expect to be serviced, and the servers who provide service to customers in multiple rounds of engagements. The aim of solving the DTAP is to synthesize an assignment strategy that maximizes the service rate. The DTAP studied in this paper follows a player-against-nature decision structure, where the decision maker selects assignment actions and the environment reveals stochastic success/failure outcomes. To this end, we propose a novel Petri-net-based approach to model and solve such DTAPs with the fail-and-retry mechanism. In our approach, the behavior of customers and servers are first modeled by path and server subnets, respectively. A novel Petri net model called the Game Petri net (GPN) is then constructed, in which the dynamic multi-stage task assignment is captured. The game Petri net is constructed in a bottom-up manner using a modular synthetic procedure, and its reachability space represents the player-against-nature decision process between the decision maker and the stochastic environment. By constructing the game reachability graph of a GPN as a game tree, the optimal target assignment strategy for the discretization is determined through backward induction. Simulations show that our proposed method achieves better performance in terms of service rate compared with conventional policies.
This paper addresses modeling, controllability, and control analysis in three extensions of Petri nets (PNs) that integrate continuous and discrete dynamics: Timed Continuous Petri Nets (TCPNs), First-Order Hybrid Petri Nets (FOHPNs), and Generalized Batches Petri Nets (GBPNs). These formalisms extend the PN paradigm to capture hybrid behaviors in complex dynamical systems while preserving their structural and analytical foundations. Regarding TCPNs, results on controllability from a structural perspective are recalled, and the design of controllers based on a Model Predictive Control (MPC) approach is presented. The FOHPN model is described in detail, and a series of applications to real systems is discussed. Two different control approaches are considered: a myopic approach, which computes the instantaneous firing speeds of transitions as the solution of an optimization problem that varies at each macro-period, and an MPC-based approach, which overcomes some of the limitations of the myopic approach. For GBPNs, a semantics inspired by FOHPNs is revisited, combining discrete, continuous, and batch dynamics. This formalism enables control over firing flows and batch transfer speeds, leading to controllable GBPNs. Within this framework, and in the absence of discrete nodes or over a macro-period, three event-driven ON/OFF control strategies are examined. Together, these results highlight the potential of Continuous and Hybrid PN extensions to provide a unified foundation for the analysis and control of hybrid dynamical systems, bridging discrete-event and continuous-flow representations.
This paper presents Timed Output Synchronized Petri Nets (TdOSPNs), an extension of Output Synchronized Petri Nets (OutSynPNs) that incorporates a temporal dimension to the net by associating a duration with each transition, while maintaining synchronized behaviors with input events. To address the challenge of infinite state spaces in TdOSPNs, we propose the Synchronized State Class Graph (SynSCG), inspired by the State Class Graph introduced by Berthomieu and Menasche (1982), as a method for state space representation and analysis. Although constructing the SynSCG involves significant computational complexity due to the Fourier-Motzkin elimination method, it allows for marking reachability verification for bounded nets. Our findings show that for bounded nets, the graph is finite and deterministic. It also faithfully represents the timed behavior of TdOSPNs, adhering to all the timing and semantic constraints of the formalism, thus enabling the monitoring of input/output sequences and their time intervals.
