A method for the computation of (a regular expression for) the language of a safe net is presented. This method is based on net reductions as introduced by Berthelot, and it uses the net's trace language to rebuild the possible interleavings which can get lost during the reduction process. A set of reduction rules preserving the net language is proposed, i. e. in each reduction step, information about the net language is memorized. The result is a regular expression that may be used to decide properties of the net as e. g. mutual exclusion of transitions or possible markings of places.

In this paper an extension of SDL by real-time assertions is suggested. A denotational compositional semantics in terms of timed high level Petri nets is given. This semantics allows to reason about timed SDL-specifications by simulation of the underlying high level nets as well as by unfolding these into timed low level nets and then applying analysis methods for timed Petri nets or temporal model checking. The approach is embedded in the MOBY-tool.

In this paper a high-level Petri net model called M-nets (for multilabeled nets) is developed. A distinctive feature of this model is that it allows not only vertical unfolding, as do most other high-level net models, but also horizontal composition — in particular, synchronisation — in a manner similar to process algebras such as CCS. This turns the set of M-nets into a domain whose composition operations satisfy various algebraic properties. The operations are shown to be consistent with unfolding in the sense that the unfolding of a composite high-level net is the composition of the unfoldings of its components. A companion paper shows how this algebra can be used to define the semantics of a concurrent programming language compositionally.

We discuss some differences between p-generic and strongly p-generic sets. While the class of p-generic sets has measure 1, the class of strongly p-generic sets has measure 0 in an appropriate measure space. Also contrasting the situation with the p-generic sets, for no oracle A, NP(A) contains a strongly p-generic set. Moreover, the notion of np-genericity is introduced and strong p-genericity is shown to be even stronger than np-genericity.

The notion of polynomial superfaimess, which is an extension of strong fairness, is introduced for Petri nets. Superfair sequences automatically have a lot of properties which are not implied by strong fairness. Nevertheless — under reasonable circumstances — almost all infinite occurrence sequences are superfair and there are recursive — in fact exponential — such sequences. The concept of superfaimess is compared to other fairness notions. Possible extensions are suggested.

We introduce the notion of a p-generic set. P-generic sets automatically have all properties which can be enforced by usual diagonalizations over polynomial time computable sets and functions. We prove that there are recursive — in fact exponential time computable — p-generic sets. The existence of p-generic sets in NP is shown to be oracle dependent, even under the assumption that P ≠ NP.

With the introduction of UML 2.0, many improvements to diagrams have been incorporated into the language. Some of the major changes were applied to sequence diagrams, which were enhanced with most of the concepts from ITU-T's Message Sequence Charts, and more. In this paper, we introduce a formal semantics for most concepts of sequence diagrams by means of Petri nets as a formal model. Thus, we are able to express the partially ordered and concurrent behaviour of the diagrams natively within the model. Moreover, the use of coloured high-level Petri nets allows a comprehensive and efficient structure for data types and control elements. The proposed semantics is defined compositionally, based on basic Petri net composition operations.

We aim at comparing various timed extensions of a fully compositional class of high-level Petri nets, called M-nets. On one hand, as a classical approach, a class of timed M-nets is considered, where intervals of duration are attached to each transition. More precisely, we study this class enriched by the recently introduced hierarchical operation of timed refinement. On the other hand, M-nets enriched by the causal time concept (H. Klaudel et al., 1999); Franck Pommereau, 2002) are considered, they are called causal time M-nets and allow us to introduce timing constraints without extending the original untimed model of M-nets. Causal time M-nets are shown to form the more powerful class. It covers timed and even hierarchical timed M-nets. Moreover, as shown by some significant examples, it permits the modelling of systems involving overlapping timing constraints. Some special cases are quoted where hierarchical timed M-nets may become favorite.

The paper aims at defining hierarchical time extensions of M-nets, a fully compositional class of high-level Petri nets. As a starting point, the class of classical timed M-nets are considered, where time intervals of duration are attached to each transition. This class is enriched by two new operations: timed refinement (which extends the class) and hierarchical scoping (which is shown to be a powerful feature for abstraction). It is argued that hierarchical timed M-nets permit the design of real-time systems in a top down manner. Moreover, a partial order semantics of hierarchical timed M-nets is defined based on branching processes. The definition is given directly for high level nets, without preliminary unfolding to low level nets. This semantics enables partial order model checking of hierarchical timed M-nets e.g. within the PEP-system.

Recently, model checking of Petri nets based on partial order semantics w.r.t. temporal logic formulae has been extended to time Petri nets. In this paper, we present an improved algorithm for computing the McMillan-unfolding of a time Petri net which gives a finite representation of the partial order semantics and some experimental results of its implementation within the PEP tool.

Model checking of place/transition-nets based on partial order semantics has been applied successfully to the analysis of causal behaviour of distributed systems. Here, this approach is extended to the causal behaviour of time Petri nets. Expansion of a time Petri net to an equivalent P/T-net is defined, and it is shown that (an abstraction of) the McMillan unfolding of the expanded net is sufficient for model checking w.r.t. formulae of a simple branching time temporal logic L.

In this paper a compositional high-level Petri net semantics for SDL (Specification and Description Language) is presented. Emphasis is laid on the modelling of dynamic creation and termination of processes and of procedures-features, which are, for instance, essential for typical client-server systems. In a preliminary paper we have already shown that we are able to use 'state of the art' verification techniques by basing our approach on M-nets (an algebra of high-level Petri nets). Therefore, this paper concentrates on the details of the semantics. A distinctive feature of the presented solution is that the 'infinite case' (infinitely many concurrent process and procedure instances as well as unbounded capacities of input queues and channels) is covered.

A new method for proving qualitative properties of SDL (Specification and Description Language) systems is presented which is based on a compositional high-level Petri net semantics for SDL. Since emphasis is laid on the modelling of dynamic creation and termination of processes and procedures, our method is especially interesting for typical client-server systems. By using M-nets as the semantic model, we are able to use `state-of-the-art' verification techniques. For instance, the verification component of the PEP (Programming Environment based on Petri nets) tool may be applied, which presently includes partial order-based model checking and algorithms based on linear programming as well as interfaces to other verification packages such as INA (Integrated Net Analyzer), SMV and SPIN, providing reduction algorithms based on BDDs, on the stubborn set or sleep set method, and on symmetries. We show the benefits of our method, applying it to a typical client-server system. After describing how safety, liveness and progress properties can be checked fully automatically, we give examples how the compositional nature of the M-net semantics can be used to solve the `state explosion' problem, and how interactive verification may extend the verification possibilities

Verification of parallel programs is a very important goal on the way to improve thereliability of software. The PEP tool, a Programming Environment based on Petrinets, allows verification of parallel programs by partial order model checking based ona compositional denotational Petri net semantics.The language supported by the PEP tool covers block structuring, parallel andsequential composition, choice, iteration, synchronous and asynchronous communication,including use of unbounded...

Verification of parallel programs is a very important goal on the way to improve the reliability of software. The PEP tool, a programming environment based on Petri nets, allows verification of parallel programs by a variety of different verification methods (e.g., partial order or BDD based model checking, and stubborn set or symmetrically reduced state space analysis) based on a compositional denotational Petri net semantics. The main contribution of this paper consists in the development of a fully compositional high-level Petri net semantics for concurrent programs with procedures, covering recursion, global variables, and different types of parameter passing (including call-by-reference). The semantics (which is already implemented) is oriented towards verification, i.e., the semantic models are minimised. Due to the abstract and flexible nature of the Petri net model used, our approach is very general and may also be applied to other specification and programming languages. We are, for instance, presently approaching SDL (Specification and Description Language)

In this paper a new approach to the veriication of SDL-speciications is presented. The key idea of the method consists of associating a com-positional Petri net semantics to SDL-speciications. A temporal logic is deened which allows the formulation of relevant properties of SDL-speciications. The model checking problem for SDL-speciications according to this logic is then reduced to the model checking problem of Petri nets and an appropriate temporal logic. This approach has been implemented in the MOBY-tool.

Verification of parallel programs is a very important goal on the way to improve the reliability of software. The PEP tool, a Programming Environment based on Petri nets, allows verification of parallel programs by partial order model checking based on a compositional denotational Petri net semantics. The language supported by the PEP tool covers block structuring, parallel and sequential composition, choice, iteration, synchronous and asynchronous communication, including use of unbounded...

Using a class of high level Petri nets, M-nets, endowed with composition operators resembling those of CCS, we give the compositional semantics of B(PN)2 - a syntactically simple but semantically powerful concur-rent programming language. We also give an associated low level net semantics and show the consistency of these high and low level semantics, as well as consistency with a previously defined low level semantics of B(PN)2.