In this paper, we focus on two properties related to the privacy of partially observable discrete event systems: state-trajectory opacity and initial-state opacity. Both properties are trajectory-dependent, meaning that if a trajectory violates the property, all of its continuations will also violate it. Our contribution lies in demonstrating that the verification of these two properties can be addressed using the notion of fault diagnoser. Specifically, we define two ad hoc automata — one for each property — and show that, by analyzing their respective diagnosers, the properties can be verified. While the complexity of our method is the same as that of other state of the art procedures, our approach opens the door to tackling complex problems by combining approaches developed within two areas of opacity and diagnosis.

With the continuous development of industries such as wind power and construction, the weight and complexity of lifted equipment have significantly increased. These lifting tasks often rely on crawler cranes, and the demand for cooperative lifting using dual crawler cranes has grown. However, current operations remain largely manual, leading to safety risks and low efficiency. While extensive research has been conducted on the coordination of overhead cranes and other lifting systems, studies on cooperative control of crawler cranes are still in their early stages and have received insufficient attention. To address this issue, this paper establishes an accurate model of a dual crawler crane system using Lagrange equations. Motion constraints are incorporated to reduce the original fifth-order dynamics to a third-order system, simplifying control implementation. Given the strong coupling characteristics of the underactuated system, a PID-based coupled error compensation control method is proposed to regulate the load’s position and attitude precisely. By coordinating cable length adjustments, the proposed method ensures stable and accurate positioning while guaranteeing finite time convergence of cable length errors. Finally, a wind turbine installation scenario is simulated to validate the effectiveness of the proposed control approach.

In this paper, we study the problem of fault diagnosis in Switching Output Automata (SOA), which is a formal modeling framework particularly suitable for describing artificial systems with discrete or quantized piecewise continuous outputs. We introduce Switching Output Automata with Faults (SOAF), an extension of SOA that incorporates timed fault arcs to model fault occurrences under specific temporal constraints. In our framework, faults are defined with respect to both the discrete states and the system outputs, where each fault occurrence is constrained to specific time intervals determined by the current global state of the system. To perform fault diagnosis, we introduce the Evolution Automaton with Faults (EAF), a nondetermistic finite automaton that serves as a logical abstraction of the SOAF. Based on the approach of Sampath and Lafortune, we construct a diagnoser for EAF that effectively performs fault diagnosis in the SOAF framework.

In this paper, the problem of cyber-attacks detection in timed probabilistic discrete event systems via artificial neural networks is investigated. We extend the problem of state estimation for timed probabilistic discrete event systems using artificial neural networks, to address attack detection. So that, a detection strategy is implemented to determine whether the system is operating in normal mode or under attack, and to identify the potential type of attack. Two primary cases are examined: (i) attack detection over observations. In this case, the attack detector recognizes whether the system is in a normal mode or an attack mode after each new observation, (ii) attack detection over time. Here, the attack detector evaluates the system’s status at each clock time increment.

We present a new discrete event model called switching output automaton where with each state is associated a set of discrete output values. The evolution of such a system, as state and output change, produces as observation a piecewise constant signal. The goal of this paper is that of designing a suitable observer for estimating the current discrete state of this model as a function of the observed output signal. In addition, we show how the observer can be used to verify if the system is current-state opaque.

Rumor spreads fast in social networks and may seriously damage our society. In this article, we present a mathematical programming formulation based on integer linear programming (ILP) to minimize rumor spread by blocking a subset of nodes (called blockers) in complex social networks modeled as a linear threshold model. We also propose a modified approach which solves the top-$k$blockers problem with a reduced computational effort and formally proves that its performance is still optimal. Then, the presented method is evaluated for its effectiveness of containing rumor spread in four different networks and its performance is compared with a greedy-based and two centrality-based approaches. The experimental analysis shows that the ILP-based method outperforms the other three approaches and is applicable to large-scale networks.

This article proposes a semi-structural approach to verify thenonblockingnessof a Petri net. We construct a structure, called minimal-maximal basis reachability graph (min-max-BRG): it provides an abstract description of the reachability set of a net while preserving all information needed to test if the net isblocking. We prove that a bounded deadlock-free Petri net isnonblockingif and only if its min-max-BRG isunobstructed, which can be verified by solving a set of integer constraints and then examining the min-max-BRG. For Petri nets that are not deadlock-free, one needs to determine the set of dead markings. This can be done with an approach based on the computation ofmaximal implicit firing sequencesenabled by the markings in the min-max-BRG. The approach we developed does not require the construction of the reachability graph and has wide applicability.

In this paper we consider timed automata endowed with a single clock that is reset at each event occurrence. A time interval is associated with each transition specifying at which clock values it may occur. We assume that the (logical and timed) structure of a timed automaton is known, and event labels associated with transitions are not observable. The problem addressed in this paper is to estimate and update the set of possible current discrete states as time elapses without any observation being received. By a partitioning of time intervals into regions, we design a λ-observer (λ is the null observed sequence) that, for a given state and a current time value, estimates the set of possible current states and the corresponding regions to which the timer value associated with each possible current state may belong.

In this paper, a two-step approach for on-line fault diagnosis of timed discrete event systems modeled with max-plus automata is presented. The set of events is divided into two disjoint subsets, i.e., observable and unobservable subsets, and failures are associated to unobservable ones. Once a sequence of pairs (event, time-instant) is observed, the fault diagnosis problem consists in detecting an abnormality of the system evolution and isolating the source of this abnormality. For a max-plus automaton, we first propose an algorithm to build its augmented version whose states are partitioned into two disjoint parts, the normal part and the faulty part, with respect to a given fault class. Then we prove that solving fault diagnosis of the original automaton is equivalent to estimating the states of the augmented automaton. Finally, an algorithm is proposed to summarize how to perform on-line fault diagnosis using a state estimation based approach.

Cyber-physical systems have emerged as a key technology in the development of distributed and autonomous large scale systems. However, one of their undesirable side effects is the fact that they are particularly exposed to cyber attacks carried out by malicious intruders. Therefore, efficient strategies for cyber security are in high demand. In this paper, we consider the issue of attack detection in the framework of partially observable discrete event systems modeled by finite automata. We assume that the observation produced by a plant can be corrupted by an intruder which, through one or more attack dictionaries, can change events into different strings. The problem we address is that of detecting if a plant has been attacked and, if such is the case, of identifying the nature of the attack, i.e., which attack dictionaries have been used. We show that the problem of attack detection can be reduced to a classical problem of state estimation or fault diagnosis for a new structure which describes the behavior of the plant under attack.

Identification of a final state after red a test is one of the fundamental testing problems for discrete event systems and synchronizing sequences represents a conventional solution to this problem. In this paper, we consider systems modeled by a special class of synchronized Petri nets, called 1-place-unbounded, that contain a single unbounded place. The infinite reachability spaces of such nets can be characterized by two types of finite graphs, called improved modified coverability graph and weighted automata with safety conditions. In case these two finite graphs are deterministic, we develop novel computation algorithms for synchronizing sequences for this class of nets by decomposing the finite graphs into strongly connected components.

Based on the concepts of word-of-mouth effect and viral marketing, the diffusion of an innovation may be triggered starting from a set of initial users. Estimating the influence spread is a preliminary step to determine a suitable or even optimal set of initial users to reach a given goal. In this paper, we focus on a stochastic model called the Independent Cascade model, and compare a few approaches to compute activation probabilities of nodes in a social network, i.e., the probability that a user adopts the innovation. In the paper, first we propose the Path Method which computes the exact value of the activation probabilities but it has high complexity. Second an approximated method, called SSS-Noself, is obtained by modification of the existing Steady State Spread algorithm, based on fixed-point computation, to achieve a better accuracy. Finally an efficient approach, also based on fixed-point computation, is proposed to compute the probability that a node is activated though a path of minimal length from the seed set. This algorithm, called SSS-Bound-t algorithm, can provide a lower-bound for the computation of activation probabilities.

The propagation of innovations in social networks has been widely studied recently. Previous research mostly focuses on either maximizing the influence by identifying a set of initial adopters, or minimizing the influence by link blocking under a certain diffusion model. In our case, we address an influence maximization problem considering the link activation under the Independent Cascade model. For this problem, we propose an approximate solution based on the computation of a cost-degree coefficient for selecting links to be activated. Simulations performed on a real network show that our algorithm performs well.

The problem of stealthy attacks for partially-observed discrete event systems is considered. An operator observes the plant through an observation mask that does not allow him to detect the occurrence of certain events (silent events). The observation is corrupted by an intruder who can insert and erase some sensor readings. We construct an attack structure A which guarantees that, when the plant reaches an unsafe state, A can make the operator think that the plant is in a safe state. Based on A, we can obtain a stealthy attack structure As by simply removing from A all the exposing states, all the weakly exposing states and their input and output arcs. The stealthy attack structure As only contains the possible attacks that can not be detected by the operator.

Timed marked graphs, a special class of Petri nets, are extensively used to model and analyze cyclic manufacturing systems. Weighted marked graphs are convenient to model systems with bulk services and arrivals. We consider two problems of practical importance for this class of nets. The marking optimization problem consists in finding an initial marking to minimize the weighted sum of tokens in places, while the average cycle time is less than or equal to a given value. The cycle time optimization problem consists in finding an initial marking to minimize the average cycle time, while the weighted sum of tokens in places is less than or equal to a given value. We propose two heuristic algorithms to solve these problems. Several simulation studies show that the proposed approach is significantly more efficient than existing ones.

For modelling and analysis of automated production systems as batch or high throughput systems, timed Petri nets are commonly used. In this paper, we deal with the marking optimization problem of a timed weighted marked graphs under infinite server semantics. The problem consists in finding an initial marking to minimize the weighted sum of tokens in places while the average cycle time is less than or equal to a given value. We propose two different heuristic approaches to solve the optimization problem.

This paper develops a decentralized supervision policy for a Petri net through collaboration between a coordinator and subnet controllers. The coordinator is chosen from the subnet controllers by solving an integer linear programming problem. An optimal objective function is used to minimize the communication cost between the subnet controllers and the coordinator. Furthermore, a protocol to reach an agreement on the firing conditions of common transitions among the subnet controllers is proposed. Observation agreement and control agreement can be achieved by the “AND” operator in logic algebra. Control agreement is used to decide the firing conditions of common transitions in the next step. The firing of common transitions, which will lead to a new marking that violates the given constraints, will be forbidden by the control agreement. A feasibility analysis of the proposed decentralized control framework is discussed. Finally, four examples are presented to illustrate the proposed approach.

In this paper, we focus on labeled Petri nets with silent transitions that may either correspond to fault events or to regular unobservable events. We address the problem of deriving a procedure to determine if a given net system is diagnosable, i.e., the occurrence of a fault event may be detected for sure after a finite observation. The proposed procedure is based on our previous results on the diagnosis of discrete-event systems modeled with labeled Petri nets, whose key notions are those of basis markings and minimal explanations, and is inspired by the diagnosability approach for finite state automata proposed by Sampath in 1995. In particular, we first give necessary and sufficient conditions for diagnosability. Then, we present a method to test diagnosability that is based on the analysis of two graphs that depend on the structure of the net, including the faults model, and the initial marking.

Synchronizing sequences have been proposed in the late 1960s to solve testing problems on systems modeled by finite-state machines. Such sequences lead a system, seen as a black box, from an unknown current state to a known final one. This paper presents a first investigation of the computation of synchronizing sequences for systems modeled by synchronized Petri nets. In the first part of the paper, existing techniques for automata are adapted to this new setting. Later on, new approaches, that exploit the net structure to efficiently compute synchronizing sequences without an exhaustive enumeration of the state space, are presented.

A remark related to our recent paper is made. Using a counterexample we show that we need more strict assumptions with respect to those used to prove that if a system is diagnosable in a decentralized setting, then it is also diagnosable in a centralized one. Specifically, we require that the central diagnoser sees all the events that can be seen by all the local diagnosers, and that the central diagnoser can distinguish all observable events that the local diagnosers can distinguish on their own.

In this paper a type of specifications called OR-GMEC for place/transition nets is defined. Such a specification consists of a set of disjunctive Generalized Mutual Exclusion Constraint, i.e. the requirement is that, at any given time, the controlled system should satisfy at least one of them. We show that a bounded OR-GMEC can be enforced by a special control structure composed by a set of monitor places (one for each constraint) plus a switcher that determines the current active constraint. We also show that such a simple control structure is not maximally permissive, and characterize this problem identifying a special subset of transitions that may be over-restricted. A modified controller that ensures maximal permissiveness is also presented. Finally, we discuss a particular control problem, that consists in preventing the firing of a given set of transitions and show that it can be reduced to an OR-GMEC problem.

Observation structures usually considered for Petri nets assume that the firing of transitions may be observed through static labels and that the marking of some places may be measurable. These observation structures are rather limited and we consider in this paper more general ones, correspondingly defining two new classes of nets: labeled Petri nets with outputs and adaptive labeled Petri nets. Several examples of nets in these classes are considered. Furthermore we also show the possibility to convert a labeled Petri net into an adaptive Petri net or a labeled Petri net.

In this paper, we propose an approach to the diagnosis of Petri nets in a decentralized setting that combines the decentralized scheme for automata presented by Debouk with the diagnosis approach for Petri nets based on the notion of basis markings and justifications presented by some of the authors of this paper. The decentralized architecture that we use is composed of a set of sites communicating their diagnosis information with a coordinator that is responsible for detecting the occurrence of failures in the system. In particular, we define three protocols that differ in the amount of information exchanged between the local sites and the coordinator and the rules adopted by the coordinator to compute the global diagnosis states. Finally, we prove that, as in the case of automata, diagnosability is strictly related to the presence of failure ambiguous strings.

A commonplace assumption in the fault diagnosis of discrete event systems (DESs) is that of modeling faulty events with unobservable transitions, i.e., transitions whose occurrence does not produce any observable label. The diagnostic system must thus infer the occurrence of a fault from the observed behavior corresponding to the firing of nonfaulty transitions. The presence of nonfaulty unobservable transitions is a source of additional complexity in the diagnostic procedure. In this paper, we assume that fault events can also be modeled by observable transitions, i.e., transitions whose occurrence produces an observable label. This does not mean, however, that the occurrence of such a transition can be unambiguously detected: In fact, the same label may be shared with other fault transitions (e.g., belonging to different fault classes) or with other nonfaulty transitions. We generalize to this new setting our previous results on the diagnosis of DESs using Petri nets based on the notions of minimal explanations and basis markings. The presented procedure does not require the enumeration of the complete reachability set but only of the subset of basis markings, thus reducing the computational complexity of solving a diagnosis problem.

We consider the scenario of a Wireless Sensor Networks (WSN) where the nodes are equipped with a programmable middleware that allows for quickly deploying different applications running on top of it so as to follow the changing ambient needs. We then address the problem of finding the optimal deployment of the target applications in terms of network lifetime. We approach the problem considering every possible decomposition of an application's sensing and computing operations into tasks to be assigned to each infrastructure component. The contribution of energy consumption due to the energy cost of each task is then considered into local cost functions in each node, allowing us to evaluate the viability of the deployment solution. The proposed algorithm is based on an iterative and asynchronous local optimization of the task allocations between neighboring nodes that increases the network lifetime. Simulation results show that our framework leads to considerable energy saving with respect to both sink-oriented and cluster-oriented deployment approaches, particularly for networks with high node densities and non-uniform energy consumption or initial battery charge.

In this paper the formation stabilization problem for a system of heterogeneous agents is considered. Agents are characterized by different linear dynamics, and assumed to be able to collaborate by exchanging information if they are within their range of communication. A sufficient algebraic condition for the stability of the formation based on a generalization of the Gerschgorin circle theorem for block matrices is proposed. Furthermore, conditions under which the formation remains stable under switching topology are investigated. Simulation results are given to corroborate the theoretical results.

In this paper we consider a software tool for the simulation and analysis of discrete, continuous and hybrid Petri nets, called HYPENS. It is an open source tool we have recently developed in Matlab. The main contribution of this paper is that of demonstrating the efficiency of HYPENS via real several non trivial examples. In particular, we consider a family of purely discrete event systems modeling a queueing network, and a job shop system with finite capacity buffers and unreliable multi-class machines. A detailed analysis of the computational times and of the accuracy of the results is proposed. In particular, in the first case example, that is modeled using discrete Petri nets, the correctness of the results is proved using well known analytical results from the queueing theory.

In this paper, we deal with the problem of modeling railway networks with Petri nets so as to apply the theory of supervisory control for discrete event systems to automatically design the system controller. We provide a modular representation of railway networks in terms of stations and tracks including sensors and semaphores. We first ensure safeness and local liveness imposing both generalized mutual exclusion constraints and constraints also involving the firing vector. The detailed model used in this first step can be abstracted, considering a higher level description of a railway network that belongs to the class of ES PR (extended simple sequential process with resources) nets and show that global liveness may be enforced by adding appropriate monitor places designed using siphon analysis. In our approach, this can be done without an exhaustive computation of all siphons and we can characterize the cases in which the procedure can be recursively applied, giving a simple test for closed-loop net to remain an ES PR net.

Power Management mechanisms are widely adopted in Wireless LANs to achieve appreciable power saving. In DCF iBSS networks, all stations in doze mode with pending frames are awaken by the AP at the beginning of next beacon interval. Such stations then switch to the active mode for the reception of the frames. In this work, we propose a different power management technique based on giving the AP the power of deciding which stations with pending frames to wake up. Indeed, there are several circumstances with high channel traffic in which it is better to defer the transmission so as to reduce the expected energy consumption. The AP decision is taken in view of the energy consumption due to collisions and transmissions together with the introduced latency. Through simulations, we show the performance of the proposed method, which may lead to an overall energy saving of about 40 % respect to the standard Power Management.

In this paper we deal with the problem of determining a set of decentralized controllers for P/T nets that are able to impose a given global specification on the net behaviour. More precisely, both the global specification and the decentralized specifications are given in terms of generalized mutual exclusion constraints (GMECs) thus the controllers take the form of monitor places. In this paper we provide some preliminary results that are a first step towards a more general and systematic approach to the problem. The lines of our future research in this topic are described in details in the last section, devoted to conclusions and future works

In this paper we consider a quantized discrete-time linear quadratic regulator (DLQR) problem, namely a DLQR problem where the input u may only take values in a given finite set 14. Eased on our previous results on the optimal control of hybrid systems we show that the optimal control law for the quantized DLQR problem takes the form of a feedback control law, that can be obtained from a partition of the state space C, computed off-line. The numerical simulations carried out enabled us to observe a particular structure of C, related to the solution of the non-quantized DLQR problem. The lines of our future research in this topic are described in details in the last section, devoted to conclusions and future work

In this paper we deal with the problem of estimating the marking of a labeled Petri net with nondeterministic transitions. In particular, we consider the case in which nondeterminism is due to the presence of transitions that share the same label and that can be simultaneously enabled. Under the assumption that: the structure of the net is known, the initial marking is known, the transition labels can be observed, the nondeterministic transitions are contact-free, we present a technique for characterizing the set of markings that are consistent with the actual observation. More precisely, we show that the set of markings consistent with an observed word can be represented by a linear system with a fixed structure that does not depend on the length of the observed word.

a generalized mutual exclusion constraint (GMEC) is a linear constraint that limits the weighted sum of tokens in a subset of places of a place/transition net system. The corresponding controller takes the simple form of a monitor place that can be added to the net to obtain the closed-loop system. In this paper we extend this approach to the case of colored Petri nets, showing that a colored GMEC can express a set of linear constraints and can be enforced by a colored monitor place. We also develop a matrix representation of multisets that is useful for the design of the monitor place.

The real-time traffic control of railway networks authorizes movements of the trains and imposes safety constraints. The paper deals with the real time traffic control focusing on deadlock prevention problem. Colored Petri nets are used to model the dynamics of the railway network system: places represent tracks and stations, tokens are trains. The prevention policy is expressed by a set of linear inequality constraints, called colored Generalized Mutual Exclusion Constraints that are enforced by adding appropriate monitor places. Using digraph tools, deadlock situations are characterized and a strategy is established to define off-line a set of Generalized Mutual Exclusion Constraints that prevent deadlock. An example shows in detail the design of the proposed control logic.

Discusses the problem of controlling a Petri net whose marking cannot be measured but is estimated using an observer. The control objective is that of enforcing a set of generalized mutual exclusion constraints (GMEC) and all transitions are assumed to be controllable. The use of marking estimates (as opposed to the exact knowledge of the actual marking of the plant) leads to a worse performance of the closed-loop system and it may also be the case that, as a result of this, the controlled system reaches a deadlock. We present a general approach, based on siphon analysis, to recover from such an "observer induced" deadlock. The most interesting feature of our approach is that the observer, controller and deadlock recovery algorithms are all based on the same linear algebraic techniques, thus allowing the overall problem to be solved using a single formalism.

We deal with the problem of allocating a given number of tokens, so as to maximize the firing rate of a cyclic event graph with deterministic transition firing delays. We propose an incremental algorithm that is inspired by the algorithm formulated by Panayiotou and Cassandras (1999) for the case of kanban systems. The algorithm can be applied to a special class of nets in which tokens are allocated to places that belong to only one circuit: this class is powerful enough to model kanban systems. We provide necessary and sufficient conditions for the convergence to the optimum also in the case of multiple solutions.

We consider in this paper first-order hybrid Petri nets, a model that consists of continuous places holding fluid, discrete places containing a nonnegative integer number of tokens, and transitions, either discrete or continuous. We set up a linear algebraic formalism to study the first-order continuous behavior of this model and show how its control can be framed as a conflict resolution policy that aims at optimizing a given objective function. The use of linear algebra leads to sensitivity analysis that allows one to study of how changes in the structure of the model influence the optimal behavior. As an example of application, we show how the proposed formalism can be applied to flexible manufacturing systems with arbitrary layout and different classes of products.

We present a formulation for the optimal control of discrete event dynamic processes which represent production systems with unreliable machines and buffers of finite capacity. We derive an optimum control strategy that is critically based on the fact that the discrete event dynamic behavior of the system is approximately represented with a hybrid model. We introduce a deterministic fluid network model where the average flow rates through the machines are the control variables and with an original approach we show that the dynamics of the system easily translate into a discrete-time, time-varying state variable model, where the optimum machine production rates can be easily obtained by solving a sequence of linear programming problems.

In this paper we present a method for performance evaluation of hybrid stochastic Petri nets based on sensitivity analysis and parametric linear programming techniques and we show how this approach can be used for optimization. The problem is addressed by determining an optimal firing speed allocation for the continuous transitions obtained by solving a sequence of linear programming problems aimed at optimizing a certain performance index. The primary advantage of our approach is that it gives rise to a dynamic firing speeds allocation that is based on global state information rather than local information. This original formulation allows us to easily solve conflicts, evaluate performance measures and perform gradient estimation very efficiently.

Recent results in the literature have provided an efficient control synthesis technique for the problem of enforcing generalized mutual exclusion constraints on place/transition nets. With this technique both the plant and the controller are described by Petri nets in order to have an useful linear algebraic model for control analysis and synthesis. The synthesis is not computation demanding since it involves only matrix multiplications. Moreover the method has been shown to be maximally permissive in the case of controllable specifications, otherwise the controller may be suboptimal and its structure may not be unique. This paper investigates on and provides an algorithm to compute these control structures and two criteria of suboptimality.

A lumped-parameter model is considered for open-channel networks that expresses the dynamic relationship, in terms of state space variables, between gate opening sections and stored water volume variations in the different canal reaches with respect to a reference configuration of uniform flow. A procedure is suggested to approximate a real steady flow condition with an ideal uniform flow configuration. A decentralized control is obtained by determining the state feedback gain matrix, whose structure is imposed to be diagonal, that minimizes the H/sub 2/ norm of a suitable transfer matrix. A numerical validation of the linear model used to synthesize the control law is proposed. A comparison between the behaviour of the linear model and that of the non-linear unsteady one, whose evolution has been determined using the SIC software, is proposed.

The paper discusses how Petri nets may be used for the qualitative modeling of physical systems. The qualitative state of a system is represented by the marking of the net. The crossing of a landmark value corresponds to the firing of a transition. We give a formal procedure to construct a Petri net model corresponding to a given set of qualitative equations. The approach can be used to study both autonomous systems and systems with forcing inputs. The dynamic behavior of the system can be studied as sequences of reachable markings of the net and can be computed with standard Petri net execution techniques. This approach also leads to a simple framework for the study of hybrid systems, i.e., systems whose behavior is described by both continuous and discrete event dynamics. Several examples, with applications to diagnosis and control, are fully discussed.

The primary motivation for this research is to show how Petri nets may be efficiently used within the framework of supervisory control. In particular, the paper discusses how integer programming techniques for Petri net models may be used to validate supervisors for the control of discrete event systems. We consider a class of place/transition nets, called elementary composed state machines. The reachability problem for this class can be solved by a modification of classical incidence matrix analysis. In fact it is possible to derive a set of linear inequalities that exactly defines the set of reachable markings. Finally, we show how important properties of discrete event systems, such as the absence of blocking states or controllability, may be analyzed by integer programming techniques.>