Controlling Reversibility in Reversing Petri Nets with Application to Wireless Communications

TL;DR

This paper introduces a method to control reversibility in Reversing Petri Nets by associating transitions with conditions, demonstrated through a distributed antenna selection algorithm in wireless communications.

Contribution

It presents a novel approach to control transition reversibility in RPNs using conditions, enhancing modeling capabilities for distributed systems.

Findings

Effective control of reversibility in RPNs demonstrated

Application to distributed antenna selection algorithm

Framework supports causal and spontaneous reversals

Abstract

Petri nets are a formalism for modelling and reasoning about the behaviour of distributed systems. Recently, a reversible approach to Petri nets, Reversing Petri Nets (RPN), has been proposed, allowing transitions to be reversed spontaneously in or out of causal order. In this work we propose an approach for controlling the reversal of actions of an RPN, by associating transitions with conditions whose satisfaction/violation allows the execution of transitions in the forward/reversed direction, respectively. We illustrate the framework with a model of a novel, distributed algorithm for antenna selection in distributed antenna arrays.

Equations

$$\begin{array}[]{rcl}M^{\prime}(x)&=&M(x)-\bigcup_{\_}{a\in F(x,t)}\mathsf{con}(a,M(x))\\ &&\cup\bigcup_{\_}{a\in F(t,x),y\in\circ{t}}\mathsf{con}(a,M(y)-\mathsf{pre}(t)\cup F(t,x))\end{array}$$

$$\begin{array}[]{rcl}M^{\prime}(x)&=&M(x)-\bigcup_{\_}{a\in F(t,x)}\mathsf{con}(a,M(x))\\ &&\cup\bigcup_{\_}{y\in t\circ,a\in F(x,t)}\mathsf{con}(a,M(y)-\mathsf{post}(t)\cup F(x,t))\end{array}$$

$$\mathcal{C}=\underset{\_}{\max }\mathbf{P},{\mathbf{H}}_{\_}\mathbf{c}{\log }_{\_}2\det \left(\mathbf{I}+\rho \frac{N_{\_}R}{N_{\_}TS}{\mathbf{H}}_{\_}\mathbf{c}\mathbf{P}{{\mathbf{H}}_{\_}\mathbf{c}}^H\right)$$

Full text

1 Introduction

Reversibility is a phenomenon that occurs in a variety of systems, e.g., biochemical systems and quantum computations. At the same time, it is often a desirable system property. To begin with, technologies based on reversible computation are considered to be the only way to potentially improve the energy efficiency of computers beyond the fundamental Landauer limit. Further applications are encountered in programming languages, concurrent transactions, and fault-tolerant systems, where in case of an error a system should reverse back to a safe state.

As such, reversible computation has been an active topic of research in recent years and its interplay with concurrency is being investigated within a variety of theoretical models of computation. The notion of causally-consistent reversibility was first introduced in the process calculus RCCS [5], advocating that a transition can be undone only if all its effects, if any, have been undone beforehand. Since then the study of reversibility continued in the context of process calculi [6, 14, 9, 12, 4], event structures [17], and Petri nets [3, 13, 2].

A distinguishing feature between the cited approaches is that of controlling reversibility: while various frameworks make no restriction as to when a transition can be reversed (uncontrolled reversibility), it can be argued that some means of controlling the conditions of transition reversal is often useful in practice. For instance, when dealing with fault recovery, reversal should only be triggered when a fault is encountered. Based on this observation, a number of strategies for controlling reversibility have been proposed: [6] introduces the concept of irreversible actions, and [11] introduces compensations to deal with irreversible actions in the context of programming abstractions for distributed systems. Another approach for controlling reversibility is proposed in [15] where an external entity is employed for capturing the order in which transitions can be executed in the forward or the backward direction. In another line of work, [10] defines a roll-back primitive for reversing computation, and in [9] roll-back is extended with the possibility of specifying the alternatives to be taken on resuming the forward execution. Finally, in [1] the authors associate the direction of action reversal with energy parameters capturing environmental conditions of the modelled systems.

In this work we focus on the framework of reversing Petri nets (RPNs) [13], which we extend with a mechanism for controlling reversibility. This control is enforced with the aid of conditions associated with transitions, whose satisfaction/violation acts as a guard for executing the transition in the forward/backward direction, respectively. The conditions are enunciated within a simple logical language expressing properties relating to available tokens. The mechanism may capture environmental conditions, e.g., changes in temperature, or the presence of faults. We present a causal-consistent semantics of the framework. Note that conditional transitions can also be found in existing Petri net models, e.g., in [8], a Petri-net model that associates transitions and arcs with expressions.

We conclude with the model of a novel antenna selection (AS) algorithm which inspired our framework. Centralized AS in DM MIMO (distributed, massive, multiple input, multiple output) systems [7] is computationally complex, demands a large information exchange, and the communication channel between antennas and users changes rapidly. We introduce an RPN-based, distributed, time-evolving solution with reversibility, asynchronous execution and local condition tracking for reliable performance and fault tolerance.

2 Reversing Petri Nets

In this section we extend the reversing Petri nets of [13] by associating transitions with conditions that control their execution and reversal, and allow tokens to carry data values of specific types (clauses (2), (6) and (7) in the following definition). We introduce a causal-consistent semantics for the framework.

Definition 1

A *reversing Petri net *(RPN) is a tuple $(P,T,\Sigma,A,B,F,C,I)$ where:

$P$ is a finite set of places and $T$ is a finite set of transitions. 2. 2.

$\Sigma$ forms a finite set of data types with $V$ the associated set of data values. 3. 3.

$A$ is a finite set of bases or tokens ranged over by $a,b,\ldots$. $\overline{A}=\{\overline{a}\mid a\in A\}$ contains a “negative” instance for each token and we write ${\cal{A}}=A\cup\overline{A}$. 4. 4.

$B\subseteq A\times A$ is a set of undirected bonds ranged over by $\beta,\gamma,\ldots$. We use the notation $a\!-\!b$ for a bond $(a,b)\in B$. $\overline{B}=\{\overline{\beta}\mid\beta\in B\}$ contains a “negative” instance for each bond and we write ${\cal{B}}=B\cup\overline{B}$. 5. 5.

$F:(P\times T\cup T\times P)\rightarrow 2^{{\cal{A}}\cup{\cal{B}}}$ is a set of directed labelled arcs. 6. 6.

$C:T\rightarrow$ COND is a function that assigns a condition to each transition $t$ such that $type(C(t))=Bool$. 7. 7.

$I:A\rightarrow V$ is a function that associates a data value from $V$ to each token $a$ such that $type(I(a))=type(a)$.

RPNs are built on the basis of a set of tokens or bases which correspond to the basic entities that occur in a system. Tokens have a type from the set $\Sigma$, and we write $type(e)$ to denote the type of a token or expression in the language. Values of these types are associated to tokens of an RPN via function $I$. Tokens may occur as stand-alone elements but as computation proceeds they may also merge together to form bonds. Transitions represent events and are associated with conditions COND defined over the data values associated with the tokens of the model and functions/predicates over the associated data types. Places have the standard meaning. Directed arcs connect places to transitions and vice versa and are labelled by a subset of ${\cal{A}}\cup{\cal{B}}$. Intuitively, these labels express the requirements for a transition to fire when placed on arcs incoming the transition, and the effects of the transition when placed on the outgoing arcs. Graphically, a Petri net is a directed bipartite graph where tokens are indicated by $\bullet$, places by circles, transitions by boxes, and bonds by lines between tokens.

The association of tokens to places is called a marking such that $M:P\rightarrow 2^{A\cup B}$ where $a\!-\!b\in M(x)$, for some $x\in P$, implies $a,b\in M(x)$. In addition, we employ the notion of a history, which assigns a memory to each transition $H:T\rightarrow 2^{\mathbb{N}}$. Intuitively, a history of $H(t)=\emptyset$ for some $t\in T$ captures that the transition has not taken place, and a history of $k\in H(t)$, captures that the transition was executed as the $k^{th}$ transition occurrence and it has not been reversed. Note that $|H(t)|>1$ may arise due to cycles in a model. A pair of a marking and a history, $\langle{M},{H}\rangle$, describes a state of a RPN with $\langle{M_{\_}0},{H_{\_}0}\rangle$ the initial state, where $H_{\_}0(t)=\emptyset$ for all $t\in T$.

We introduce the following notations. We write $\circ t=\{x\in P\mid F(x,t)\neq\emptyset\}$ and $t\circ=\{x\in P\mid F(t,x)\neq\emptyset\}$ for the incoming and outgoing places of transition $t$, respectively. Furthermore, we write $\mathsf{pre}(t)=\bigcup_{\_}{x\in P}F(x,t)$ and $\mathsf{post}(t)=\bigcup_{\_}{x\in P}F(t,x)$. Finally, we define $\mathsf{con}(a,C)$, where $a$ is a token and $C\subseteq A\cup B$ a set of connections, to be the tokens connected to $a$ via a sequence of bonds in $B$, together with the bonds creating these connections.

In what follows we assume that: (1) transitions do not erase tokens ($A\cap\mathsf{pre}(t)=A\cap\mathsf{post}(t)$), and (2) tokens/bonds cannot be cloned into more than one outgoing places of a transition ($F(t,x)\cap F(t,y)=\emptyset$ for all $x,y\in P,x\neq y$). Furthermore, we assume for all $a\in A,|\{\!\!|{x|a\in M_{\_}0(x)}|\!\!\}|=1$, i.e., there exists exactly one base of each type in $M_{\_}0$. Note that we extend the exposition of [13] by allowing transitions to break bonds and by permitting cyclic structures.

2.1 Forward execution

For a transition to be forward-enabled in an RPN the following must hold:

Definition 2

Consider a RPN $(P,T,\Sigma,A,B,F,C,I)$, a transition $t$, and a state $\langle{M},{H}\rangle$. We say that $t$ is forward-enabled in $\langle{M},{H}\rangle$ if:

If $a\in F(x,t)$ (resp. $\beta\in F(x,t)$) for some $x\in\circ t$, then $a\in M(x)$ (resp. $\beta\in M(x)$), and if $\overline{a}\in F(x,t)$ (resp. $\overline{\beta}\in F(x,t)$) for some $x\in\circ t$, then $a\not\in M(x)$ (resp. $\beta\not\in M(x)$), 2. 2.

If $\beta\in F(t,x)$ for some $x\in t\circ$ and $\beta\in M(y)$ for some $y\in\circ t$ then $\beta\in F(y,t)$, 3. 3.

$E(C(t))$= True.

Thus, $t$ is enabled in state $\langle{M},{H}\rangle$ if (1) all tokens and bonds required for the transition are available in $t$’s incoming places and none of the tokens/bonds whose absence is required exists in $t$’s incoming place, (2) if a pre-existing bond appears in an outgoing arc of a transition, then it is also a precondition of the transition to fire, and (3) the transition’s condition $C(t)$ evaluates to true. We write $E(c)$ for the value of the condition based on the assignment function $I$.

When a transition $t$ is executed in the forward direction, all tokens and bonds occurring in its outgoing arcs are relocated from the input to the output places along with their connected components. The history of $t$ is extended accordingly:

Definition 3

Given a RPN $(P,T,\Sigma,A,B,F,C,I)$, a state $\langle M,H\rangle$, and a transition $t$ enabled in $\langle{M},{H}\rangle$, we write $\langle{M},{H}\rangle\stackrel{{\scriptstyle t}}{{\longrightarrow}}\langle{M^{\prime}},{H^{\prime}}\rangle$ where:

[TABLE]

and $H^{\prime}(t^{\prime})=H(t^{\prime})\cup\{\max(\{0\}\cup\bigcup_{\_}{t^{\prime\prime}\in T}H(t^{\prime\prime}))+1\},$ if $t^{\prime}=t$, and $H(t^{\prime})$, otherwise.

2.2 Causal order reversing

We now move on to causal-order reversibility. The following definition enunciates that a transition $t$ is $co$-enabled (‘$co$’ standing for causal-order reversing) if it has been previously executed and all the tokens on the outgoing arcs of the transition are available in its outplaces. Furthermore, to handle causality in the presence of cycles, clause (1) additionally requires that all bonds involved in the connected components of such tokens have been constructed by transitions $t^{\prime}$ that have preceded $t$. Furthermore, clause (2) of the definition requires that the condition of the transition is not satisfied.

Definition 4

Consider a RPN $(P,T,\Sigma,A,B,F,C,I)$, a state $\langle{M},{H}\rangle$, and a transition $t\in T$ with $k=\max(H(t))$. Then $t$ is $co$-enabled in $\langle{M},{H}\rangle$ if: (1) for all $a\in F(t,y)$ then $a\in M(y)$, and if $\mathsf{con}(a,M(y))\cap\mathsf{post}(t^{\prime})\neq\emptyset$ for some $t^{\prime}\in T$ with $k^{\prime}\in H(t^{\prime})$, then $k^{\prime}\leq k$, and, (2) $E(C(t))$= False.

When a transition $t$ is reversed all tokens and bonds in the pre-conditions of $t$, as well as their connected components, are transferred to $t$’s incoming places.

Definition 5

Given a RPN a state $\langle M,H\rangle$, and a transition $t$ $co$-enabled in $\langle{M},{H}\rangle$ with history $k\in H(t)$, we write $\langle{M},{H}\rangle\stackrel{{\scriptstyle t}}{{\rightsquigarrow}}\langle{M^{\prime}},{H^{\prime}}\rangle$ where:

[TABLE]

and $H^{\prime}(t^{\prime})=H(t^{\prime})-\{k\}$ if $t^{\prime}=t$, and $H(t^{\prime})$, otherwise.

3 Case Study: Antenna Selection in DM MIMO

The search for a suitable set of antennas is a sum capacity maximization problem:

[TABLE]

where $\rho$ is the signal to noise ratio, $N_{\_}{TS}$ the number of antennas selected from a total of $N_{\_}T$ antennas, $N_{\_}{R}$ the number of users, $\mathbf{I}$ the $N_{\_}{TS}\times N_{\_}{TS}$ identity matrix, $\mathbf{P}$ a diagonal $N_{\_}{R}\times N_{\_}{R}$ power matrix. $\mathbf{H_{\_}{c}}$ is the $N_{\_}{TS}\times N_{\_}{R}$ submatrix of $N_{\_}{T}\times N_{\_}{R}$ channel matrix $\mathbf{H}$ [7]. Instead of centralized AS, in our approach (1) is calculated locally for small sets of antennas (neighborhoods), switching on only antennas which improve the capacity: in Fig. 1(a), antenna $A_{\_}{i-1}$ will not be selected.

In the RPN interpretation, we present the antennas by places $A_{\_}1,\ldots,A_{\_}n$, where $n=N_{\_}T$, and the overlapping neighbourhoods by places $M_{\_}1,\ldots,M_{\_}h$. These places are connected together via transitions $t_{\_}{i,j}$, connecting $A_{\_}i$, $A_{\_}j$ and $M_{\_}k$, whenever there is a connection link between antennas $A_{\_}i$ and $A_{\_}j$. The transition captures that, based on the neighbourhood knowledge in place $M_{\_}k$, antenna $A_{\_}i$ may be preferred over $A_{\_}j$ or vice versa (the transition may be reversed).

To implement the intended mechanism, we employ three types of tokens. First, we have the power tokens $p_{\_}1,\ldots,p_{\_}l$, where $l$ is the number of enabled antennas. If token $p$ is located on place $A_{\_}i$, antenna $A_{\_}i$ is considered to be on. Transfer of these tokens results into new antenna selections, ideally converging to a locally optimal solution. Second, tokens $m_{\_}1,\ldots,m_{\_}h$, each represent one neighborhood. Finally, $a_{\_}1,\ldots,a_{\_}n$, represent the antennas. The tokens are used as follows: Given transition $t_{\_}{i,j}$ between antenna places $A_{\_}i$ and $A_{\_}j$ in neighbourhood $M_{\_}k$, transition $t_{\_}{i,j}$ is enabled if token $p$ is available on $A_{\_}i$, token $a_{\_}j$ on $A_{\_}j$, and bond $(a_{\_}i,m_{\_}k)$ on $M_{\_}k$, i.e., $F(A_{\_}i,t_{\_}{i,j})=\{p\}$, $F(A_{\_}j,t_{\_}{i,j})=\{a_{\_}j\}$, and $F(M_{\_}k,t_{\_}{i,j})=\{(a_{\_}i,m_{\_}k)\}$. This configuration captures that antennas $A_{\_}i$ and $A_{\_}j$ are on and off, respectively. (Note that the bonds between token $m_{\_}k$ and tokens of type $a$ in $M_{\_}k$ capture the active antennas in the neighbourhood.) Then, the effect of the transition is to break the bond $(a_{\_}i,m_{\_}k)$, and release token $a_{\_}i$ to place $A_{\_}i$, transferring the power token to $A_{\_}j$, and creating the bond $(a_{\_}j,m_{\_}k)$ on $M_{\_}k$, i.e., $F(t_{\_}{i,j},A_{\_}i)=\{a_{\_}i\}$, $F(t_{\_}{i,j},A_{\_}j)=\{p\}$, and $F(t_{\_}{i,j},M_{\_}k)=\{(a_{\_}j,m_{\_}k)\}$. The mechanism achieving this for two antennas can be seen in Fig. 1(b).

Finally, to capture the transition’s condition, an antenna token $a_{\_}i$ is associated with data vector $I(a_{\_}i)=\mathbf{h}_{\_}i$, $type(\mathbf{h}_{\_}i)=\mathbb{R}^{2}$ ($=\mathbb{C}$), i.e., the corresponding row of $\mathbf{H}$. The condition constructs the matrix $\mathbf{H}_{\_}c$ of (1) by collecting the data vectors $\mathbf{h}_{\_}i$ associated with the antenna tokens $a_{\_}i$ in place $M_{\_}k$: $\mathbf{H}_{\_}c=(\mathbf{h}_{\_}1,...,\mathbf{h}_{\_}n)^{T}$ where $\mathbf{h}_{\_}i=I(a_{\_}i)$ if $a_{\_}i\in M_{\_}k$, otherwise $\mathbf{h}_{\_}i=(0\;\ldots\;0)$. The transition $t_{\_}{i,j}$ will occur if the sum capacity calculated for all currently active antennas (including $a_{\_}i$), $\mathcal{C}_{\_}{a_{\_}i}$, is less than the sum capacity calculated for the same neighbourhood with the antenna $A_{\_}i$ replaced by $A_{\_}j$, $\mathcal{C}_{\_}{a_{\_}j}$, i.e., $\mathcal{C}_{\_}{a_{\_}i}<\mathcal{C}_{\_}{a_{\_}{j}}$. Note that if the condition is violated, the transition may be executed in the reverse direction.

Results of the RPN-based approach on an array consisting of $64$ antennas serving $16$ users, varying the number of selected antennas from $16$ to $64$ are shown in Fig. 2 [16]. If we run five RPN models in parallel and select the one with the best performance for the final selection, the results are consistently superior to those of a centralised (greedy) algorithm, and if we run just one (equivalent to the average of the performance of these five models) the results are on par with those of the centralised algorithm.

4 Conclusions

We have extended RPNs with conditions that control reversibility by determining the direction of transition execution, and we have applied our framework to model an AS algorithm. Preliminary results show superior performance to centralised approaches. Our experience strongly suggests that resource management can be studied and understood in terms of RPNs as, along with their visual nature, they offer a number of relevant features. In subsequent work, we plan to extend RPNs for allowing multiple tokens of the same base/type to occur in a model and for developing out-of-causal-order reversibility semantics in the presence of conditional transitions as well as the destruction of bonds.

Acknowledgents: This work was partially supported by the European COST Action IC 1405: Reversible Computation - Extending Horizons of Computing, Science Foundation Ireland (SFI) and European Regional Development Fund under Grant Number 13/RC/2077, and the EU Horizon 2020 research & innovation programme under the Marie Sklodowska-Curie grant agreement No 713567.