1 Introduction

Reversibility is a phenomenon referring to the ability of a system to execute its actions in both the forward and the reverse directions. It occurs in a variety of systems (e.g., quantum computation and biochemical systems) and can be exploited in many others (e.g., robotics, manufacturing systems, distributed systems, and logical circuits). Recently, its study has been receiving increased attention. Among the developments, a variety of formal frameworks of modeling reversible systems have been defined, contributing towards an improved understanding of the basic principles of reversibility. A natural next step for this work is the development of techniques for the automatic analysis of reversible models.

In this paper we consider reversing Petri nets (RPNs) [8], a recently-proposed Petri-net framework that allows transitions to be carried out in both the forward and the reverse directions in or out of causal order. Specifically, we present work in progress towards a framework for simulation and analysis of RPN models via an encoding into Answer Set Programming (ASP) [5, 7] a declarative programming framework with competitive solvers that may be used to model a system as well as a query about the system via a logic program, such that models of the program provide the answers to the set query. ASP has proved to be a promising approach towards reasoning about Petri nets with encodings to ASP having been defined for a number of Petri net subclasses, e.g. [1,2,3, 6]. In this paper we provide a systematic way of modelling RPNs and their causal reversibility semantics in ASP. Our long term goal is the development of an ASP-based framework for reasoning about RPN models.

2 Reversing Petri Nets

In this section we briefly recall RPNs and we refer the reader to [8, 9] for the full exposition. Following [9], RPNs are cyclic structures defined as follows:

Definition 1

A reversing Petri net (RPN) is a tuple (A, P, B, T, F) where:

  1. 1.

    A is a finite set of bases or tokens ranged over by a, b, \(\ldots \). We write \(\overline{A} = \{\overline{a}\mid a\in A\}\) and \(\mathcal{{A}}=A \cup \overline{A}\).

  2. 2.

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

  3. 3.

    \(B\subseteq A\times A\) is a set of undirected bonds ranged over by \(\beta \), \(\gamma \), \(\ldots \). We write \(a \!-\!b\) for a bond \((a,b)\in B\), \(\overline{B} = \{\overline{\beta }\mid \beta \in B\}\), and \(\mathcal{{B}}=B \cup \overline{B}\).

  4. 4.

    \(F : (P\times T \cup T \times P)\rightarrow 2^{\mathcal{{A}}\cup \mathcal{{B}}}\) defines a set of directed arcs.

RPNs are built on the basis of a set of bases or tokens each having a unique name. Tokens may occur as stand-alone elements or merge together to form bonds. Places and transitions have the standard meaning. Directed arcs connect places to transitions and vice versa and are labelled by a subset of \(\mathcal{{A}}\cup \mathcal{{B}}\) where \(\overline{A}\) and \(\overline{B}\) are the sets of “negative” tokens and bonds, expressing token and bond absence, respectively. For a label \(\ell = F(x,t)\) or \(\ell = F(t,x)\), we assume that each token a can appear in \(\ell \) at most once, either as a or as \(\overline{a}\), and that if \((a,b)\in \ell \) then \(a,b\in \ell \). Furthermore, for \(\ell = F(t,x)\) it must be that \(\ell \cap (\overline{A}\cup \overline{B}) = \emptyset \). \(F(x,y)= \emptyset \) implies that there is no arc between x and y. Finally, we assume that F is defined so that transitions (1) do not erase tokens, (2) do not destroy bonds, and (3) do not clone tokens/bonds into more than one outgoing place.

We write \(\circ t = \{x\in P\mid F(x,t)\ne \emptyset \}\) and \( t\circ = \{x\in P\mid F(t,x)\ne \emptyset \}\), \(\mathsf {pre}(t) = \bigcup _{x\in P} F(x,t)\) and \(\mathsf {post}(t) = \bigcup _{x\in P} F(t,x)\), and define the effect of a transition as \(\mathsf {eff}(t) = \mathsf {post}(t) - \mathsf {pre}(t)\). Furthermore, we employ the notion of a marking defined as a distribution of tokens and bonds across places, \(M: P\rightarrow 2^{A\cup B}\). In addition, a history assigns a memory to each transition, \(H : T\rightarrow 2^\mathbb {N}\), where \(H(t)=\emptyset \) captures that transition t has not taken place, or it has been reversed, and \(H(t) =\{k_1,\ldots ,k_n\}\) captures that t was executed and not reversed n times where the \(k_i\) indicate the order of the execution instances. A pair \(\langle {M}, {H}\rangle \) describes a state of a RPN. Finally, we write \(\mathsf {con}(a,C)\), where \(a\in C\) and \(C\subseteq A\cup B\), for the connected component of token a in the graph described by C.

We proceed to define forward execution for RPNs.

Definition 2

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

  1. 1.

    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 \(a\in F(t,y_1)\), \(b\in F(t,y_2)\), \(y_1 \ne y_2\), then \(b \not \in \mathsf {con}(a,M(x))\) for all \(x \in \circ t\),

  3. 3.

    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)\).

Definition 3

Given a RPN (A, P, B, T, F), a state \(\langle M, H\rangle \), and a transition t forward enabled in \(\langle {M}, {H}\rangle \), we write \(\langle {M}, {H}\rangle {\mathop {\longrightarrow }\limits ^{t}} \langle {M'}, {H'}\rangle \) where:

$$ \begin{array}{rcl} M'(x) &{} = &{} \left\{ \begin{array}{ll} M(x)-\bigcup \nolimits _{a\in F(x,t)}\mathsf {con}(a,M(x)) &{} \text {if } x\in \circ {t} \\ M(x)\cup F(t,x)\cup \bigcup \nolimits _{ a\in F(t,x)\cap F(y,t)}\mathsf {con}(a,M(y)) &{} \text {if } x\in t\circ \\ M(x), &{}\text {otherwise} \end{array} \right. \end{array} $$
$$ \begin{array}{rcl} H'(t') &{} = &{} \left\{ \begin{array}{lll} H(t')\cup \{ \max ( \{0\} \cup \{k \mid k\in H(t''), t''\in T\}) +1\}, &{} \text {if } t' = t\\ H(t'), &{} \text {otherwise} \end{array} \right. \end{array} $$

Thus, when a transition is executed all tokens and bonds on its incoming arcs are relocated from its input to its output places with their connected components.

According to causal-order reversibility, a transition may be reversed only if all transitions causally dependent on it have either been reversed or not executed:

Definition 4

Consider a RPN (A, P, B, T, F), a state \(\langle {M}, {H}\rangle \), and a transition \(t\in T\). Then t is co-enabled in \(\langle {M}, {H}\rangle \) if \(H(t)\ne \emptyset \) and, for all \(a\in F(t,x)\), if \(a\in M(y)\) for some y and \(\mathsf {con}(a,M(y))\cap \mathsf {pre}(t') \ne \emptyset \) for some \(t'\) then either \(H(t')=\emptyset \) or there is \(k\in H(t)\) such that \(k>k'\) for all \(k\in H(t')\).

When a transition is reversed in a causal fashion, all tokens and bonds in the postcondition of the transition and their connected components are transferred to the incoming places of the transition and any created bonds are broken.

Definition 5

Given a RPN (A, P, B, T, F), a state \(\langle M, H\rangle \), and a transition t co-enabled in \(\langle {M}, {H}\rangle \), we write \(\langle {M}, {H}\rangle {\mathop {\rightsquigarrow }\limits ^{t}}_{c} \langle {M'}, {H'}\rangle \) where

$$ \begin{array}{rcl} M'(x) &{} = &{} \left\{ \begin{array}{ll} M(x)\cup \bigcup \nolimits _{ y \in t\circ , a\in F(x,t)\cap F(t,y)}\mathsf {con}(a,M(y)-\mathsf {eff}(t)), &{} \text {if } x\in \circ {t} \\ M(x)- \bigcup \nolimits _{a\in F(t,x)}\mathsf {con}(a,M(x)) , &{} \text {if } x\in t\circ \\ M(x) &{}\text {otherwise} \end{array} \right. \end{array} $$
$$ { \begin{array}{rcl} H'(t')=\left\{ \begin{array}{lll} H(t')- \{ k \}, \text {if } t' = t,k=\max (H(t))\\ \{k'\mid k'\in H(t'), k'<k \} \cup \{k'-1\mid k'\in H(t'), k'>k \} , \text {otherwise} \end{array} \right. \end{array}} $$
Fig. 1.
figure 1

Causal-order example

Full size image

An example of a reversing Petri net can be seen in Fig. 1 simulating the assembly of a three-component product. A principal process during the re-manufacturing of worn-out or malfunctioning products is disassembly that enables the dumping, cleaning, repair or replacement of components as desired. Therefore, reversible computation can be used as means of modelling the disassembly process while considering the product topology, mating relations, and precedence relations. Here we have three tokens a, b, and c representing the three components of an assembly line. Token d represents the machine required in order to assemble the components into the final product. The system consists of two independent transitions, \(t_2\) and \(t_3\) causally following transition \(t_1\), and transition \(t_4\) causally following \(t_2\). This structure gives the ability to the machine to directly bond component a with c by executing \(t_3\) or to indirectly bond a with c through component b. The ability to reverse every transition in the context of manufacturing task planning, can be used in order to recover from failures during the assembly process. In the figure, we observe the execution of transition sequence \(t_1;t_3;\underline{t_3};t_2;t_4\), demonstrating a causally-ordered reversal of transition \(t_3\) (denoted by \(\underline{t_3}\)) in order to accommodate the manufacturing of a product consisting of \(a\!-\!b \!-\!c\). Note that a non-empty history of transitions is presented as a list over the transitions.

3 Translating RPNs into ASP

Answer Set Programming (ASP) [5, 7] is an extension of logic programming with negation as failure under the stable model or answer set semantics. An Answer Set Program is a set of rules of the form

$$\begin{aligned} A_0 \leftarrow A_1, A_2, \ldots A_m, not\ A_{m+1}, not\ A_{m+2}, \ldots not\ A_n \end{aligned}$$

with the intuitive reading that if all atoms \(A_1, A_2, \ldots , A_m\) are true and none of \(A_{m+1}, A_{m+2}, \ldots , A_n\) is true, then \(A_0\) must be true. Most ASP systems, such as clingo (https://potassco.org/clingo/) that we use for our encoding, extend the basic language with additional constructs such as choice rules of the form \(\{A_0^1,\ldots , A_0^k\} \leftarrow A_1, \ldots , A_m,\) \(not\ A_{m+1}, \ldots not\ A_n\), with the meaning that if the right hand side of the rule holds, then some subset of the atoms \(\{A_0^1, \ldots , A_0^k\}\) must hold true, which introduces a form of non-determinism that is useful when modeling combinatorial problems. ASP systems, such as clingo, couple a highly expressive language that provides constructs from various fields, such as database systems and constraint programming, with powerful solvers. Therefore, these systems can be successfully applied to a large number of application domains and they have shown the potential of solving problems with thousands of variables and hundreds of thousands of rules in seconds or minutes.

In the following we discuss a translation of reversing Petri nets under the causal reversibility semantics into ASP for a simulation length that is encoded by the last argument \(\texttt {TS}\) of the predicates of our model. The basic predicates that represent the input network are \(\texttt {trans(T)}\), \(\texttt {token(Q)}\), and \(\texttt {place(P)}\), that correspond to the transitions, tokens and places, respectively, whereas predicates \(\texttt {ptarc(P,T,Q)}\) declare that \(\texttt {Q} \in F(\texttt {P},\texttt {T})\) (similarly for \(\texttt {tparc(T,P,Q)}\)) and \(\texttt {ptarcbond(P,T,Q1,Q2)}\) refer to bonds, i.e. \(\texttt {Q1-Q2} \in F(\texttt {P},\texttt {T})\). The markings of a RPN are captured by predicates \(\texttt {holds}\) for tokens and \(\texttt {holdsbonds}\) for bonds. That is, \(\texttt {holdsbonds(P,Q1,Q2,TS)}\) means \(\texttt {Q1-Q2} \in M_{TS}(\texttt {P})\), where \(M_{TS}\) refers to the marking at step \(\texttt {TS}\) of the simulation.

In the following we discuss some excerpts of the RPN to ASP translation that has been implemented in the clingo system.

Forward-enableness of Definition 2 is captured via \(\texttt {notenabled(T,TS)}\), which assumes the value true if transition \(\texttt {T}\) cannot be enabled at step \(\texttt {TS}\). Some of the rules for this predicate are depicted in Listing 3.1. The first rule refers to the case \(\texttt {Q} \in F(\texttt {P},\texttt {T)}\) and \(\texttt {Q} \not \in M_{\texttt {TS}}(\texttt {P})\), and the second to the similar case for bonds. The rule in lines 5–6 corresponds to the second item of Definition 2, i.e. \(\texttt {Q1} \in F(\texttt {P1},\texttt {T})\), \(\texttt {Q2} \in F(\texttt {P2},\texttt {T})\) and \(\texttt {Q2} \in \mathsf {con}(\texttt {Q1},M_{\texttt {TS}}(\texttt {P}))\), where predicate \(\texttt {connected}\) defines the set \(\mathsf {con}(a,C)\). The third case of Definition 2 corresponds to the rule in lines 7–9.

If none of the conditions that disable a transition holds, the transition is enabled, as encoded by the rule in line 11. The choice rule of line 12, allows clingo to assign any of the values true or false to atom \(\texttt {fires(T,TS)}\), i.e. choose whether transition \(\texttt {T}\) executes or not.

figure a

Lines 15–22 of Listing 3.1 are the rules for bond addition and deletion that result from forward transition execution. The rule in line 15 says that \(\texttt {Q1-Q2} \in M(\texttt {TP}_{\texttt {TS+1}})\) for \(\texttt {Q1-Q2} \in F(\texttt {T},\texttt {TP})\) if transition \(\texttt {T}\) fires at time \(\texttt {TS}\). The rule in lines 16–18 enforces that \(\texttt {Q1-Q2} \in M(\texttt {TP}_{\texttt {TS+1}})\) for \(\texttt {Q1-Q2} \in M(\texttt {PT}_\texttt {TS})\), \(\texttt {Q1-Q2} \in \mathsf {con}(\texttt {Q},M(\texttt {PT}_{\texttt {TS}})\), \(\texttt {Q} \in F(\texttt {PT},\texttt {T}) \cap F(\texttt {T},\texttt {TP})\), and transition \(\texttt {T}\) that fires at time \(\texttt {TS}\). Lines 20–22 implement bond deletion in a similar way. The encoding also contains rules for token addition and deletion.

Lines 1–9 of Listing 3.2 define predicate \(\texttt {dependent(T2,T1,TS)}\), which is true if the execution of transition \(\texttt {T2}\) depends on the execution of transition \(\texttt {T1}\). The rule in lines 1–4 requires that this is the case if \(max(H(\texttt {T2})) > max(H(\texttt {T1}))\) and there is \(\texttt {Q}\) such that \(\texttt {Q} \in F(\texttt {T1},x)\) and \(\texttt {Q} \in F(y,\texttt {T2})\). The rule in lines 5–9 covers the similar case where \(\texttt {Q} \in F(\texttt {T1},x)\), \(\texttt {Q1} \in F(y,\texttt {T2})\), and \(\texttt {Q1} \in \mathsf {con}(\texttt {Q},M_{TS}(\texttt {P}))\). Lines 11 and 12 encode coenableness, whereas the rule in line 13 encodes the choice of reversing a transition or not.

figure b

The ASP encoding can be used to tackle complex reasoning tasks about RPNs. Consider for instance the network of Fig. 1 and its ASP representation in Listing 3.3. Lines 1–6 define the places, transitions and tokens of the network, whereas lines 8–24 list all arcs (both incoming and outgoing) associated with each transition. For instance, lines 11–14 define all arcs related to transition t2. Finally, line 26 represents the initial marking.

figure c

Then, query

figure d

asks for a reachable state where there is a place \(\texttt {P}\) s.t. \(a-c \in M(\texttt {P})\). The ASP encoding returns the answer fires(t1,0) fires(t3,1). For query

figure e

where a state is sought where some place holds a bond with at least three tokens, clingo finds the solution fires(t1,0) fires(t2,1) fires(t4,2). We can arbitrarily increase the complexity of the analysis, by combining aggregates such as #count in conjunctive or disjunctive queries such as

figure f

where we search for a sequence of transitions that first create a bond with at least three tokens, and then a bond with a and c but without b. The answer computed now is fires(t1,0) fires(t2,1) fires(t4,2) reversesC(t4,3) reversesC(t2,4) fires(t3,5).

4 Conclusions

We have presented work in progress towards a methodology for analysing reversible systems modeled as RPNs based on ASP. We argue that ASP allows an expressive and flexible methodology for defining models and their properties, which can handle difficult queries on complex models efficiently. As future work, we plan to extend our translation to out-of-causal reversibility, to capture a variety of RPN properties, and to apply the framework on realistic systems. We remark that a complementary approach which we are also exploring is the possibility to exploit existing model-checking Petri net tools (CPN tools [10]) for analysing RPN models through a translation of RPNs to coloured Petri nets [4]. CPN tools is a graphical tool for the simulation of Reversing Petri nets. However, it does not pursue more than one simulation and it breaks transition choice ties randomly. Its effectiveness is still to be verified as the approach is characterized by a blow-up in the state space during the translation to coloured Petri nets.