A Quotient-Graph for the Analysis of Reflective Petri Nets

Abstract

The design of dynamic, adaptable discrete-event systems calls for adequate modeling formalisms and tools in order to manage possible changes occurring during system’s lifecycle. A common approach is to pollute the design with details not concerning the current system behavior, rather its evolution. That hampers analysis, reuse and maintenance in general. A Petri net-based reflective model (based on classical Petri nets) was recently proposed to support dynamic discrete-event system’s design, and was applied to dynamic workflow’s management. Behind there is the idea that keeping functional aspects separated from evolutionary ones, and applying evolution to the (current) system only when necessary, results in a clean formal model for dynamic systems. This model preserves the ability of verifying properties typical of classical Petri nets. As a first step toward the implementation (in the short time) of a discrete-event simulator, Reflective Petri nets are provided in this paper with a semantics defined in terms of labeled state-transitions.

19.1 Introduction

Most existing discrete-event systems are subject to evolution during their lifecycle. Think e.g. of mobile ad-hoc networks, adaptable software, business processes, and so on. Designing dynamic/adaptable discrete-event systems calls for adequate modeling formalisms and tools. Unfortunately, the known well-established formalisms for discrete-event systems, such as classical Petri nets [13], lack features for naturally expressing possible run-time changes to system’s structure. An approach commonly followed consists of polluting system’s functional aspects with details concerning evolution. That practice hampers system analysis, reuse and maintenance.

Reflective Petri nets [5] have been recently proposed as design framework for dynamic discrete-event systems, and successfully applied to dynamic workflows [4]. They rely on a reflective layout formed by two logical levels. The achieved clean separation between functional and evolutionary concerns results in a simple formal model for systems exhibiting a high dynamism, which should preserve the analysis capabilities of classical Petri nets. With respect to other dynamic extensions of Petri nets appeared in last decade, which set up new (hybrid) paradigms [2, 3, 9, 12], the Reflective Petri nets approach tries to achieve a satisfactory compromise between expressive power and analysis capability, through a rigorous application of reflection concepts in a consolidated Petri net framework.

On the perspective of implementing in the short time an automatic solver and a discrete-event simulation engine, Reflective Petri nets are provided in this paper with a (labeled) state-transition semantics. Any analysis/simulation techniques based on state-space inspection has to face a crucial question, that is how to recognize possible equivalent states during base-level’s evolution. That major topic is managed by exploiting the symbolic state definition the particular Colored Petri net flavor [11] used for the meta-level is provided with, and represents the paper’s original contribution.

The balance is as follows: background information on Reflective Petri nets and the employed Petri net formalisms are given in Sections 19.2 and 19.3. The focus is put there on those elements directly connected to the paper’s main contribution, the definition of a state-transition semantics for Reflective Petri nets (Section 19.4). An application of the semantics to a dynamic system taken from literature is summarized in Section 19.5. Related works are mentioned and discussed in Section 19.6. Finally Section 19.7 is about work-in-progress.

19.2 WN’s Basic Notions

The formalisms employed for the two levels (meta- and base-) of the reflective layout are Well-formed Nets (WN) [6], a flavor of Colored Petri nets (CPN) [11], and their unfolded counterpart, an extension of ordinary Place/Transition nets [13], respectively. This choice has revealed convenient for two main reasons: first, the behavior of Reflective Petri nets can be formally stated in terms of classical Petri nets state-transition; secondly, the symbolic state notion peculiar of WN makes it possible to efficiently recognize equivalent base-level’s evolutions.

While retaining CPN’s expressive power, WNs are characterized by a structured syntax, exploited by efficient analysis algorithms.This section does not present all the features of WNs, for which the reader can refer to [6], just introduces them informally, focusing on the symbolic marking definition. Unlike CPNs, WNs include priority levels for transition and inhibitor arcs. These features enhance the formalism expressiveness and are helpful to represent the transactional execution of evolutionary strategies.

As in CPN, places as well as transitions are associated to color domains, i.e., tokens in places have an identifier (color), similarly transitions are parameterized, so that there exist different color instances of a given transition. A marking M maps every place p to a multiset on the respective color domain C(p). The projection of M to a subset P′ is denoted M[P′]. Any arc connecting p to a transition t is labeled by a function mapping every element of C(t) to a multiset on C(p).

SWN color domains are Cartesian products of basic color classesC _i. A class C _i may be in turn partitioned into static subclassesC _i,k. The idea is that objects in a subclass are indistinguishable from one another.

19.2.1 The Symbolic Marking

The Symbolic Marking [7] provides syntactical equivalence relation on ordinary WN markings: two markings belong to the same SM if and only if they can be obtained from one another by means of a permutation of colors that preserve static subclasses. A SM (denoted $\widehat{\bf M}$) is formally expressed in terms of dynamic subclasses, and specifies the distribution of symbolic colors (tuples built of dynamic subclasses) over the WN places.

Dynamic subclasses define a parametric partition of color classes preserving the static partition: let Z _i and s _i denote the set of dynamic subclass of C _i (in $\widehat{\bf M}$), and the number of static subclasses of C _i (s _i ≥ 1). The j-th dynamic subclass of C _i, z _j ⁱ ∈ Z _i, refers to a static subclass, denoted d(z _j ⁱ), 1 ≤ d(z _j ⁱ) ≤ s _i, and has a cardinality | z _j ⁱ |, i.e., it represents a parametric set of colors. It must hold, ∀k : 1... s _i

The SM canonical form [7], based on a lexicographic ordering and a minimization of dynamic subclass distribution over the places, provides a way to uniquely represent an SM.

19.3 Reflective Petri Nets Layout

The Reflective Petri nets [5] approach relies on a logical layout divided in two levels. The first one, called base-level, is an ordinary Petri net (a P/T net with priorities and inhibitor arcs) representing the system prone to evolve (base-level PN); while the second level, called meta-level, consists of a high-level Petri net (a colored Petri net) representing the evolutionary strategies (the meta-program, following the reflection parlance) that drive the evolution of the base-level upon occurrence of certain conditions/events.

The meta-level acts on a representative of the base-level, called reification, which is formalized by a colored marking. The reification is used by the meta-program to observe (introspection) and manipulate (intercession) the base-level PN. Changes to the reification are reflected down to the base-level at the end of a meta-computation (shift-down).

The meta-level is implicitly activated (shift-up) at any base-level change of state. Then a strategy is selected depending on whether (a) the base-level has entered a given condition, (b) and/or any external events (simulated at meta-level) have occurred. The ability of specifying arbitrary selection conditions enhances the flexibility of the reflective layout.

The reflective framework is another high-level Petri net component, somehow similar to a transparent meta-layer, which is in charge of implementing base-level’s introspection and intercession. The framework has a fixed layout, formed by higher-priority transitions. Intercession is performed in terms of a minimal, complete set of low-level operations (the evolutionary interface): addition/removal of nodes and arcs, change of transition priorities (structural changes), free moving of tokens overall the base-level PN places (state changes). If one such operation fails, the meta-program as a whole is restarted and any changes caused in the meanwhile to the reification are discarded. Trying to delete a yet not existing node is an example of failure In other words, the evolutionary strategies have a transactional semantics. After a strategy’s succeeding run, changes are reflected down to the base-level Petri net.

A designer is provided with a tiny ad-hoc language, originally inspired to Hoare’s CSP, to specify his/her own strategy in a simple way, without any skills in high-level Petri net being required. An automatic translation to a corresponding high-level Petri net is done.

Several strategies could be candidate for execution at a given instant: different policies might be adopted to select one, varying from a non deterministic choice, to a static assignment of priorities. According to the reflective paradigm, the base-level is unaware of the meta-program. The system designer may freely decide, using priority, to block the base-level while the meta-program is active, or to leave it running. It may also define local influence areas for some strategies, by (temporarily) locking corresponding portions of the base-level.

Let us only outline here some essential points about the interaction between base- and meta-levels:

• 1. The reflective framework and the meta-program share two sets of boundary colored places, denoted reification set and evolutionary interface in the sequel. Their composition, through a simple superposition of shared places, gives rise to the meta-model, called meta-level PN.

• 2. The reification is a well-defined marking of the reification set Reif formed by reifP, reifT, reifA, reifΠ, reifM. Such places encode structure (nodes, connections, and priorities) and current state of the base-level PN, respectively. Their color domains are built of basic classes Place, Tran, which are (logically) unbounded repositories holding all potential base-level nodes (they must contain the nodes of the initial base-level Petri net). We have: C(reifP), C(reifM): Place; C(reifT), C(reifΠ): Tran; C(reifA): Place ×Tran ×{ i, o, h}.

• 3. The isomorphism between base-level nets and reification is formalized by a bijection φ. For example a net formed by places {p ₁, p ₂, …}, transitions {t ₁, t ₂, …} having priority levels 0, 1, … respectively, by an input arc (p ₁, t ₁) of weight 2, an output arc (t ₁, p ₂) of weight 1.., whose current marking is m(p ₁) = 2, m(p ₂) = 1, is reified as: $\mathbf{M}(\text{ reifP}) = {p}_{1} + {p}_{2} + \ldots \,$, $\mathbf{M}(\text{ reifT}) = {t}_{1} + {t}_{2} + \ldots$, $\mathbf{M}(\text{ reif}\Pi ) = {t}_{2} + \ldots$, $\mathbf{M}(\text{ reifA}) = 2 \cdot \langle {p}_{1},{t}_{1},i\rangle +\langle {p}_{1},{t}_{2},o\rangle + \ldots$, $\mathbf{M}(\text{ reifM}) = 2 \cdot {p}_{1} + {p}_{2}$.

• 4. A back-up copy Reif _back of set Reif is kept. Evolutionary strategies work on Reif: if an operation fails, then the contents of Reif _back are copied back to Reif, and the control passes to the base-level.

• 5. The shift-up is implemented in transparent way at net-level, by connecting every base-level transition to the place(s) reifM (reifM _back ) by means of colored arcs. The resulting model is denoted base-meta PN. Consider transition t ₁ of the above example: its firing makes two colors p ₁ and one color p ₂ be withdrawn/ added from/to reifM (reifM _back ), respectively. Base-level changes of state are thus instantaneously mirrored on the reification, maintaining base-level’s unawareness of the meta-level.

• 6. The shift-down is emulated by a homonym highest-priority meta-transition of the meta-level PN.

19.4 State-Transition Semantics for Reflective Nets

The causal connection between base- and meta-level makes it possible to formalize the behavior of Reflective Petri nets in terms of WN state-transitions:

Definition 19.1 (Reflective Petri net state).

A state of a Reflective Petri net is a marking M _i of the base-meta PN.

Let PN ₀ be the (marked) base-level Petri net which models the initial system. Assume it has been connected to the meta-level. The initial state of the corresponding Reflective Petri net is obtained setting: M ₀[Reif] = M ₀[Reif _back ] = φ(PN ₀).

Let t _c be any transition (color instance) of the base-meta PN, other than shiftdown. If t _c is enabled in M _i, according to the ordinary enabling rule, and M _j is the marking reached upon the firing, we have the state-transition:

$\begin{array}{rcl}{ \mathbf{M}}_{\mathrm{i}}\stackrel{{t}_{\mathrm{c}}}{ \rightarrow }{\mathbf{M}}_{\mathrm{j}}& & \\ \end{array}$

Only one case must be treated apart. Let { shift-down be enabled in M _i, according to the ordinary firing rule. Then:

$\begin{array}{rcl}{ \mathbf{M}}_{\mathrm{i}}\stackrel{\mathit{shift}-\mathit{down}}{\rightarrow }{\mathbf{M}^\prime}_{0},& & \\ \end{array}$

M ′ ₀ being the marking of the base-meta PN obtained by firing shift-down in the ordinary way, making the contents of Reif _back be updated to Reif, finally (side-effect), replacing the current base-level PN with PN′= φ^{− 1}(M _i[Reif]) and connecting PN′ to the meta-level.

19.4.1 Handling Equivalent Evolutions

The just introduced state-transition semantics defines precisely the untimed behavior of a reflective Petri net, but suffers from two evident drawbacks affecting efficiency and effectiveness. First, the notion of state is exceedingly redundant, comprising a part, the meta-level, which outs the functional specification of a system. Secondly, there is no way of recognizing whether the system dynamics/evolution leads to equivalent conditions. The latter question is critical: the ability of deciding about finiteness and strongly-connectedness (strictly related to the ability of recognizing equivalences) is in fact mandatory for any techniques based on state-space inspection.

Recognizing equivalences in an evolving system is tricky. It may happen that after a series of transformations the base-level comes back to the original condition (state). Even more likely, the internal dynamics of the evolving system might lead to equivalent conditions. The problem is tackled by resorting to the symbolic marking notion, peculiar of WN, and the base-level reification at the meta-level.

The modeler, on his/her needs may define a logical partition of classes Place, Tran, possibly different from the completely split partition (implicitly) adopted when setting up the base-meta PN:

$\mathit{Place} = {P}_{1} \cup {P}_{2} \cup \ldots {P}_{\mathrm{k}}\quad \mathit{Tran} = {T}_{1} \cup {T}_{2} \cup \ldots {T}_{\mathrm{n}}$

The idea is simple: elements belonging to a subclasses P _i (T _j) denote indistinguishable base-level nodes, which might be freely permuted, without altering the model’s semantics. Those nodes that, for any reasons, must preserve their identity during evolution, will correspond to cardinality one subclasses. The default logical partition is that in which all places/transitions can be permuted. Of course the evolutionary strategies refer to the logical partition of base-level nodes.

The causal connection between base- and meta- levels establishes an exact correspondence (at any instant) between the current base-level PN and the contents of Reif _back . On the light of that, we state the following state-equivalence notion, in which we refer to the logical partition of Place and Tran.

Definition 19.2 (state equivalence).

Let $\widehat{\bf M}$ _i be the symbolic marking obtained from M _i[Reif _back ] replacing every p _i ∈ P _k (t _j ∈ T _l) with a corresponding dynamic subclass z _i ¹ (z _j ²), d(z _i ¹) = k (d(z _j ²) = l), | z _i ¹ | ( | z _j ² | ) = 1. Then M _i ≡ M _j if and only if $\widehat{\bf M}$ _i ≡ $\widehat{\bf M}$ _j.

$\widehat{\bf M}$ _i represents an equivalence class of states (Def.19.1), so we shall use the notation M ∈ $\widehat{\bf M}$ _i. The state-transition notion is redefined accordingly.

Definition 19.3 (visible state-transition).

Let σ be a finite sequence of meta-level transition color instances other than shiftdown (σ possibly empty). Then if and only if t is either shiftdown or a base-level transition, and there exist σ, M _i ′ s.t. M _i $\mathop{\longrightarrow}\limits^\alpha$ M _i ′ $\mathop{\longrightarrow}\limits^t$ →M _j (according to the above definition).

M _i ′, as well as any intermediate marking crossed by σ, are equivalent to M _i. Visible state-transitions are caused by the occurrence of either shiftdown, or any base-level transition. Meta-level transition sequences (σ) are not visible to an external observer.

We call reachable a state M _i such that M ₀ $\mathop{\longrightarrow}\limits^{t_1}$ M ₁ $\mathop{\longrightarrow}\limits^{t_2}$ … M _i. We say $\widehat{\bf M}$ _i reachable if and only if any M ∈ $\widehat{\bf M}$ _i is.

Lemma 19.4.

Let t ∈ T _k, M _i $\mathop{\longrightarrow}\limits^t$ M _j . Then:

∀ M ∈$\widehat{\bf M}$ _i ∃t′∈ T _k, M′∈$\widehat{\bf M}$ _j M $\mathop{\longrightarrow}\limits^{t^\prime}$ M′

∀ M′∈$\widehat{\bf M}$ _j ∃t′∈ T _k, M ∈$\widehat{\bf M}$ _i M $\mathop{\longrightarrow}\limits^{t^\prime}$ M′

Thanks to the above lemma we can build a quotient-graph in which nodes are the reachable {$\widehat{\bf M}$ _i}, and there is a labeled arc $\widehat{\bf M}$ _i $\mathop{\longrightarrow}\limits^{T_k}$ $\widehat{\bf M}$ _j if and only if there exist t ∈ T _k, M ∈ $\widehat{\bf M}$ _i, M ′ ∈ $\widehat{\bf M}$ _j, s.t. M $\mathop{\longrightarrow}\limits^t$ →M ′.

If the meta-level PN never enters a deadlock or a livelock, then the liveness and reachability properties of the original state-transition graph are preserved.

19.5 The Dynamic Philosophers Example

The (symbolic) state-transition semantics of Reflective Petri nets has been tested on a variant of the well known dining philosophers problem which introduces a high dynamism [14]. The version here considered meets the following requirements:

• Two philosophers initially sit on the table.

• A philosopher can eat only when he/she simultaneously picks up the pair of adjacent forks, one of which is owned by the philosopher.

• A philosopher sitting on the table has two additional faculties, both requiring that the owned fork is currently available.

  • He/she can invite a colleague which is outside to join the table, sharing with him/her the owned fork.

  • He/she can leave the table, if there are at least three philosophers sited on it.

• Each philosopher is going around with his/her own fork.

The base-level Petri net representing the starting condition is depicted in Fig. 19.1. We observe that the functional aspects are described in detail, while the dynamic features are only sketched (transitions invite _i, leave _i), thus keeping the model as simple as possible. Any invitation/leaving intents activate the meta-program, which consequently implements two different strategies.

Fig. 19.1

Dynamic philosopher’s base-level Petri net

The logical partition of base-level nodes groups places/transition playing a similar role:

$\mathit{Place} = \mathit{Ph} \cup \mathit{Fork} \cup \mathit{Lv} \cup \mathit{Inv} \cup \ldots \quad \mathit{Tran} = \mathit{Invite} \cup \mathit{Think} \cup \mathit{Leave} \cup \ldots $

where Ph = { ph _i}, Fork = { fk _i}, Lv = { lv _i},..Think = { th _i}, etc.

According to Def.19.2 the depicted base-level net, and that having the same structure, but places eat ₁, ph ₂ marked instead of eat ₂, ph ₁, are equivalent (reachable) states of the corresponding Reflective Petri net. They can be obtained from one another by the permutation:

$\{\,{\mathit{ph}}_{1} \leftrightarrow {\mathit{ph}}_{2},{\mathit{eat}}_{1} \leftrightarrow {\mathit{eat}}_{2}\}$

The leaving strategy is informally described in Table 19.1. The strategy is divided into an introspection step, which consists of checking a logical condition on the base-level reification, followed, if the check is positive, by an intercession phase. Symbols used in the description correspond to typed variables of the strategy specification language, which are bound from time to time to color instances.

An evidence of the effectiveness of the quotient graph based on the equivalent states notion (Def. 19.2), which comes to be live, versus the ordinary state-transition graph, is given in Table 19.2. Only visible changes of state involving the base-level are numbered. The experiment was conducted using the GreatSPN tool, with a script emulating the shift-down effect. The first column reports the problem size, i.e., the table capacity. We can appreciate a sensible reduction of the number of reached states also for small sizes, due to the high symmetry exhibited by the system during evolution. Some data about time/memory saving, not reported for the lack of space, confirm the effectiveness of the approach.

Table 19.1 Leaving strategy description

Table 19.2 Symbolic vs. ordinary state-space size

19.6 Related Works

Many efforts have been devoted in trying to extend Petri nets with dynamical features. In [15], the author is proposing his pioneering work, self-modifying nets, in which the flow relation between a place and a transition is a linear function of the place marking. Another major contribution of Valk is the so-called nets-within-nets paradigm [16], where tokens flowing through a net are in turn nets. In his work, Valk takes an object as a token in a unary elementary Petri net system, whereas the object itself is an elementary net system. Even if in the original Valk’s proposal no dynamic changes are possible, and mobility is weakly supported, most extensions introduced afterward rely upon his idea.

Badouel and Oliver [2] defined a class of high level Petri nets, called reconfigurable nets, which can dynamically modify their own structure by rewriting some of their components. Reconfigurable nets can be unfolded to a subclass of self-modifying Petri nets for which boundedness can be decided. Mobile and dynamic Petri nets [1] integrate Petri nets with RCHAM (Reflective Chemical Abstract Machine) based process algebra.

Tokens in self-modifying, mobile/dynamic and reconfigurable nets, are passive. To bridge the gap between tokens and active objects (agents) some variations on the theme of nets-within-nets have been proposed. In [9] objects are studied as high-level net tokens having an individual dynamical behavior. Object nets behave like tokens, i.e., they are lying in places and are moved by transitions. However, they may also change their state. Reference nets [12] are a flavor of high level Petri nets which provides dynamic creation of net instances, references to other nets/tokens, and communication via synchronous channels (net-inscriptions are in Java).

More recent proposals have some similarity with the work we are presenting. In [3], a dynamic architecture modeling is presented which allows active elements to be nested in arbitrary and dynamically changeable hierarchies, enabling the design of systems at different levels of abstractions, by using refinements of net models. In [10], the paradigm of nets and rules as tokens is introduced, which permit the structure and behavior of P/T systems to be changed. The new concept is implemented using algebraic nets and graph transformations.

Most dynamic extensions of Petri nets set up new (hybrid) paradigms. While the expressive power has increased, the cognitive simplicity of Petri nets has decreased as well. As argued in [2], the intricacy of these proposals leaves little hope to obtain significant mathematical results and/or automated verification tools in a close future. The Reflective Petri nets approach is different, because it tries to achieve a satisfactory compromise between expressive power and analysis capability, through a rigorous application of reflection concepts in a consolidated high-level Petri Net framework.

19.7 Conclusions and Future Work

We have semi-formally introduced a state-transition semantics for reflective Petri nets, a formal layout based on classical Petri nets (Well formed Nets, and their unfolded counterpart) well suited to model adaptable/reconfigurable discrete-event systems. In particular, we have addressed a major topic related to recognizing equivalent system’s evolutions, through the WN’s symbolic state notion. We are planning to integrate the GreatSPN tool [8], that natively supports WN and their stochastic extension, SWN, with new modules for the graphical editing and the analysis/simulation of reflective Petri net models. For that purpose we are defining a stochastic process for Reflective Petri nets, in large part inspired to the SWN (GSPN) timed semantics.