Catálogo de publicaciones - libros

Well-formed Nets (WN) structural analysis techniques allow to study interesting system properties without requiring the state space generation. In order to avoid the net unfolding, which would reduce significantly the effectiveness of the analysis, a symbolic calculus allowing to directly work on the WN colour structure is needed. The algorithms for high level Petri nets structural analysis most often require a common subset of operators on symbols annotating the net elements, in particular the arc functions. These operators are the function difference, the function transpose and the function composition. This paper focuses on the first two, it introduces a language to denote structural relations in WN and proves that it is actually closed under the difference and transpose.

Abstract interpretation is a paradigm that has been successfully used in the verification and optimization of programs. This paper presents a new approach for the analysis of Petri Nets based on abstract interpretation. The main contribution is the capability of deriving non-structural invariants that can increase the accuracy of structural methods in calculating approximations of the reachability space. This new approach is illustrated with the verification of two examples from the literature.

Regulatory networks are at the core of all biological functions from bio-chemical pathways to gene regulation and cell communication processes. Because of the complexity of the interweaving retroactions, the overall behavior is difficult to grasp and the development of formal methods is needed in order to confront the supposed properties of the biological system to the model. We revisit here the tremendous work of R. Thomas and show that its binary and also its multi-valued approach can be expressed in a unified way with high-level Petri nets. A compact modeling of genetic networks is proposed in which the tokens represent gene’s expression levels and their dynamical behavior depends on a certain number of biological parameters. This allows us to take advantage of techniques and tools in the field of high-level Petri nets. A developed prototype allows a biologist to verify systematically the coherence of the system under various hypotheses. These hypotheses are translated into temporal logic formulae and the model-checking techniques are used to retain only the models whose behavior is coherent with the biological knowledge.

The Transmission Control Protocol (TCP) is the most widely used transport protocol in the Internet, providing a reliable data transfer service to many applications. This paper analyses TCP’s Connection Management procedures for correct termination and absence of deadlocks. The protocol is assumed to be operating over a reordering lossless channel and is modelled using Coloured Petri nets. The following connection management scenarios are examined using state space analysis: client-server and simultaneous opening; orderly release; and abortion. The results demonstrate that TCP terminates correctly for client-server and simultaneous connection establishment, orderly release after the connection is established and aborting of connections. However, we discover a deadlock when connection release is initiated before the connection has been fully established when operating over a reordering lossless channel.

We study concurrent processes modelled as workflow Petri nets extended with resource constraints. We define a behavioural correctness criterion called soundness : given a sufficient initial number of resources, all cases in the net are guaranteed to terminate successfully, no matter which schedule is used. We give a necessary and sufficient condition for soundness and an algorithm that checks it.

High-Level net models following the paradigm “nets as tokens” have been studied already in the literature with several interesting applications. In this paper we propose the new paradigm “nets and rules as tokens”, where in addition to nets as tokens also rules as tokens are considered. The rules can be used to change the net structure. This leads to the new concept of high-level net and rule systems, which allows to integrate the token game with rule-based transformations of P/T-systems. The new concept is based on algebraic high-level nets and on the main ideas of graph transformation systems. We introduce the new concept with the case study “House of Philosophers”, a dynamic extension of the well-known dining philosophers. In the main part we present a basic theory for rule-based transformations of P/T-systems and for high-level nets with nets and rules as tokens leading to the concept of high-level net and rule systems.

In this paper we present a polynomial algorithm to decide whether a scenario (given as a Labelled Partial Order) is executable in a given place/transition Petri net while preserving at least the given amount of concurrency (adding no causality). In the positive case the algorithm computes a process net that respects the concurrency formulated by the scenario. We moreover present a polynomial algorithm to decide whether the amount of concurrency given by a Labelled Partial Order is maximal, i.e. whether the Labelled Partial Order precisely matches a process net w.r.t. causality and concurrency of the events, if this process net represents a minimal causality of events among all process nets.

The concept of mobile agents imposes a great security risk for information systems. In this paper we propose object nets as a specification formalism for multi-agent systems. Since the general formalism is Turing-powerful not every analysis method that is common for Petri net can be applied. So, we define the subclass of “ordinary” object nets that allows for the application of standard P/T-net techniques, i.e. the computation of boundedness, liveness etc.

In the framework of the study and analysis of new flight procedures, we propose a new Petri net-based formalism to represent both continuous and discrete evolutions and uncertainties: the particle Petri net . This model is based on a particle filtering-like representation of the probabilistic uncertainty on the continuous part of the procedure, and a possibilistic Petri net-inspired approach to deal with the uncertainty on events. After introducing this formalism, we propose an analysis of an approach procedure, and a further application to the on-line tracking of pilots’ activities.

High-level Petri nets are frequently represented as Petri net schemas , with places, transitions and arcs inscribed by terms . A concrete system is then gained by interpreting the symbols in those terms. The behavior of a concrete system is a transition system . The composition of all those transition systems represents the behavior of the Petri net schema. This paper characterizes the expressive power of (a basic class of) Petri net schemas. It turns out that quite simple as well as quite general requirements at a transition system suffice to generate it by such a Petri net schema.