Abstract The study of real discrete event systems requires the use of models to cope with complexity and large scale. The only way to understand and analyse their behaviour prior to implementation is, in practice, through distributed simulation. Although it is a widely studied discipline, the difficulty of developing efficient distributed simulation code remains a challenge. The use of model driven engineering approaches allows a smooth way from informal specifications to executable code showing traces of the system behaviour. Formal models allow to conduct the phases of this engineering process, and in this work, the formalism is Petri nets. In the simulation literature, Petri nets have been shown to be particularly suitable for modelling and simulation of discrete event systems. This article reviews the role of Petri nets as the core formalism to support a model‐driven engineering approach for the execution of large scale models using distributed simulation. It deals with different aspects related to the Petri net‐based languages used at different stages of the modelling and simulation process, from conceptual modelling of complex systems to the generation of code for executing simulations of Petri net‐based models. After the review, the article proposes an efficient representation of Petri net‐based models. It is analysed from the perspective of the essential properties required for distributed simulation, and was found to provide efficient execution, scalability and dynamic configuration. The article highlights the importance of considering modelling constraints in order to guarantee good properties such as liveness and structural boundedness of Petri net components for the execution of large‐scale Petri net models. The Petri net‐based methodology is illustrated from the perspective of the impact of the formalism to help developing well‐formed models and efficient code for distributed simulation.

The proliferation of sensors over the last years has generated large amounts of raw data, forming data streams that need to be processed. In many cases, cloud resources are used for such processing, exploiting their flexibility, but these sensor streaming applications often need to support operational and control actions that have real-time and low-latency requirements that go beyond the cost effective and flexible solutions supported by existing cloud frameworks, such as Apache Kafka, Apache Spark Streaming, or Map-Reduce Streams. In this paper, we describe a model-driven and stepwise refinement methodological approach for streaming applications executed over clouds. The central role is assigned to a set of Petri Net models for specifying functional and non-functional requirements. They support model reuse, and a way to combine formal analysis, simulation, and approximate computation of minimal and maximal boundaries of non-functional requirements when the problem is either mathematically or computationally intractable. We show how our proposal can assist developers in their design and implementation decisions from a performance perspective. Our methodology allows to conduct performance analysis: The methodology is intended for all the engineering process stages, and we can (i) analyse how it can be mapped onto cloud resources, and (ii) obtain key performance indicators, including throughput or economic cost, so that developers are assisted in their development tasks and in their decision taking. In order to illustrate our approach, we make use of the pipelined wavefront array.

BACKGROUND: Model checking has been recently introduced as an integrated framework for extracting information of the phylogenetic trees using temporal logics as a querying language, an extension of modal logics that imposes restrictions of a boolean formula along a path of events. The phylogenetic tree is considered a transition system modeling the evolution as a sequence of genomic mutations (we understand mutation as different ways that DNA can be changed), while this kind of logics are suitable for traversing it in a strict and exhaustive way. Given a biological property that we desire to inspect over the phylogeny, the verifier returns true if the specification is satisfied or a counterexample that falsifies it. However, this approach has been only considered over qualitative aspects of the phylogeny. RESULTS: In this paper, we repair the limitations of the previous framework for including and handling quantitative information such as explicit time or probability. To this end, we apply current probabilistic continuous-time extensions of model checking to phylogenetics. We reinterpret a catalog of qualitative properties in a numerical way, and we also present new properties that couldn't be analyzed before. For instance, we obtain the likelihood of a tree topology according to a mutation model. As case of study, we analyze several phylogenies in order to obtain the maximum likelihood with the model checking tool PRISM. In addition, we have adapted the software for optimizing the computation of maximum likelihoods. CONCLUSIONS: We have shown that probabilistic model checking is a competitive framework for describing and analyzing quantitative properties over phylogenetic trees. This formalism adds soundness and readability to the definition of models and specifications. Besides, the existence of model checking tools hides the underlying technology, omitting the extension, upgrade, debugging and maintenance of a software tool to the biologists. A set of benchmarks justify the feasibility of our approach.

This paper presents a modeling methodology for clinical guidelines used in hospitals. The clinical guidelines are assumed to be given in a graphical form in a structure obtained by combining few elements. It is shown how the clinical guidelines represented with this syntax can be automatically converted into a mathematical model represented as Petri nets. The main advantage of the new model is the inclusion of resources and patient flow in the same model which makes possible its use in analysis and verification of the guidelines. Moreover, if different clinical guidelines in a hospital or department in a hospital are considered, the models can be used for resource optimization and performance evaluation. The clinical guideline of hip fracture from the ”Lozano Blesa” University hospital in Zaragoza is taken as an example.

The disparity of Petri net models in the literature for the study of resource allocation problems in Flexible Manufacturing Systems (FMSs) is overwhelming. Paradoxically, those models often strongly overlap in terms of their modeling capability. Such clustering seems to be impelled by a mature knowledge of results which capsize liveness at the topological level of the FMS for families of models which comply with some properties of good behaviour. Not rarely, such properties are embraced at the expense of severe or inconsistent syntax restrictions paying slight regard to actual modelling requirements in the application domain of FMSs. In this paper, we promote a distillation of the current amalgam of subclasses and tangent results, proposing taxonomic categories that allow capturing the different capabilities of each kind of model and establishing a reference framework for past and future advances.

This paper provides a strategy for supervising the motion of some mobile robots that evolve in the same environment. Some regions of the environment are assumed to have a limited capacity in terms of the number of robots that can simultaneously occupy them, and a set of possible trajectories is available for each robot. The solution comprises the construction of a specific Petri net model for the available trajectories, and the use of resource-allocation techniques based on restricted-capacity regions and on deadlock-free execution.

The need for general-purpose algorithms for studying biological properties in phylogenetics motivates research into formal verification frameworks. Researchers can focus their efforts exclusively on evolution trees and property specifications. To this end, model checking, a mature automated verification technique originating in computer science, is applied to phylogenetic analysis. Our approach is based on three cornerstones: a logical modeling of the evolution with transition systems; the specification of both phylogenetic properties and trees using flexible temporal logic formulas; and the verification of the latter by means of automated computer tools. The most conspicuous result is the inception of a formal framework which allows for a symbolic manipulation of biological data (based on the codification of the taxa). Additionally, different logical models of evolution can be considered, complex properties can be specified in terms of the logical composition of others, and the refinement of unfulfilled properties as well as the discovery of new properties can be undertaken by exploiting the verification results. Some experimental results using a symbolic model verifier support the feasibility of the approach.

This paper presents a modular Petri net approach for modeling a health system. In particular, the Spanish national health system is considered as case study. After a global description of the health system structure, it is shown that it can be composed by different modules with inputs and outputs. Each module can be modeled separately and the procedure consists in two steps: (1) model the medical protocols as state-machine Petri nets and (2) add the (shared) medical resources. The global model is obtained by composing these modules by fusing the input and output places and adding information on the population. It is proved that by following these procedure, the obtained Petri net system is a S4PR. Finally, it is shown how the model can be exploited in order to check different properties of the system.

Distributed control for Agile Manufacturing Systems (AMSs) is an active research field. Many efforts are focused on the IEC 61499 standard, although there is still work to be done for its adoption by the industry. A part of this work is related to solve its semantic ambiguities derived from implementation-dependent issues. This paper presents the COSME platform, which uses an adapted component model, a specific execution model and a set of communication types for the distributed control of communicating machine tools in the context of Agile Manufacturing Systems. These models can be expressed in IEC 61499 terms. This adaptation facilitates application designing and implementation.

The long interest in finding efficient solutions to deadlock occurrence induced by resource sharing is persistent in the context of concurrent control software production. Petri net-based correction techniques which were traditionally applied in the context of flexible manufacturing systems (FMS) constitute a promising new approach. In this vein, Gadara nets were introduced as an attempt to import the strengths of these techniques into the software domain. In this paper, we prove that these Petri nets are close to a subclass of S4PR (a widely-exploited class in the context of FMS) and provide some related equivalence results. Some limitations which Gadara nets present for the modelling and automated correction of software are also unveiled. Last but no least, we present formal proofs of the theorems characterising non-liveness in Gadara nets. To our knowledge, no such proofs were published before.

Software involved in modern control applications is becoming increasingly complex, having to deal with newer and more sophisticated responsibilities. It must be now considered as a very relevant part in the mix of the system complexities and, unfortunately maybe very often, it is also an important source of engineering headaches. Its specific particularities should be conveniently taken into account using common software techniques. Design patterns are one of such techniques, widely used in the software world. The presented design pattern suggests a way to handle predictive maintenance, a service oriented to machine tools containing parts that suffer progressive deterioration which can be indirectly detected. This way, adequate maintenance actions can be scheduled just in time to avoid further problems development.

Minimal siphons in the class of S4PR nets have become a conceptual and practical central tool to deal with deadlocks caused by the sharing of resources in Flexible Manufacturing Systems. The availability of efficient algorithms to compute these structural objects is very important. In this paper we take advantage from the particular properties of the siphons in S4PR to obtain an efficient algorithm. These properties allow to compute the minimal siphons from a generating family of minimal siphons. This family is composed by the minimal siphons containing only one resource. The computation of the minimal siphons is based in the maximal strongly connected components of a graph representing the relations between the siphons of the generating family. The algorithm is very economic in memory in all intermediate steps with respect to the classical algorithms.

Multicomputer Interconnection Networks and the design of routing algorithms for these networks, is a very active research domain that in the last decade has given rise to technologically consolidated systems. Nevertheless, from the methodological point of view, the diverse approaches are very limited, moreover in many cases are not complete in order to cover the different phases of the design cycle. In this paper we present a complete design approach, supported by a methodology until to get a deadlock-free routing algorithm. The starting information is the topology of the interconnection network and the initial minimal routing algorithm elaborated by the designer. From this information we obtain a Petri Net model, allowing to characterize the deadlock situations, and, if necessary, to modify the algorithm in order to produce a deadlock-free minimal adaptive routing algorithm.

Formal models, as Petri nets, applied to the resource allocation problem have been a fruitful approach in the last years from a double perspective. Firstly, the consolidation of an abstraction process of systems leading to models structured around the concepts of processes and resources, which can be easily translated into Petri nets. Secondly, the obtention of analysis results characterizing deadlock states, as well as methods to amend the problem. Thanks to abstraction, this methods can be applied to many different application domains, although manufacturing is yet predominant. In this paper we follow the same philosophy, but extending the kind of systems that can be tackled. These extensions allow to consider nested iterations within the processes, and to hold resources in the initial state. We will show that these extensions are very relevant, from the real-world system point of view, in order to extend these techniques to a broader scope of scenarios. Nevertheless, the behaviours of the resulting models are much more complex than those of the previous restricted models, e.g., non-directedness.

A novel strategy for the logic synthesis of asynchronous control circuits is presented. It is based on the structural theory of Petri nets and integer linear programming. Techniques that are capable of checking implementability conditions, such as complete state coding, and deriving a gate netlist to implement the specified behavior are presented. These techniques can handle Petri net specifications consisting of several thousands of transitions and provide a significant speed-up compared with techniques that have previously been proposed

A new method for the deadlock prevention problem in concurrent systems where a set of processes share a set of common resources in a conservative way is proposed. It can be applied to flexible manufacturing systems, modeled with Petri nets. In this paper, we present a set of important results related to the deadlock prevention problem in S4PR nets. First, a liveness characterization is introduced, establishing how deadlocks can be studied in terms of circular waits. Second, we show how a circular wait situation corresponds to a particular marking related to a siphon of the Petri net model. Finally, this last characterization is used to obtain an iterative method that successively forbids deadlock related states, synthesizing the control necessary to ensure a final live behavior. The method can be implemented by means of the solutions of a set of integer linear programming problems.

Banker's-like approaches to deadlock avoidance are based on a decision procedure to grant active processes resources using information about the maximum needs of resources that a process can request in order to ensure termination. The paper presents an extension of the classical Banker's algorithm to a class of flexible manufacturing systems modeled by means of Petri nets. These systems have two interesting characteristics from the application point of view. First, flexible routing of parts is allowed, and second, a multiset of resources is allowed to be used at each processing step. The decision procedure introduced is polynomial in the Petri net model size.

The paper presents two methods for deadlock avoidance in concurrent systems. We apply the proposed approaches to flexible manufacturing systems, modeled by means of Petri nets. Both methods correspond to improvements of the classical Banker's algorithm, and are based on the knowledge of the process structure. The first one is polynomial in the size of the Petri net model. The second one depends strongly on the number of alternative paths for the processing of parts and can be of a non-polynomial cost.

In this paper we research a modeling methodology, applicable to a large class of flexible manufacturing systems (FMS), that takes advantage of the differentiation between the FMS layout and the set of process plans corresponding to the different types of parts to be processed, We propose a separate modeling of these two components. In a second step, both models are integrated automatically in a unique model, represented as a colored Petri net (CPN). The second aim of the paper is the application of a deadlock prevention control policy ensuring that the processing of each part can be completed.

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

In this paper we illustrate a compositional method for modeling the concurrent execution of working processes in flexible manufacturing systems (FMS) through a special class of Petri nets that we call S/sup 3/PR. In essence, this class is built from state machines sharing a set of places modeling the availability of system resources. The analysis of S/sup 3/PR leads us to characterize deadlock situations in terms of a zero marking for some structural objects called siphons. In order to prevent the system from deadlocks, we propose a policy for resource allocation based on the addition of new places to the net imposing restrictions that prevent the presence of unmarked siphons (direct cause of deadlocks). Finally we present the application of this technique to a realistic FMS case.>

A general iterative technique for approximate throughput computation of stochastic strongly connected marked graphs is presented. It generalizes a previous technique based on net decomposition through a single input-single output cut, allowing the split of the model through any cut. The approach has two basic foundations. First, a deep understanding of the qualitative behavior of marked graphs leads to a general decomposition technique. Second, after the decomposition phase, an iterative response time approximation method is applied for the computation of the throughput. Experimental results on several examples generally have an error of less than 3%. The state space is usually reduced by more than one order of magnitude; therefore, the analysis of otherwise intractable systems is possible.>