Search

Opacity is a security notion that focuses on determining whether a given system's behavior is kept secret to intruders. Various notions of opacity have received significant attention during the last decade including current state opacity and initial state opacity, which have been studied for deterministic and probabilistic systems in untimed contexts. In timed systems, opacity requirements may vary with time and one could also be interested in knowing the time duration for which opacity requirements are violated or preserved. The main contribution of this work is to introduce and analyze opacity exposure and opacity revelation times as measures of vulnerability in timed DES that behave according to Markovian dynamics (i.e., at any given time, all enabled events are independent and distributed in time with exponential probability density functions). Labeled Stochastic Petri Nets (LSPN) are used to model timed stochastic discrete event systems (DES), and appropriate constructions (involving current and initial state observers) are used to evaluate exposure and revelation times for a given LSPN.

Cyber–physical system (CPS) is a complex system that contains multiple components working cooperatively. According to its characteristics, we propose an object-oriented generalized stochastic Petri net (OGSPN), in which the CPS is abstracted into several types of objects and its logical structure and working process is visually described. Moreover, we model and measure the time consumed by each activity in CPS for quantitative analysis. To simplify the process of performance analysis on this model, in this article we propose a compression algorithm to convert OGSPN into a generalized stochastic Petri net (GSPN). Considering the uncertainty in CPS, we use a fuzzy mathematics based method to process the compressed model of GSPN for improving the accuracy of the performance analysis. We apply our method to a real-world thick metal plate production line in a manufacturing company, and the availability of our method is verified by extensive experiments.

In this article we develop an intrusion detection attack–defense game for Internet of Things (IoT) systems for which autonomous IoT devices collaboratively solve a problem. We develop an analytical model to determine the conditions under which malicious nodes have no incentives to perform attack in the intrusion detection attack–defense game. We also develop a stochastic Petri net model to analyze the effect of attack–defense behaviors on system reliability, given a definition of system failure conditions as input. The performance evaluation results demonstrate that our intrusion detection system (IDS) attack-defense game design greatly improves system reliability over existing autonomous IoT systems without gaming design consideration when attacks are reckless and intensive.

In order to reduce the failure rate of Integrated Modular Avionics (IMA) partition software, due to the reliability block diagram (RBD) method, fault tree analysis (FTA) method and GO method cannot describe the state transition process of partition software, according to the ARINC 653 standard and the actual running status of the partition software, this paper determines the state machine and conversion delay of the partition software, and establishes the stochastic Petri nets (SPN) reliability quantitative model of the partition software. By proving that each transition in the SPN model of the partition software approximately obeying exponential distribution, and according to the reachable state tree of the SPN isomorphic to a homogeneous Markov chain (MC), the steady-state probability of the partition software in the fault state is calculated to be $5.2778^\ast 10^{-9}$ by using MC stochastic process theory. The factors affecting the reliability of the partition software are obtained, and the sensitivity of each factor to the model is studied. Finally, the relevant conclusions are drawn to provide guidance for improving the reliability of partition software.

In order to improve the optical and electrical consistency in lighting and display, light emitting diode (LED) dies should be sorted and aligned precisely one by one. As per given current production process practices, the sorting efficiency is required to be more than 36 thousand units per hour (KUPH), while the alignment deviation should not exceed 1 mil (25.4 $\mu \text{m}$ ) and all dies’ angle deviations should fall within 5°. Among all the requirements, the chip angle correction is particularly difficult to achieve because a small die correction on wafer would cause a change in all dies’ positions, leading to significant performance degradation. This results in an ambiguity, due to the difficulty in balancing efficiency and accuracy. In this article, the influence factors of the accuracy deviation caused by the angle correction are analyzed in detail, and the negative effect caused by tiny deformation of the elastic substrate is studied with comprehensive experiments. The parallel scheduling mechanism of the angle correction is analyzed, and the influences on sorting performance are evaluated with stochastic petri net (SPN) model, so that the suitable working area is disclosed. A local compensation strategy using the local deformation trend of the membrane is utilized to optimize the accuracy of precorrection. Further, the alignment area is actively compensated according to the alignment precision requirements, so that the performance and accuracy requirements are balanced. In the chip packaging field, microchip angle correction is often needed. This method is applicable to similar situation and chips are adhesive on membrane.

Availability of a common, shared benchmark to provide repeatable, quantifiable, and comparable results is an added value for any scientific community. International consortia provide benchmarks in a wide range of domains, being normally used by industry, vendors, and researchers for evaluating their software products. In this regard, a benchmark of untimed Petri net models was developed to be used in a yearly software competition driven by the Petri net community. However, to the best of our knowledge there is not a similar benchmark to evaluate solution techniques for Petri nets with timing extensions. In this paper, we propose an evaluation framework for the comparative analysis of generalized stochastic Petri nets (GSPNs) simulation techniques. Although we focus on simulation techniques, our framework provides a baseline for a comparative analysis of different GSPN solvers (e.g., simulators, numerical solvers, or other techniques). The evaluation framework encompasses a set of 50 GSPN models including test cases and case studies from the literature, and a set of evaluation guidelines for the comparative analysis. In order to show the applicability of the proposed framework, we carry out a comparative analysis of steady-state simulators implemented in three academic software tools, namely, GreatSPN , PeabraiN , and TimeNET . The results allow us to validate the trustfulness of these academic software tools, as well as to point out potential problems and algorithmic optimization opportunities.

Cyberspace mimic domain name system (CMDNS) adopts dynamic heterogeneous redundant architecture with strategic decision mechanism to control the effectiveness of uncertain disturbance. There is lack of methods to evaluate the availability and awareness security of CMDNS. To further describe and analyze the characteristics of CMDNS accurately, the Generalized stochastic Petri net (GSPN) is used to model the attack disturbance and defense of mimic Domain name system (DNS), and the availability and awareness security of Dissimilar redundancy system (DRS) and mimic DNS under different disturbance intensities are compared. We compared the different effect of local service query and real network query on the average response delay. The results show that the introduction of mimic architecture will inevitably pay the corresponding delay cost which increase 9.3% compared with traditional local DNS, but it has little effect on the service which only increases by 1.9% compared with the DNS transmission delay at the network communication level.

Efficient business process is important to the operations of supply chain finance (SCF). Many deficiencies exist in the processes of SCF such as complicated workflows and high time-consuming steps. However, few studies have paid attention to evaluate and improve the performance of SCF processes. We empirically model and investigate the processes of supply chain finance by constructing a Stochastic Petri Net based on the field survey of a focal firm. Two critical indices, place busy rate and transition utilization rate, are evaluated. The results demonstrate that some places (transitions) of the Petri Net have high busy rates (utilization rates). By integrating the Petri Net and dependency graph, several key places and transitions in the Petri Net of SCF processes are identified for further optimization. To improve the performance of SCF processes, we propose three optional adjusting schemes on the basis of information sharing perspective (for the first half of the Petri Net) and risk sharing perspective (for the second half of the Petri Net). The proposed optimization strategies have further been proven to reduce the place busy rates, shorten the process, and improve the process efficiency of the supply chain finance.

Communication-based train control (CBTC) systems are widely applied in the world. The primary functions are carried out by wireless communications, which implement the communication between train and ground. However, this kind of solution involves too many subsystems and interfaces, which makes the group equipment complex and expensive to maintain. What is more, once the ground control center or the communication channel is out of service, the train must operate in degraded modes, and more human factors will be involved. As a result, the efficiency and safety of the train operation will be affected. In order to significantly increase efficiency and safety, train-to-train (T2T) communication is proposed as a new solution for railway signaling. Hence, the availability and performance analysis of the direct T2T data communication system is essential. In this paper, the system structure is described, and different parameters that can affect the performance of the communication system are discussed. In order to evaluate the system availability and performance, the stochastic Petri nets (SPNs) are applied to formalize the communication system. The numerical analysis is carried out with different parameters, which consider both bit error and transmission rates. The results show that the method applied in this paper can be used to evaluate the performance and availability of the T2T data communication system.

This technical note concerns the fault diagnosis of stochastic discrete event systems. Specifically, the goal is to characterize a detected fault by estimating its occurrence date. For that purpose, partially observed stochastic Petri nets are used to model the system, the failure processes, and the sensors. From the proposed modeling and collected dated measurements, the probabilities of consistent trajectories are computed and diagnosis in terms of faults probability is established as a consequence. For each detected fault, the probability density function of its occurrence date is approximated. This estimation improves the diagnosis by providing the most probable time interval of the fault occurrence. The interest of fault datation and the applicability of the proposed approach are showed through a case study that represents a distribution system.

Deadlock detection plays an important role in the analysis of system behavior. Several kinds of reachability trees have been proposed to analyze Petri net properties including deadlock freedom. However, existing reachability trees can only solve the deadlock detection problem of bounded or some special kinds of unbounded Petri nets. To increase the applicable scope of reachability trees in the deadlock detection field, this paper presents a new type of reachability trees called complex reachability tree (CRT). Different from others, transition sequences corresponding to root-started paths of cyclic CRTs are always firable from the initial marking. The proposed trees can completely solve the deadlock detection problem of ${\omega }$ -gone node-free Petri nets, but cannot guarantee to detect all the deadlocks for the other kinds of unbounded Petri nets. Their construction method and applications are presented.

Communication-based train control (CBTC) systems are automated train control systems using wireless communications. The normal operation of CBTC systems depends on a reliable data communication system. The existing CBTC data communication system are based on train-to-ground communication, which suffers from too many subsystem interfaces and makes ground equipment extremely complicated. In next-generation CBTC systems, train-to-train communication is adopted with the advantages of higher efficiency and briefer system structure. Although train-to-train communication based CBTC systems has been implemented in urban rail systems. The data communication system reliability has not been studied before. In this paper, the next generation CBTC data communication system reliability is modeled with Deterministic and stochastic Petri nets (DSPNs). We design a next generation CBTC data communication system using LTE technologies, and set up laboratory test environment to test system performance. The performance data is converted as DSPN model parameters to evaluate system reliability. With the tested system performance measures, we evaluate the reliability of data communication scenarios, which includes the reconnection and handoff scenarios. Extensive simulation results are then given to illustrate the system reliability, which considers both the train to train communication link and train to ground communication link.

A cyber physical distribution power system (CPDS) is a large and complex infrastructure that coordinates the cyber communication system and the physical distribution power system. Because of the increasingly advanced information communication technology, the development of cyber physical distribution power system has caused key cyber security issues related to system operation. This paper is focused on realizing a unified system attack modeling and security assessment of an active distribution power system. In this paper, first we present an overview of the system operation from the fusion system perspective. The significant effects of network intrusion attacks on operational security are evaluated. A new unified cyber physical network model is established using a limited stochastic Petri net graph theory that considers refined firewalls and password components. Then, a security effectiveness evaluation method is proposed to analyze channel throughput variation and system robustness. Overall CPDS security risk values are determined based on physical influence coefficients. Finally, simulations of an improved IEEE-33 bus distribution power system and security assessment under intrusion attacks are described. The research work could raise awareness of the cyber intrusion threats and provide the basis for security defense.

This paper proposes a novel decentralized on-line fault diagnosis approach based on the solution of some integer linear programming problems for discrete event systems in a Petri net framework. The decentralized architecture consists of a set of local sites communicating with a coordinator that decides whether the system behavior is normal or subject to some possible faults. To this aim, some results allow defining the rules applied by the coordinator and the local sites to provide the global diagnosis results. Moreover, two protocols for the detection and diagnosis of faults are proposed: they differ for the information exchanged between local sites and coordinator and the diagnostic capability. In addition, a sufficient and necessary condition under which the second presented protocol can successfully diagnose a fault in the decentralized architecture is proved. Finally, some examples are presented to show the efficiency of the proposed approach.

This paper is about control design for discrete event systems modeled with Petri nets. It addresses the problems of reachability and of firing sequence design. The untimed and timed cases are successively studied by searching control sequences from an initial marking to a reference one with length or duration that approach the minimal value, avoiding forbidden states and nonpromising branches. The proposed algorithms are applicable to a large class of discrete event systems in particular in the domain of flexible manufacturing, engineering. To accelerate the computation and make robust the control strategy, only a small area of the reachability graph is worked out and an approach inspired from model predictive control is used. The approach is suitable for deadlock-free scheduling and fault-tolerant control problems.

Control of a large-scale automated manufacturing system is an important and challenging issue. Its discrete event system model represented by Petri nets tends to become highly complicated in structure, especially when there exist uncontrollable or unobservable events. The existing approaches are nontrivial to design both efficient and maximally permissive supervisors to impose constraints on an overall system. In this paper, instead of considering the control problem from an overall system perspective, we intend to transform an overall control problem into the one designing multiple controllers in parallel, each of which is much simpler in structure. A Petri net structure is decomposed via integer linear programming or a polynomial decomposition method to obtain multiple state-machine subnets that constitute a decentralized system. A necessary and sufficient condition for preserving the equivalence in terms of states and behaviors between the overall system and its decentralized version is reported. Constraints representing control requirements are further converted and enforced in the respective subnets. Then, supervisors are generated via a generalized mutual exclusion constraint method. By considering the deviations between the subnet control and overall control, this paper formulates a communication mechanism to guarantee that the decentralized system runs in an appropriate manner. Finally, two examples are presented to demonstrate the proposed approach.

The main contribution of this correspondence paper consists in a linear algebraic characterization of the admissible marking set relative to a Petri net with uncontrollable transitions, subject to a linear constraint. In more detail, given a linear constraint that limits the number of tokens in one place, an algorithm is proposed to compute an approximation of the admissible marking set in terms of a disjunction of transformed linear constraints. The optimality of the solution is guaranteed provided that certain conditions are satisfied during the intermediate steps of the iterative approach. In all the other cases, the set of markings described by the transformed constraints could be surely contained in the admissible marking set.

This paper presents an ordinary Petri net (PN)-based approach to the modeling and race-detection problems of programs for programmable logic controllers (PLCs). First, a PLC program is formalized by a graph where nodes represent contacts and coils. Second, an algorithm is proposed to translate this graph into an ordinary PN. Third, a method is presented to detect whether there exists a race in a program by using a reachability graph technique, to locate a race by introducing the race path, and to correct a race by analyzing the subnet that contains it. An example is utilized to illustrate the theoretic results.

Elaborate efforts have been made to eliminate fake markings and refine ${\omega }$ -markings in the existing modified or improved Karp–Miller trees for various classes of unbounded Petri nets since the late 1980s. The main issues fundamentally are incurred due to the generation manners of the trees that prematurely introduce some potentially unbounded markings with ${\omega }$ symbols and keep their growth into new ones. Aiming at addressing them, this work presents a non-Karp–Miller tree called a lean reachability tree (LRT). First, a sufficient and necessary condition of the unbounded places and some reachability properties are established to reveal the features of unbounded nets. Then, we present an LRT generation algorithm with a sufficiently enabling condition (SEC). When generating a tree, SEC requires that the components of a covering node are not replaced by ${\omega }$ symbols, but continue to grow until any transition on an output path of an unbounded place has been branch-enabled at least once. In return, no fake marking is produced and no legal marking is lost during the tree generation. We prove that LRT can faithfully express by folding, instead of equivalently representing, the reachability set of an unbounded net. Also, some properties of LRT are examined and a sufficient condition of deadlock existence based on it is given. The case studies show that LRT outperforms the latest modified Karp–Miller trees in terms of size, expressiveness, and applicability. It can be applied to the analysis of the emerging discrete event systems with infinite states.

The scenario that two trains occupy the same block sometimes happens in actual operations. For example, cases like train formation, fast shunting, relief wrecking, and so on. In the fixed-block based railways, the close proximity driving in the same one block section is monitored by train drivers. Similarly, in the moving-block based railways when Automatic Train Protection (ATP) out of service, the drivers have to take more responsibility and workload to ensure the train operation safety. In these specific scenarios accidents caused by human errors have more possibility to happen. To increase the safety demanding needs of railway transport in a close distance, this paper proposes a close proximity driving train movement authority system (MAp). This system permits implementing train to train distance measurement and movement authority generation for trains that located at a close distance. Apart from a wireless communication unit, the system does not require any other infrastructure. With the assistance of train-centric communication technology, the MA+ can detect the train to train distance interval within a certain scope. The principle and structure of the system are proposed. Stochastic Petri nets are applied to evaluate the system availability.

Delay tolerant networks (DTNs) are often encountered in military network environments where end-to-end connectivity is not guaranteed due to frequent disconnection or delay. This work proposes a provenance-based trust framework, namely PROVEST (PROVEnance-baSed Trust model) that aims to achieve accurate peer-to-peer trust assessment and maximize the delivery of correct messages received by destination nodes while minimizing message delay and communication cost under resource-constrained network environments. Provenance refers to the history of ownership of a valued object or information. We leverage the interdependency between trustworthiness of information source and information itself in PROVEST. PROVEST takes a data-driven approach to reduce resource consumption in the presence of selfish or malicious nodes while estimating a node's trust dynamically in response to changes in the environmental and node conditions. This work adopts a model-based method to evaluate the performance of PROVEST (i.e., trust accuracy and routing performance) using Stochastic Petri Nets. We conduct a comparative performance analysis of PROVEST against existing trust-based and non-trust-based DTN routing protocols to analyze the benefits of PROVEST. We validate PROVEST using a real dataset of DTN mobility traces.

In this paper, we investigate the decidability and complexity of the fault diagnosis problem in unbounded labeled Petri nets. First, we show that checking diagnosability for unbounded Petri nets is decidable. We present a new necessary and sufficient condition for diagnosability, which can be reduced to a model checking problem for unbounded Petri nets. Then, we show that checking diagnosability for unbounded Petri nets is EXPSPACE-complete. This complexity result is further extended to various subclasses of Petri nets. To the best of our knowledge, this is the first paper that establishes decidability and complexity results for diagnosability of unbounded Petri nets.

Human–machine collaborative manufacturing systems consist of human operators and automated machines. They cooperate with each other to accomplish complex tasks that are difficult for either the human or machine alone. This letter considers an optimal task-allocation problem for human–machine collaborative manufacturing systems, where various tasks are dispatched to human operators and automated machines to achieve optimal joint human-system performance. Designing such optimal task allocation is challenging because of the stochastic hybrid feature of manufacturing processes, as well as varying human performance caused by physical fatigue. To address this challenge, we first model human fatigue as a continuous-time Markov decision process, which is capable of capturing stochastic uncertainties on fatigue dynamics under different task assignments. A novel controlled stochastic petri net is then proposed to model the manufacturing process, in which both time- and event-driven dynamics can be regulated by task allocation between the human and machine. Under mild assumptions, we show that the optimal task-allocation problem under the proposed human manufacturing framework can be solved by linear programming. Simulation results of a four-part assembly process are used to verify our theoretical findings.

This paper deals with the identification of time Petri net systems. An identification algorithm for timed net systems must take into account that the firing of a transition requires not only that the enabling condition is met, as in untimed net systems, but it is also required that the firing interval of a transition is congruent with the observed firing instant times. The key idea behind the approach is to express these conditions by a set of logical propositions that can be directly transformed into linear mixed-integer inequalities. The identification algorithm consists of building the logical propositions from the observed behavior and solving a mixed-integer linear programming problem.

State Class Graph is a very useful tool to analyse Time Petri nets properties. It generates however a states explosion problem in large Petri nets. This can be overcome by using unfolding technique, which still imposes restrictions on time analysis. This paper proposes a relaxation in the unfolding process, which generates a new occurrence net, in which all temporal sequences are preserved.

The above paper [1] proposes a method to reduce simultaneously a Petri net model and the linear constraints. The reduced result preserves the control specification and the liveness. This note shows via some simple counterexamples that some results claimed in the above paper are incorrect, and then presents the corresponding corrections for two of the results.

For bounded Petri nets, Cabasino et al. propose a diagnosability test method that is based on the analysis of a modified basis reachability graph and a basis reachability diagnoser. However, its complexity is exponential in the number of nodes of the basis reachability diagnoser. In order to reduce the complexity of their method, this paper presents a new diagnosability test approach for bounded Petri nets. We present the concept of an extended basis reachability graph and prove that our approach is of polynomial complexity in the number of nodes of extended basis reachability graphs. An example is given to illustrate the application of the presented approach.

In this paper, a compact representation of the reachability graph of a Petri net is proposed. The transition set of a Petri net is partitioned into the subsets of explicit and implicit transitions in such a way that the subnet induced by implicit transitions does not contain directed cycles. The firing of implicit transitions can be abstracted so that the reachability set of the net can be completely characterized by a subset of reachable markings called basis makings . We show that to determine a max-cardinality- $T_{I}$ basis partition is an NP-hard problem, but a max-set- $T_{I}$ basis partition can be determined in polynomial time. The generalized version of the marking reachability problem in a Petri net can be solved by a practically efficient algorithm based on the basis reachability graph. Finally, this approach is further extended to unbounded nets.

In this paper, we focus on two notions of diagnosability for labeled Time Petri net (PN) systems: $K$ -diagnosability implies that any fault occurrence can be detected after at most $K$ observations, while $\tau$ -diagnosability implies that any fault occurrence can be detected after at most $\tau$ time units. A procedure to analyze such properties is provided. The proposed approach uses the Modified State Class Graph, a graph the authors recently introduced for the marking estimation of labeled Time PN systems, which provides an exhaustive description of the system behavior. A preliminary diagnosabilty analysis of the underlying logic system based on classical approaches taken from the literature is required. Then, the solution of some linear programming problems should be performed to take into account the timing constraints associated with transitions.

To enforce linear constraints on Petri nets that are partially controllable and observable, this work proposes an approach based on constraint transformation. First, a state-space equation of a Petri net control system based on event feedback is obtained by expressing a control action as a matrix, and the optimal control policy is designed. However, this policy needs to solve a nonlinear program on line. Second, pre-transition-gain-transformation is proposed to equivalently transform a constraint into a disjunction of new ones for an uncontrollable transition, and, similarly, post-transition-gain-transformation to transform a constraint into a disjunction of new ones for an unobservable transition. An algorithm is then given to transform a constraint into a disjunction of admissible ones, and, consequently, an efficient policy, which may not be optimal, can be designed. Third, in order to guarantee that the policy be both efficient and optimal, a dynamic linear constraint is introduced. Further, observing-transformation is proposed to simplify a dynamic constraint for an unobservable transition, and an algorithm is given to equivalently transform a class of linear constraints into admissible dynamic ones. As a result, an optimal controller requiring little online computation can be designed accordingly for some class of Petri nets. Finally, a maze system is used to illustrate the theoretical results.

The main purpose of this correspondence is to point out the fallacy of Theorem 1 in the paper that is mentioned in the title, a result that attempts to provide a structural characterization for the liveness of the Petri net class considered in the manuscript. The closing part of the correspondence also takes this opportunity to make some further remarks on the results that are claimed in the paper.

Extended logical Petri nets are proposed to improve logical Petri nets, and the related firing rules and state reachability graph are introduced. Their attributes, place arrival time, and priority function are defined for each token, batch processing wait time and transition firing duration are defined for each logical input/output transition, and firing duration is defined for each ordinary transition. Their token removal and generation functions are defined to operate the attributes and arrival time of tokens in places. A state in their reachability graph is redefined. They are used to model an e-commerce system. The reachability, time cost superiority of tokens with different priorities, and fairness of the resulting model are analyzed and correct end-states are illustrated.

This paper proposes the synthesis of Petri net supervisors based on a think-globally-act-locally (TGAL) approach and a vector covering technique for flexible manufacturing systems. Given a Petri net model with deadlocks, the TGAL approach first temporarily adds a global idle place (GP). A GP has initially only one token. Then, we generate the reachability graph of the net model with the GP. If there are deadlocks, we find all the legal markings and first-met bad markings (FBMs). The legal markings and FBMs that need to be considered can be reduced by using a vector covering approach. An integer linear programming problem is formulated to design a set of control places to forbid all FBMs but no legal markings. Meanwhile, the redundancy of the obtained control places is checked to remove the redundant ones. Then, we increase one token in the GP and compute a set of control place again. This process is carried out until the reachable markings of the Petri net model do not increase when the number of tokens in the GP is increased. As a result, we can find a set of control places to make the Petri net model live. Finally, some Petri net examples from the literature are used to demonstrate the proposed methods. It can be verified that the obtained supervisors can lead to more reachable markings, since the obtained control places are maximally permissive at each iteration.

This paper proposes a Petri net (PN) representation of the activities performed by the key human operators for unloading/loading containers in an intermodal maritime container terminal (CT) with a low level of automation. These processes are the core of the export, import, and transshipment cycles executed in the terminal. The aim of this paper is to consider both the human component and the material handling resources, e.g., cranes and transporters, by defining an accurate model, which describes how to coordinate humans and use the system resources necessary for serving mother or feeder ships. The developed generalized stochastic PN-based model is of limited complexity and represents a complete, unambiguous, and readable model of the target process before coding it in the target simulation tool. The modular integrated model is tested and validated by the simulation of typical and perturbed scenarios of the Taranto CT, a real terminal that is taken as a case study for its complexity and similarity to CTs with multiple transport modes.

Observation structures considered for Petri net generators usually assume that the firing of transitions may be observed through a static mask and that the marking of some places may be measurable. These observation structures, however, are rather limited, namely they do not cover all cases of practical interest where complex observations are possible. We consider in this paper more general ones, by correspondingly defining two new classes of Petri net generators: labeled Petri nets with outputs (LPNOs) and adaptive labeled Petri nets (ALPNs). To compare the modeling power of different Petri net generators, the notion of observation equivalence is proposed. ALPNs are shown to be the class of bounded generators possessing the highest modeling power. Looking for bridges between the different formalisms, we first present a general procedure to convert a bounded LPNO into an equivalent ALPN or even into an equivalent labeled Petri net (if any exists). Finally, we discuss the possibility of converting an unbounded LPNO into an equivalent ALPN.

The main contribution of this note is to propose algorithms that incrementally compute control sequences that drive the marking of timed Petri nets from an initial value to a reference one with a duration that approaches the minimal duration. These algorithms are based on a partial exploration of the reachability graph that is inspired from model predictive control. They include perturbation rejection and forbidden marking avoidance and are suitable to track trajectories when the initial and reference markings are far from each other. Application cases illustrate the efficiency of the method.

The dynamic behavior of traffic lights regulating a network of intersections can be viewed as a complex discrete-event system that can be modeled and controlled by Petri nets. In this paper, a bilayer signalized control method is presented. In the lower layer, a colored stochastic Petri net controls the signal indication displays and stage transitions. In the upper layer, a supervisory logic layer decides which stage should be serviced next. The proposed model increases modularity, reduces complexity, and, more importantly, is capable of being used to implement various signal control strategies. The method is used to implement four different control strategies: pretimed control, fully actuated control, semiactuated control, and random stage selection (as a benchmark) in the context of a signalized traffic network containing six intersections. Extensibility and future potential research to further enhance the proposed method are discussed and proposed at the end.

In this paper, we develop an analytical model based on stochastic Petri nets to capture the dynamics between adversary behavior and defense for cyber physical systems. We consider several types of failures including attrition failure, pervasion failure, and exfiltration failure which can happen to a cyber physical system. Using a modernized electrical grid as an example, we illustrate the parameterization process. Our results reveal optimal design conditions, including the intrusion detection interval, and the redundancy level, under which the modernized electrical grid's mean time to failure is maximized. Further, there exists a design tradeoff between exfiltration failure, attrition failure, and pervasion failure when using redundancy to improve the overall system reliability.

We consider the problem of verifying quantitative reachability properties in stochastic models of concurrent activities with generally distributed durations. Models are specified as stochastic time Petri nets and checked against Boolean combinations of interval until operators imposing bounds on the probability that the marking process will satisfy a goal condition at some time in the interval $[\alpha, \beta ]$ after an execution that never violates a safety property. The proposed solution is based on the analysis of regeneration points in model executions: a regeneration is encountered after a discrete event if the future evolution depends only on the current marking and not on its previous history, thus satisfying the Markov property. We analyze systems in which multiple generally distributed timers can be started or stopped independently, but regeneration points are always encountered with probability 1 after a bounded number of discrete events. Leveraging the properties of regeneration points in probability spaces of execution paths, we show that the problem can be reduced to a set of Volterra integral equations, and we provide algorithms to compute their parameters through the enumeration of finite sequences of stochastic state classes encoding the joint probability density function (PDF) of generally distributed timers after each discrete event. The computation of symbolic PDFs is limited to discrete events before the first regeneration, and the repetitive structure of the stochastic process is exploited also before the lower bound $\alpha$ , providing crucial benefits for large time bounds. A case study is presented through the probabilistic formulation of Fischer's mutual exclusion protocol, a well-known real-time verification benchmark.

In this paper, we consider the problem of developing a microscopic model for a signalized traffic intersection using Petri nets (PNs). We propose a two-module timed PN representation, where the first module is to model the traffic intersection and the second module is to model its traffic signal system. We use both deterministic and stochastic transitions in our model, and we describe in detail how they operate by considering both the event and time constraints associated with the physical traffic intersection. We also compare our model with some existing models in literature, and we explicitly state the potential advantages of our model.

The reversible released form (RRF) of Petri nets is introduced as an extension of the released form. This new form introduces undo transitions in order to reverse the effect of some of the transitions of the original Petri net. It is shown that the RRF preserves the soundness property of workflow (WF) nets: a WF net is sound if and only if its RRF is sound too. Then, various properties of the RRF of circuit-based Petri nets are investigated, and complexity results of the soundness property of circuit-based WF nets are derived.

This technical note is concerned with the structural sequence detectability problem in Free Choice Interpreted Petri nets, i.e., with the possibility of recovering the firing transition sequence in Free Choice Interpreted Petri nets using the output information when the initial marking is unknown. Based on the Free Choice Interpreted Petri net structure, three relationships are proposed which are devoted to capture the confusion over the transitions. These relationships depend on interpreted Petri nets structures such as $T-invariants$ , $P-Invariants$ , attribution, and distribution places. Thus, the approach herein presented exploits the interpreted Petri nets structural information in order to determine the structural sequence detectability of an interpreted Petri net.

This paper proposes a fully expanded tree (FET) approach for one-place-unbounded Petri nets. The FET of a one-place-unbounded Petri net consists of all and only reachable markings from its initial marking. Its applications to liveness and deadlock analysis for such Petri nets are developed. The proposed method has a larger application scope than all the existing methods for them. Several examples are provided to show its superiority over the state-of-the-art methods.

Liveness of Petri nets means all activities in a modeled system can potentially take place and thus implies deadlock freedom. The research on liveness analysis approaches is inadequate. This paper proposes a liveness judgment reachability graph (LJRG) approach to analyze the liveness of $ {\omega }$ -independent Petri nets. Such nets can be loosely explained as a class of unbounded Petri nets in which the changes of tokens in unbounded places are not related to each other. This paper proposes several algorithms to transform a new modified reachability tree to a new modified reachability graph and then transform it to an LJRG. It then develops the application of LJRG into the liveness analysis of $ {\omega }$ -independent unbounded Petri nets. The proposed method provides a new theoretical method and important tool for the liveness analysis of unbounded Petri nets. It is illustrated via some examples.

Homing of stem cells to the sites of injury is crucial for tissue regeneration. Stromal derived factor 1 (SDF-1) is among the most important chemokines recruiting these cells. Unexpectedly, our previous experimental data on mouse models of acute kidney injury showed that SDF-1 has a declining trend following ischemic kidney insult. To describe this unforeseen observation, a stochastic Petri net model of SDF-1 regulation in the hypoxia pathway was constructed based on main related components extracted from literature. Using this strategy, predictions regarding the underlying mechanisms of SDF-1 kinetics are generated and a novel incoherent feed forward loop regulating SDF-1 expression is proposed. The computational approach suggested here can be exploited to propose novel therapies for debilitating disorders such as kidney injury.

In this paper we contrast the application of two different methods for verifying soundness of workflow. The first approach considers the structure of the workflow net and proposes an analytical process that takes into account the incidence matrix and a strict positive vector to prove soundness. The second method is based on decision process Petri nets theory showing that the problem of finding an optimum trajectory for validation of well-formed workflow is solvable. The advantage of both solutions is that to tackle the soundness verification problem use the Lyapunov stability theory which corresponds to an analytical method for Petri nets. We validate our statement theoretically and by an application example.

As a powerful analysis tool of Petri nets, reachability trees are fundamental for systematically investigating many characteristics such as boundedness, liveness and reversibility. This work proposes a method to generate a reachability tree, called ωRT for short, for a class of unbounded generalized nets called ω-independent nets based on new modified reachability trees (NMRTs). ωRT can effectively decrease the number of nodes by removing duplicate and ω-duplicate nodes in the tree, and verify properties such as reachability, liveness and deadlocks. Two examples are provided to show its superiority over NMRTs in terms of tree size.

A polynomial algorithm for the sensor placement for observability problem in Continuous timed Petri nets (ContPN) is presented. Afterwards, an observer design with a single observer structure is proposed to avoid the classical approach requiring one observer for each LS, which becomes prohibited in classes of ContPN. In addition, this observer has the feature that it presents global and finite time convergence to the marking of the ContPN. The effectiveness of our approach is shown through illustrative examples.

In this paper, an adaptive Petri net (PN), capable of adaptation to environmental changes, is introduced by the fusion of learning automata and PN. In this new model, called learning automata-based adaptive PN (APN-LA), learning automata are used to resolve the conflicts among the transitions. In the proposed APN-LA model, transitions are portioned into several sets of conflicting transitions and each set of conflicting transitions is equipped with a learning automaton which is responsible for controlling the conflicts among transitions in the corresponding transition set. We also generalize the proposed APN-LA to ASPN-LA which is a fusion between LA and stochastic PN (SPN). An application of the proposed ASPN-LA to priority assignment in queuing systems with unknown parameters is also presented.

A Markovian Petri net (MPN) is a stochastic discrete event system (DES) frequently used for qualitative analysis, performance evaluation, and control purposes. In the past, the fluidization has been proposed in different DES formalisms (Markov chains, queuing networks, stochastic Petri nets (PNs), stochastic process algebra, etc.) as a relaxation technique for avoiding the state-explosion problem. Following that kind of approach, in this paper, a new hybrid PN model is defined as a partial relaxation of an original MPN. Nevertheless, it is shown through a simple example that such a partial relaxation can be worse than a full relaxation (given by a fully continuous PN), if certain conditions are not meet. Therefore, the rest of this paper is devoted to analyze the approximation of MPNs by means of hybrid PNs, where both the discrete and the continuous parts are stochastic. It is demonstrated that under certain conditions, the average and probability distribution function of the marking of a MPN can be approximated by those of the marking of the corresponding hybrid PN. The key point is to recognize the variability in behavior due to the time stochasticity. In some sense, a kind of functional central limit approach is obtained in a hybrid context.