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.
Cyber-physical systems (CPSs) are formed of physical and computational components that interact to operate a process safely and efficiently according to the desired behavior. To do so, the plant is continuously monitored, and the information obtained from its components is transmitted to computer-based devices. The connection between the plant and the monitoring and control device is carried out using communication networks, which may be susceptible to cyber-attacks. In this paper, we consider that the communication channel used to transmit data from the plant to the monitoring and control device is vulnerable to attacks, and that the attacker eavesdrops on the communication channel to gather sensitive information and discover if the system has reached a secret state. Since we assume that the information transmitted in the network is the status of system components, such as sensors, actuators, and memory variables of local controllers, the system can be modeled, from the attacker’s perspective, as a finite state transducer, where each state of the model is associated with an output vector formed of the signals associated with the system components. Considering that the attacker has full knowledge of the system model and does not know the current state of the system when he/she initiates to eavesdrop on the communication channel, the attacker tries to estimate the current state of the system by observing the state outputs transmitted in the network. Therefore, in this case, it is necessary to verify whether the attacker is never able to detect the secret states of the system. In the Discrete-Event System literature, the system property associated with the intruder’s inability to discover the system secret based on the transmitted information is called opacity. Since, in this paper, the attacker observes state outputs of a finite state transducer instead of events, we introduce a new notion of opacity called Current-State Opacity based on State Outputs (CSO-SO). We also present a method for the verification of CSO-SO. In addition, a comparison between the definition of current-state opacity based on event observations and CSO-SO is provided. A practical system is used to illustrate the definition and verification of CSO-SO.
Following the publication of this work (Zippo et al. 2023a), we identified a few deficiencies in the original proofs. In the case of pseudoinverses, the proofs were found to be incomplete; however, the corresponding results remain valid. In contrast, the analysis concerning composition contained an error arising from an overlooked edge case, which affected both the theoretical results and the associated algorithm. In this erratum, we present corrected and complete proofs, as well as amendments to the affected results.
Bisimulation is a powerful abstraction method, which can be used to perform model reduction, especially for modular transition systems. A unified formulation of strong, weak, stutter, and branching bisimulation is presented. For branching bisimulation an extended relation is shown to coincide with the original branching bisimulation when the largest relations (equivalence relations) are considered. A block transition based description that is more natural from a model reduction perspective is also shown to be equivalent to the original relation based bisimulations. All bisimulation formulations are based on general transition system models, which means that systems both including state and transition labels are handled in a unified way. An incremental abstraction based on divergence sensitive branching bisimulation is then formulated and applied to Petri nets. The strength of the proposed method is demonstrated especially for Petri nets, combining both analytical and computational abstraction.
Constrained multi-objective optimization problems frequently arise in domains, such as industrial production, supply chain management, and finance. However, despite their widespread relevance, these problems have received limited attention in the simulation optimization literature. This paper considers a multi-objective ranking and selection problem with stochastic constraints, where each alternative has multiple performance measures and is subject to different constraints. Given a fixed simulation budget, the objective is to develop an efficient simulation budget allocation strategy to accurately identify the set of Pareto-optimal and feasible alternatives from a finite set of candidates. To this end, an optimal computing budget allocation (OCBA) problem is formulated to maximize the probability of correctly selecting the Pareto feasible set. Then, a lower bound on the probability of correct selection for the Pareto feasible set is derived, and used to construct an OCBA rule along with a sequential allocation procedure. Numerical experiments and a portfolio selection case study demonstrate the effectiveness of the proposed OCBA rule in significantly improving simulation sampling efficiency.
This work integrates Markov Decision Process (MDP) framework with Supervisory Control Theory (SCT) to address production planning challenges, especially minimizing makespan. By leveraging MDP’s sequential decision-making framework and SCT’s constraint based framework, the approach ensures online decision-making in dynamic industrial environments. The feasibility of this integration is demonstrated through the formalization of a mapping between the two approaches. The results demonstrate that the proposed approach efficiently solves the tested problems, achieving makespan values close to the reference solution but with significantly lower processing times in most cases.
This work presents a comprehensive investigation into the robust supervisory control of metric discrete event systems, which are modeled as finite state automata and incorporate metric functions to measure state distances. While existing studies on supervisory control primarily focus on qualitative analysis and provide a binary answer regarding whether the controlled system satisfies the given specifications, our work introduces Metric Discrete Event Systems to quantitatively investigate robust supervisory control. Specifications are defined using a fragment of Linear Temporal Logic (LTL), specifically syntactically co-safe LTL (scLTL). Environmental disturbances can cause deviations from the system’s nominal behaviors, thereby hindering the successful accomplishment of the original tasks. To mitigate this issue, we design supervisors to ensure that the controlled system degrades gracefully under adverse conditions. We formally define the robustness of supervisors in a topological context and formulate two key problems: verification of the existence of robust supervisors and synthesis of optimal robust supervisors. We propose a two-player game framework to address both problems. First, we introduce a bipartite structure called distance bipartite transition system (DBTS) as the arena of the game between the supervisor and the environment. The verification problem is then reformulated and solved as a reachability game on a special DBTS, where the set of target states is properly defined. For the synthesis problem, we define a sequence of vectors to track the shortest distance to the accepting states under disturbances and compute their fixed-point using dynamic programming techniques. Then we synthesize the optimal winning strategy of the supervisor, which eventually yields the optimal robust supervisor. Finally, we provide a case study of robot task planning to validate the performance of our proposed methods that demonstrates persuasive results in real-world scenarios.
A large number of ship locks in the Netherlands require renovation as they reach their end of life-cycle or do not adhere to the changing environment. These renovations imply the redesign of their control software. This paper explores the use of synthesis-based engineering (SBE) to achieve correct-by-construction supervisory controllers for these systems. To address the complexity and scale of this task, a configurator for SBE models is proposed, enabling the automated generation of controllers and model simulation based on mechanical parameters. The accompanying tool improves efficiency, quality, and reduces human error and is already in use for ship lock supervisors in Lelystad and Maasbracht. Although developed for ship locks, the structure of the tool is adaptable to support other families of systems.
The study of discrete event dynamic systems with inexact (interval) data plays an important role in optimization problems such as scheduling or project management in which the objective function depends on the interval data and the maximum and plus operations. This approach is based on the formalism and characteristics of max-plus balanced matrices, balanced determinants, and Hankel matrices as their properties are key in modeling discrete event dynamic systems. This article deals with the generalization of balanced max-plus matrices and two basic versions of balanced matrices with interval entries, i.e. universally and possibly balanced matrices, and two other versions derived from them, namely EA-balanced and AE-balanced circulant-Hankel interval matrices. For each concept of circulant-Hankel interval matrices, we present polynomially checking equivalent conditions.
Time-dependent Petri nets extend the classical Petri net formalism by incorporating timing constraints, enabling the modeling and analysis of temporal behavior in discrete event systems. This survey provides a comprehensive overview of the foundational concepts and major classes of time-dependent Petri nets, including both deterministic and stochastic variants. We explore their modeling capabilities, formal analysis techniques, and a range of performance evaluation methods. In particular, we aim to analyze the performance indices such as cycle time, throughput, and resource utilization, which are critical for assessing system efficiency and scalability. Examples are provided to demonstrate how system performance is evaluated. Additionally, we discuss current challenges and emerging trends in the field, highlighting open research problems and potential future directions.
Sea-rail intermodal transportation is an essential infrastructure in global supply chains nowadays. However, the efficiency of this system is often hindered by bottlenecks in the storage and retrieval of containers in the yard. Recent studies on container-to-stack assignment treat all stacks as a whole, resulting in a large solution space that makes these approaches unsuitable for large-scale problems. Additionally, widely adopted heuristic methods often lead to suboptimal solutions. The challenge of achieving real-time, optimal yard storage allocation in large yards remains unresolved. In this work, we address this critical issue and make the following contributions. By exploiting the independence among stacks, we formulate the yard storage allocation problem as a restless multi-armed bandit (RMAB) problem and leverage the Whittle index policy to address it. We empirically establish the indexability of this RMAB problem for the general case and provide theoretical verification for a specific scenario. Recognizing the challenges of analytically deriving the Whittle index for this practical application, we propose a novel algorithm, SWIRL, which leverages reinforcement learning to estimate the Whittle index both accurately and efficiently. Unlike existing methods for Whittle index estimation, SWIRL is capable of handling complex RMAB problems with large arm state spaces. Numerical experiments demonstrate the effectiveness and scalability of the proposed method. Furthermore, the model trained by SWIRL can be directly applied to different scenarios without requiring retraining, even when the container distribution or the number of stacks changes, showing the potential of the proposed method to be applied in practice.
In this paper, we develop a unified theory of IPA estimators for steady-state performance characteristics. Our goal is to clarify how infinitesimal perturbation analysis can be systematically connected to a measure-valued differentiation framework for the underlying Markov chain dynamics. Traditionally, the asymptotic behavior of gradient estimators has been studied by analyzing the estimators themselves. Here, we take a different perspective. We show that by clearly separating the level at which arguments are made, either at the sample-path level, where IPA is usually formulated, or at the operator/measure level, where Markov chain differentiation is naturally expressed, one can combine the strengths of both approaches. Our framework helps bridge two established streams of research and contributes a more general understanding of IPA for steady-state problems.
We propose new intermediate semantics for T-time Petri nets (T-TPN), which fill the gap between strong and weak semantics. By encoding a 2-counter machine, we prove that reachability is not decidable for these semantics in the case of unbounded nets. As regards with bounded nets, we construct a state space abstraction using zones and we study its termination. We then consider safe nets and we propose a translation into interval weighted automata (IWA) over an interval like semiring, product of (max,+) semiring with itself, that preserves the timed behaviour of T-TPN.
The concept of k -level opacity is used to determine the level of opacity in a system. If the tolerance level k is higher, then the degree of opacity for any secret information will also be higher. However, if more non-secret information are not distinguished from secret ones, then the cost of achieving a control strategy will also be higher. In this paper, an optimization model that minimizes the discount total choosing cost while maintaining k -level opacity and releasing all the secret string is presented. If the secret language is k -level opaque w.r.t. its closure, the closure or the infimal controllable super-language of the closure is the optimal solution. If the secret language is not k -level opaque w.r.t. its closure, then a Multi-Stage Optimization Problem with Multi-Selection at each Stage (MSOP-MSS) is proposed. By analyzing the MSOP-MSS, an algorithm for handling the situation was proposed and used to obtain control strategy for the optimization model. The control strategy has been proven to be optimal. Finally, a complete algorithm, computational complexity analysis, and application examples are described.
We study the Traffic Light Control (TLC) problem for a single intersection, considering both straigh driving vehicle flows and corresponding crossing pedestrian flows with the goal of achieving a fair jointly optimal sharing policy in terms of average waiting times. Using a stochastic hybrid system model, we design a quasi-dynamic policy controlling the traffic light cycles with several threshold parameters applied to the light cycles and the partially observed contents of vehicle and pedestrian queues. Infinitesimal Perturbation Analysis (IPA) is then used to derive a data-driven gradient estimator of a cost metric with respect to the policy parameters and to iteratively adjust these parameters through an online gradient-based algorithm in order to improve overall performance on this intersection and adapt the policy to changing traffic conditions. The controller is applied to a simulated intersection in the town of Veberöd, Sweden, to illustrate the performance of this approach using real traffic data from this intersection.
The high penetration of renewable power generation introduces new challenges to the economic and stable operation of power systems. The security-constrained unit commitment (SCUC) problem is an important mixed-integer programming (MIP) problem solved within a limited time by independent system operators every day. To address the uncertainty associated with renewable power, there is a growing need for fast solutions to stochastic multi-objective SCUC (MO-SCUC), which considers both operational cost and spinning reserve capacity. In this paper, we propose a fast solution method based on vector ordinal optimization (VOO) to effectively obtain good enough solutions for MO-SCUC. We first propose a method for efficiently generating high-quality initial solutions for integer variables, which includes a machine learning-based probability-guided sampling method and analytical feasibility conditions derived from the problem structure. Then, VOO is applied to rapidly select good enough solutions. Our method can quickly determine the values of integer variables in MO-SCUC, transforming the computational burden from large-scale MIP problems into a few small-scale linear programming problems that can be solved in parallel. Furthermore, to enhance the performance of VOO, we propose a hybrid approach that integrates VOO with existing multi-objective evolutionary methods to efficiently obtain approximately Pareto optimal solutions. Experimental results on the IEEE 30-bus and 118-bus systems show that the proposed VOO-M method achieves speedups of 35 ∼ 210 times compared to traditional methods using the commercial solver Gurobi, with solution quality degradation of less than 15 ∼ 31 times while outperforming the Weighted-sum method in solution quality by 0.53 ∼ 3.05
In this paper we study an N-player constrained absorbing continuous-time Markov game with a countable state space and compact action spaces. The reward / cost rates as well as the transition rates are allowed to be unbounded. Players in the game are to maximize their total expected rewards by adopting strategies which keep their total expected costs below some given constants. Such a game model with these features seemingly has not been handled in the previous literature. To solve the game, we first introduce correlated strategies to induce occupation measures. Then under usual continuity-compactness conditions, we obtain the topological properties of the occupation measures, establishing the existence of a constrained stationary Nash equilibrium in the family of all history-dependent strategies of the players when applying Kakutani-Fan-Glicksberg fixed point theorem.
