Modern distributed systems are becoming pervasive and increasingly provided with adaptation, (self-)reconfiguration and mobility capability. On one side, to face the challenges of the highly dynamic environments where they are deployed. On the other side, to keep production/maintenance costs down. Therein lies the increasing demand for formal models encompassing all of these aspects (besides concurrency). Hardly any of the classical formalisms like Petri Nets, Automata, and Process Algebra, even though powerful, permits designers to easily specify dynamic structural changes to systems and evaluate their impact on system behaviour. That has led to several extensions of classical formal models (e.g., the Pi calculus or the Nets-within-Nets paradigm) rarely accompanied by suitable analysis techniques. A recent formalization of a class of Rewritable Place-Transition Nets (RwPT) in Maude has proved potentially convenient to specify dynamically reconfigurable systems. Concerning analogous proposals, the RwPT formalism provides more abstraction/flexibility in modelling and efficiency in analysis. Nevertheless, its ability to scale the size of distributed systems built of several similar (nested) components is limited. This paper presents a compositional approach to define large RwPT models in a typical algebraic way and to exploit the modular structure of models during the analysis: Symmetries are implicitly captured by composite node-labelling (reflecting the model's hierarchical structure) that is preserved by net rewrites. A distributed, gracefully degrading production system is used as a case study. Experimental evidence points out the dramatic impact of the approach against a non-modular one and the advantages over alternative techniques. Even if the emphasis is on state-space-based verification, the paper shows the convenience of combining it with structural analysis, which is typical of Petri nets as well. For that purpose, rewrite-rule abstractions are given in the form of guidelines.

In this paper we study the complexity of the reachability problem HORNETS, an algebraic extension of object nets. Here we consider the restricted class of safe, elementary HORNETS. In previous work we established the lower bound, i.e. reachability requires at least exponential space. In another wor k we have shown we can simulate elementary HORNETS with elementary object nets EOS, where reachability is known to be PSpace-complete. Since this simulation leads to a double exponential increase in the size of the simulating EOS, we obtain that for HORNETS the reachability problem is solvable in double exponential space. In this contribution we show that this kind of simulation is rather bad, since we show that exponential space is sufficient. Together with the known lower bound this shows that the upper is tight.

Elementary object systems (EOS for short) are Petri nets in which tokens may be Petri nets again. Originally proposed by Valk for a two levelled structure, the formalism was later generalised for arbitrary nesting structures. However, even if restricted to a nesting depth of two, EOS are Turing-complete and thus many problems like reachability and liveness are undecidable for them. Nonetheless, since they are useful to model many practical applications a natural question is how to restrict the formalism in such a way, that the resulting restricted formalism is still helpful in a modelling context, but so that important verification problems like reachability become quickly decidable. In the last years several structural and dynamic restrictions for EOS have therefore been investigated. These investigations have been central to the first author's recent PhD thesis and have been published in past editions of this journal and on conferences. In this paper we add several new results and present them together with the old in a unified fashion highlighting the central message of these investigations.

In this paper we study the complexity of HORNETS, an algebraic extension of object nets. We define a restricted class: safe, elementary HORNETS, to guarantee finite state spaces. It will turn out, that the reachability problem for this class requires exponential space, which is a major increase when compared to safe, elementary object nets, which require polynomial space.

This contribution presents recent results on Elementary Object Systems (EOS). Object nets are Petri nets which have Petri nets as tokens – an approach known as the nets-within-nets paradigm. In this work we study the relationship of EOS to existing Petri net formalisms. It turns out that EOS are equivalent to counter programs. But even for the restricted subclass of conservative EOS reachability and liveness are undecidable problems. On the other hand for other properties like boundedness are still decidable for conservative EOS. We also study the sub-class of generalised state machines, which is worth mentioning since it combines decidability of many theoretically interesting properties with a quite rich practical modelling expressiveness.

In this paper we develop a negotiation and contracting framework for inter-organisational workflows. The overall aim is to compute a group-plan from a given set of individual plans, where plans are formulated in the context of a given inter-organisat

This contribution presents decidability results for the formalism of Elementary Object Systems (EOS). Object nets are Petri nets which have Petri nets as tokens – an approach known as the nets-within-nets paradigm. In this paper we study the relationship of the reachability and the liveness problem. We prove that both problems are undecidable for EOS (even for the subclass of conservative EOS) while it is well known that both are decidable for classical p/t nets. Despite these undecidability results, boundedness can be decided for conservative EOS using a monotonicity argument similar to that for p/t nets.

In this paper we study the complexity of the liveness problem for safe Elementary Object Nets (EOS). Object nets are Petri nets which have Petri nets as tokens. They are called elementary if the net system has a two levelled structure. The concept of

In this paper we discuss the concept of safeness for Elementary Object Nets (EOS). Object nets are Petri nets which have Petri nets as tokens – an approach known as the nets-within-nets paradigm. Object nets are called elementary if the net system has a two levelled structure. The well known p/t nets can be considered as a special case of EOS. For p/t nets the concept of safeness means that there is at most one token on each place. Since object nets have nested markings there are different possibilities to generalise this idea for EOS. In this paper we define different variants of EOS safeness, discuss their relationships, show that they all coincide for p/t-like EOS, and address the complexity of well known Petri net problems like reachability and liveness for this new class of object nets.

In this work we present object net systems, i.e. Petri nets with nets as token objects, which are equipped with channels that allow to transfer net-tokens in the vertical dimension of the nested marking. These channels are a modelling element powerful enough to describe a direct simulation of counter programs which shows that typical net problems like boundedness, coverability, and reachability are undecidable.