final.tex

% This is samplepaper.tex, a sample chapter demonstrating the
% LLNCS macro package for Springer Computer Science proceedings;
% Version 2.20 of 2017/10/04
%
\documentclass[runningheads]{llncs}
%
\usepackage{graphicx}
\usepackage{amsmath}
%\usepackage{psfrag}
\usepackage{url}
\usepackage{rotating}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{subfigure}

\usepackage{xcolor}
\newcommand\anna[1]{\textcolor{red}{#1}}

% Used for displaying a sample figure. If possible, figure files should
% be included in EPS format.
%
% If you use the hyperref package, please uncomment the following line
% to display URLs in blue roman font according to Springer's eBook style:
% \renewcommand\UrlFont{\color{blue}\rmfamily}
\newcommand{\Bsep}{\: \mid \: }
\newcommand{\Rule}[2]{\displaystyle{\frac{#1}{#2}}}
\newcommand{\SF}[1]{\mathsf{#1}}
\newcommand{\Act}{\mathsf{Act}}
\newcommand{\Vis}{\mathsf{Vis}}
\newcommand{\ActK}{\mathsf{ActK}}
\newcommand{\Proc}{\mathsf{Proc}}
\newcommand{\Var}{\mathsf{Var}}
\newcommand{\Procc}{\mathsf{ProcC}}
\newcommand{\Pred}{\mathsf{Pred}}
\newcommand{\Std}{\mathsf{Std}}
\newcommand{\rms}{\mathrm{S}}
\newcommand{\rmrec}{\mathrm{rec}}
\newcommand{\rmreck}{\mathrm{reck}}
\newcommand{\rmreckR}{\mathrm{reckR}}
\newcommand{\rma}{\mathrm{A}}
\newcommand{\rmp}{\mathrm{P}}
\newcommand{\rmf}{\mathrm{F}}
\newcommand{\rmr}{\mathrm{R}}
\newcommand{\rmfr}{\mathrm{FR}}
\newcommand{\equivS}{\equiv_{\mathrm{S}}}
\newcommand{\SigSA}{\Sigma_{\mathrm{SA}}}
\newcommand{\ltran}[1]{\stackrel{#1}{\longrightarrow}}
\newcommand{\tran}[1]{\stackrel{#1}{\rightarrow}}
\newcommand{\Tran}[1]{\stackrel{#1}{\Rightarrow}}
\newcommand{\nottran}[1]{\stackrel{#1}{\not\rightarrow}}
\newcommand{\Rtran}[1]{\stackrel{#1}{\rightsquigarrow}}
\newcommand{\notRtran}[1]{\stackrel{#1}{\not\rightsquigarrow}}
\newcommand{\trans}[1]{\stackrel{#1}{\rightarrow}_{\mathrm{S}}}
\newcommand{\Par}{\mid}
\newcommand{\restrict}[1]{\!\setminus\!#1}
\newcommand{\paral}{\; \vert \;}

\newcommand{\mA}{\mathcal{A}}
\newcommand{\mSA}{\mathcal{SA}}
\newcommand{\mWA}{\mathcal{WA}}
\newcommand{\mAK}{\mathcal{AK}}
\newcommand{\aAK}{\mathcal{(A)K}}
\newcommand{\umAK}{\underline{\mathcal{A}}\mathcal{K}}
\newcommand{\un}[1]{\underline {#1}}
\newcommand{\PI}{\mathcal{PI}}
\newcommand{\rom}[1]{\mbox{\rm{#1}}}

\newcommand{\Nil}{\mathbf{0}}
\newcommand{\New}[1]{\nu#1\: }
\newcommand{\Str}{\equiv}
\newcommand{\stdpred}{\mathsf{std}}
\newcommand{\std}[1]{\mathsf{std}(#1)}
%
\newcommand{\Bch}[2]{\mathsf{before}_{#1}(#2)}

\newcommand{\keys}[1]{\mathsf{keys}(#1)}
\newcommand{\kkey}[1]{\mathsf{k}(#1)}
\newcommand{\key}[1]{[#1]}
\newcommand{\Keys}{\mathcal{K}}
\newcommand{\Subscripts}{\mathcal{S}}
\newcommand{\freshpred}[1]{\mathsf{fsh}[#1]}
\newcommand{\fresh}[2]{\mathsf{fsh}[#1](#2)}
\newcommand{\freshsubscript}[2]{\mathsf{fshsubscript}[#1](#2)}
\newcommand{\subscript}[1]{\mathsf{s}(#1)}

\newcommand{\alphaconversionkey}[3]{\mathsf{\alpha keys}(#1,#2,#3)}
\newcommand{\alphaconversionkeyk}[3]{\mathsf{\alpha k}(#1,#2,#3)}
\newcommand{\alphaconversionsub}[3]{\mathsf{\alpha subscripts}(#1,#2,#3)}
\newcommand{\alphaconversionsubs}[3]{\mathsf{\alpha s}(#1,#2,#3)}
\newcommand{\alphaconversionsubsr}[3]{\mathsf{\alpha sr}(#1,#2,#3)}
\newcommand{\alphaconversionsubsc}[3]{\mathsf{\alpha sc}(#1,#2,#3)}

\newcommand{\ta}[1]{\mathsf{ta}(#1)}
\newcommand{\action}[1]{\mathsf{act}(#1)}

\newcommand{\intr}{\mbox{\ $\hat{}$\ }}
%\newcommand{\intr}{\mbox{\; $\widehat{}$\;}}
\newcommand{\sterm}{\mathsf{trm}}
\newcommand{\Sterm}[1]{\sterm(#1)}
\newcommand{\und}[1]{\underline{#1}}
\newcommand{\sqc}{\mathop{\cdot}}
\newcommand{\card}[1]{|#1|}
\newcommand{\bydef}{\stackrel{\emph{def}}{=}}
%
\newcommand{\Angle}[1]{\langle #1 \rangle}
\newcommand{\Tri}{\triangleright}
\newcommand{\Hole}{\bullet}
\newcommand{\rec}[1]{\mathrm{rec}\, #1}
\newcommand{\Rec}[1]{\rec #1 .}
\newcommand{\Rch}{\mathsf{Rch}}
\newcommand{\prune}{\pi}
\newcommand{\Prune}[1]{\prune(#1)}
\newcommand{\Root}[1]{\mathsf{rt}(#1)}
\newcommand{\hole}{\mbox{$[\ ]$}}

\newcommand{\Bis}{\sim}
\newcommand{\Biss}{\Bis_{\mathsf{S}}}
\newcommand{\Bisf}{\Bis_{\mathsf{F}}}
\newcommand{\Bisfr}{\Bis_{\mathsf{FR}}}
%\newcommand{\Bisu}{\Bis_{\Un}}
\newcommand{\Sim}{\mathcal{S}}
\newcommand{\Rem}{\backslash}
\newcommand{\sqeqt}{\sim}
% rules:
% static rule
\newcommand{\one}{\mbox{(I)}}
\newcommand{\onef}{\mbox{(1)}}
\newcommand{\oner}{\mbox{(1R)}}
% choice rule
\newcommand{\two}{\mbox{(II)}}
\newcommand{\twof}{\mbox{(2)}}
\newcommand{\twor}{\mbox{(2R)}}
% choice axiom
\newcommand{\thr}{\mbox{(III)}}
\newcommand{\thrf}{\mbox{(3)}}
\newcommand{\thrr}{\mbox{(3R)}}
\newcommand{\thrpf}{\mbox{(3\,$'$\!)}}
\newcommand{\thrpr}{\mbox{(3\,$'$\!R)}}
%
%
\newcommand{\Draft}[1]{}
\newcommand{\Comment}[1]{}
\newcommand{\Rev}[1]{{#1}^{-1}}
\newcommand{\Stefan}[1]{{\bf S(} #1 {\bf )S}}
\newcommand{\rulename}[1]{\textsf{#1}}

\newcommand{\A}{\mathcal{A}}
\newcommand{\B}{\mathcal{B}}
\newcommand{\N}{\mathbb{N}}
\newcommand{\mN}{\mathcal{N}}
\newcommand{\mM}{\mathcal{M}}
\newcommand{\mP}{\mathcal{P}}
\newcommand{\I}{\mathcal{I}}
\newcommand{\Q}{\mathbb{Q}^+}
\newcommand{\C}{\mathcal{C}}
\newcommand{\R}{\mathbb{R}}
\newcommand{\MolOxy}{\mathit{MolOxy}}
\newcommand{\MolHy}{\mathit{MolHy}}
\newcommand{\Uppaal}{{\scshape Uppaal}\,}

\newcommand{\PN}{reversing Petri net } 
\newcommand{\guard}[1]{\mathsf{pre}(#1)}
\newcommand{\effects}[1]{\mathsf{post}(#1)}
\newcommand{\bond}{\!-\!}
\newcommand{\connected}{\mathsf{con}}
\newcommand{\state}[2]{\langle {#1}, {#2}\rangle}
\newcommand{\rtrans}[1]{\ensuremath{\stackrel{#1}{\rightsquigarrow}}}
\newcommand{\RPN}{\textsc{RPN\ }} 
\newcommand{\type}{\mathit{type}}
\begin{document}
%
\title{Reversibility in Chemical Reactions\thanks{The authors acknowledge partial support 
of COST Action IC1405 on Reversible Computation - Extending Horizons of Computing.}}
%
%\titlerunning{Abbreviated paper title}
% If the paper title is too long for the running head, you can set
% an abbreviated paper title here
%
\author{Stefan Kuhn\orcidID{0000-0002-5990-4157}\inst{1}, Bogdan Aman\orcidID{0000-0001-7649-8181}\inst{2,3}, Gabriel Ciobanu\orcidID{0000-0002-8166-9456}\inst{2,3},  Anna Philippou\orcidID{0000-0002-1665-9913}\inst{4}, Kyriaki Psara\orcidID{0000-0002-6554-7950}\inst{4}, and 
Irek Ulidowski\orcidID{0000-0002-3834-2036}\inst{5}}
%
\authorrunning{S. Kuhn et al.}
% First names are abbreviated in the running head.
% If there are more than two authors, 'et al.' is used.
%
\institute{School of Computer Science and Informatics, De Montfort University, Leicester, UK\\ \email{\scriptsize stefan.kuhn@dmu.ac.uk} \and
Romanian Academy, Institute of Computer Science, Ia\c si, Rom\^ania\\
 \and
A.I.Cuza University, Faculty of Computer Science, Ia\c si, Rom\^ania\\ 
 \email{\scriptsize \{bogdan.aman, gabriel\}@info.uaic.ro }
\and
Department of Computer Science, University of Cyprus, Nicosia, Cyprus \\ \email{\scriptsize \{annap,kpsara01\}@cs.ucy.ac.cy}  \and 
School of Informatics, University of Leicester, Leicester, UK\\ 
\email{\scriptsize irek.ulidowski@leicester.ac.uk} 
}
%
\maketitle              % typeset the header of the contribution
%
\begin{abstract}
In this chapter we give an overview of techniques for the modelling and reasoning 
about reversibility of systems, including out-of-causal-order reversibility, as it 
appears in chemical reactions. We consider the autoprotolysis of water reaction, and model it with the Calculus 
of Covalent Bonding, the Bonding Calculus, and Reversing Petri Nets.
This exercise demonstrates that the formalisms, developed for expressing advanced forms of 
reversibility, are able to model autoprotolysis of water very accurately. Characteristics and 
expressiveness of the three formalisms are discussed and illustrated.

\keywords{ Reversible Computation \and Reaction Modelling
\and Calculus of Covalent Bonding \and Bonding Calculus \and Reversing Petri Nets }
\end{abstract}
%
%
%
\section{Introduction}

Biological reactions, pathways, and reaction networks have been extensively studied in the literature 
using various  techniques,  including  process  calculi and Petri nets.  Initial research was mainly 
focused  on
reaction rates by the modelling and simulating networks of reactions, in order to
analyse or even predict the common paths through the network.  Reversibility
was not considered explicitly.  Later on
reversibility  started  to  be  taken  into  account,  since  it  plays  a  crucial  r\^ole  in
many processes, typically by going back to a previous state in the system. 
Two common types of reversibility 
are backtracking and causally-consistent reversibility~\cite{danos2004ccsr,Irek2007,LaneseMS10}.
%
Backtracking executes exactly the inverse order of the 
forward execution, and causally-consistent reversibility allows undoing effects before causes, 
but not necessarily in the exact inverse order. 
Beyond backtracking and causally-consistent reversibility, there is a more general form of 
reversibility, known as out-of-causal-order reversibility~\cite{Irek2012}, 
which makes it possible to get to states which cannot be reached by forward reactions alone.  Such sequences
of forward and reverse reaction steps are important as they lead to new chemical
structures and new reactions, which would not be possible without out-of-causal-order
reversibility~\cite{Irek2012}. A typical example is a catalytic reaction: a catalyst $C$ enables compounds 
$A$ and $B$ to combine, a combination that would not normally happen or be very unlikely without the presence 
of $C$. Initially, catalyst $C$ binds with $B$ resulting in a compound $BC$. Then $A$ combines with $BC$
creating $ABC$. Finally, with its job done, $C$ breaks away from $ABC$, leaving $A$ and $B$ bonded. 
This sequence of reactions can be written as follows:

$$ A + B + C \rightarrow A+ BC \rightarrow ABC \rightarrow AB + C$$

\noindent
This is a typical example of out-of-causal order reversibility since the bond between $B$ and $C$
is undone before its effect, namely the bond from $A$ to $B$ (which is not undone at all). 
The modelling of such reactions is the focus of this chapter. For further
motivation, formal definitions and more illustrating examples of the various types of reversibility 
we refer the reader to~\cite{danos2004ccsr,Irek2007,LaneseMS10,Irek2012}.

\subsection{Contribution}  This chapter presents and compares three formalisms, the Calculus of Covalent 
Bonding (CCB) \cite{KU16,KUHN201818}, the Bonding Calculus \cite{NaCo18}, and Reversing Petri Nets~\cite{RPNs}, that have been developed during COST Action IC1405. These models are variations of existing formalisms and set out to study reversible computation by allowing systems to reverse at any time leading to previously visited states or even new states without the need of additional forward actions. The contribution of this chapter is a comparative overview of the three formalisms, a discussion of their expressiveness, and a demonstration of their use on a common case study, namely the autoprotolysis of water
reaction.

Our case study was selected to be non-trivial, of manageable size, and to allow us to 
exhibit the crucial features of the formalisms. It is a chemical reaction that involves small molecules,
so it is different from biological reactions that involve proteins and other macromolecules. 
New modelling techniques may be needed in order to capture fully reversible behaviour of biological systems, however,
in this chapter we concentrate on chemical  reactions, a domain that offers
interesting examples of out-of-causal-order reversibility. 

The discussed formalisms enable us to model the intermediate steps of chemical reactions where 
some bonds are only ``helping'' to achieve the overall aim of the reaction:  specifically, they 
are only formed to be
broken before the end of the reactions.  Thus, the allowed level of detail 
makes a more accurate depiction of the reversibility possible, and allows a more thorough understanding of the underlying reaction mechanisms 
compared to higher-level models.


\subsection{Related Work} 
Process calculi, originally designed for the modelling of sequential and 
concurrent computation, have been applied to biochemical and biological systems. The main 
instances  are the $\pi$-calculus \cite{Regev2004}, BioAmbients \cite{RegevBioambients}, the stochastic $\pi$-calculus \cite{PriamiStochasticPi}, beta binders~\cite{betabinders} and bioPEPA \cite{CiocchettaBiopepa}. Another way to model biochemical reactions is with rule-based formalisms such as BIOCHAM \cite{biocham}, the $\kappa$-calculus  \cite{danoscausality}, and the BioNetGen Language (BNGL) \cite{pmid19399430}. 
The formalisms $\kappa$ and BNGL can be used to model interactions between proteins, while this is not
possible in BIOCHAM. BNGL allows the use of molecule sites having the same name, which is not allowed 
in the $\kappa$-calculus.

Most of the formalisms mentioned above do not explicitly represent reversibility. If an action is 
the reverse of another action performed before, there is no explicit knowledge of that in the model. 
Reversibility was added explicitly to process calculi in
RCCS \cite{danos2004ccsr}, CCSK \cite{Irek2007}, and reversible 
$\pi$ \cite{Lanese_controllingreversibility,Lanese_controlled}. CCSK and RCCS are based on the Calculus of Communicating Systems (CCS) \cite{Milner1980}. They extend CCS by keeping track of past actions 
and enabling an undo of those. So a reverse action is the reverse execution of a forward action.
These calculi support backtracking and causally-consistent reversibility. 
Out-of-causal-order reversibility was first addressed in CCSK extended with controller 
processes~\cite{Irek2012}, and in the context of reversible event 
structures~\cite{Irek2013,irekconcur2013,irekNGC2018}. 
CCB~\cite{KUHN201818} allows all types of reversibility in the context of chemical reactions and in
other settings.

Petri nets (PNs)~\cite{PNs} are another formalism that has been widely used to model and reason
about a wide range of applications featuring concurrency and distribution. They are a graphical 
language  associated with 
a rich mathematical theory and supported by a variety of tools. Their use in systems 
biology dates back to~\cite{DBLP:conf/ismb/ReddyML93,DBLP:journals/jsamas/HofestadtH94}.
Since then, they have been employed for
the modelling, analysis, and simulation of 
biochemical reactions in metabolic pathways, gene expression, signal transduction, and neural 
processes~\cite{PNbiology,DBLP:journals/bib/Chaouiya07,DBLP:journals/nc/BaldanCMS10}. 
Indeed, PNs seem to be a natural framework for representing biochemical systems as they constitute a set of interdependent
transitions/reactions which consume 
and produce resources, and are represented graphically in a similar fashion to the systems
in question.
Several specialised Petri net classes, such as qualitative, stochastic, continuous, or
hybrid Petri nets and their coloured counterparts, have been used to describe different biochemical 
systems~\cite{DBLP:journals/jamia/PelegRA05,DBLP:journals/isb/HofestadtT98,DBLP:journals/fuin/Popova-ZeugmannHK05,DBLP:journals/nc/MatsunoNM11,DBLP:journals/isb/VossHK03}.


Even though classical PNs and their extensions have been extensively used to model biochemical systems, 
they cannot directly model reversibility. Specifically, when  modelling reversible reactions in these formalisms
it is required to employ mechanisms involving two distinct transitions,
one for the forward and one for the reverse version of a reaction. This
may result in expanded models and less natural and/or less accurate
models of  reversible behaviour. It is also in contrast to the notion of reversible computation, 
where the intention is not to return to a state via arbitrary execution but to reverse the effect of already executed transitions. 
For this reason, the formalism of reversing Petri nets~\cite{RPNs} has been proposed to allow 
systems to reverse already executed transitions leading to previously visited states 
or even new ones without the need of additional 
forward actions. Reversing Petri nets 
have also been extended with a mechanism for controlling transition
reversal by associating transitions with conditions~\cite{RC19}.


\subsection{Paper organisation} 
In the next section, we introduce the autoprotolysis of water 
reaction, which will be modelled using our three formalisms. This is followed by a section 
introducing the formalisms, their syntax and, informally, their operational semantics. We also 
give three models of the autoprotolysis of water using the formalisms. In Section~\ref{sec:evaluation}, we compare the formalisms and the models of our example reaction, and we also 
briefly discuss software support for the three formalisms. Finally, Section~\ref{sec:conclusion} concludes the paper.

\section{Autoprotolysis of Water}

We consider a chemical reaction that transfers a hydrogen atom between two water molecules. This
reaction is known as the \emph{autoprotolysis of water} and is shown 
in Figure~\ref{fig:autoprotolysis}. There, $O$ indicates an oxygen atom and $H$ a hydrogen atom. The lines indicate bonds. Positive and negative charges on atoms are shown by $\oplus$ and $\ominus$
respectively. The meaning of the curved arrows and the dots will be explained in the next paragraphs.
The reaction is reversible and it takes place at a relatively 
low rate, making pure water slightly conductive. We have chosen this reaction 
as our example reaction, since it is non-trivial but manageable, and has some
interesting aspects to be represented.

\begin{figure}
\vspace{-2ex}\centering
\includegraphics[height=2.5cm]{autoprotolysis_corr3}
\vspace{-2ex}\caption{Autoprotolysis of water.}
\label{fig:autoprotolysis}
\vspace{-2ex}\end{figure}

To model the reaction we need to understand why it takes place and what causes it.
The main reason is that the oxygen in the water molecule is \emph{nucleophilic}, meaning it has the tendency to bond to another atomic nucleus, which would serve as an \emph{electrophile}. This is because oxygen has a high 
electro-negativity, therefore it attracts electrons and has an abundance of electrons around it. The electrons around the atomic nucleus are arranged on electron shells, where only those in the outer shell participate in bonding. Oxygen has four electrons in its outer shell, which are not involved in the initial bonding with hydrogen atoms. These electrons form two \emph{lone pairs} of two electrons each, which can form new bonds (lone pairs are shown in Figure~\ref{fig:autoprotolysis} by pairs of dots). All this makes oxygen nucleophilic: it tends to connect 
to other atomic nuclei by forming bonds from its lone pairs. Since oxygen attracts electrons, the hydrogen atoms in water
have a positive partial charge and oxygen has a negative partial 
charge. 

The reaction starts when an oxygen in one water molecule is attracted by a hydrogen in another 
water molecule due to their opposite charges. This results in a \emph{hydrogen bond}. 
This bond is formed out of 
the electrons of one of the lone pairs of the oxygen. The large curved arrow in Figure~\ref{fig:autoprotolysis} indicates the movements of the electrons. Since a hydrogen atom cannot have more 
than one bond, 
the creation of a new bond is compensated by breaking the existing hydrogen-oxygen bond (indicated by the small curved arrow). When this happens, the two electrons, which formed the original hydrogen-oxygen bond, remain with the oxygen. Since a hydrogen contains %consists of 
one electron and one proton, it is only the proton that is transferred, so the process can be called a proton transfer as well as a hydrogen transfer. The forming of the new bond and the breaking of the old bond are \emph{concerted}, meaning that %namely
they happen together without a stable 
intermediate configuration. As a result we have reached the state where one oxygen atom
has three bonds to hydrogen atoms and is positively charged, represented on the right side of the reaction in %of
 Figure~\ref{fig:autoprotolysis}. This molecule is called \emph{hydronium} and is written as $\mathrm{H_3O^+}$. The other oxygen atom bonds to only one hydrogen and is negatively charged, having an 
electron in surplus. This molecule is called a \emph{hydroxide} and is written as $\mathrm{OH^-}$. 

Note that the reaction is reversible: the oxygen that lost a hydrogen can 
pull back one of the hydrogens from the other molecule, the  $\mathrm{H_3O^+}$ molecule. This is the case since the negatively 
charged oxygen is a strong nucleophile and the hydrogens in the $\mathrm{H_3O^+}$ molecule are 
all positively charged. Thus, any of~the hydrogens 
can be removed, making both oxygens formally uncharged, and restoring the two water 
molecules. In Figure~\ref{fig:autoprotolysis} the curved arrows are given for the reaction going from left to right. Since the reaction is reversible (indicated by the double arrow) there are corresponding
electron movements when going from right to left. These are not given in line with usual conventions, but can be~inferred.

In this simple reaction, the forward and the reverse step consist of two steps each. The breaking of the old and the forming of the new bond occur simultaneously. This means that there is no strict causality of actions, since none of them can be called the cause of the overall reaction. Furthermore, the reverse step can be done with a different atom to the one used during the forward step because each of the molecules are in a sense identical and in practice there does not exist a single ``reverse'' path corresponding to a forward one.%it is difficult to identify a  clear forward and reverse path. 

It should be noted that there are two types of bonding modelled here. Firstly, we have the initial bonds where two atoms contribute an electron each. Secondly, the \emph{dative} or \emph{coordinate bonds} are formed where both electrons come from one atom (an oxygen in this case). Both are \emph{covalent bonds}, and once formed they cannot be distinguished. Specifically, in the oxygen with three bonds all bonds are the same and no distinction can be made. If one of the bonds is broken by a deprotonation (as in the autoprotolysis of water) the two electrons are left behind and they form a lone pair. If the broken bond was not previously formed as a dative bond, the electrons changed their ``r\^ole''. This explains why any proton can be transferred in the reverse reaction and not just the one that was 
involved in the forward path.

\section{Formalisms for Reversible Chemical Reactions}
\subsection{Calculus of Covalent Bonding}
\label{sec:ccb}

In this subsection we introduce the Calculus of Covalent Bonding (CCB) \cite{KUHN201818}, 
concentrating on the new general prefixing operator $(s;b).P$ which, together with a generalised composition operator, produces pairs of \emph{concerted} actions. Then we present a CCB 
model of the autoprotolysis of water.

\subsubsection{Definition of CCB}\label{sec:calculusdef}

We recall the definition of CCB, presenting only the main ideas. More details can be found in 
\cite{KU16,KUHN201818}. First, we introduce some preliminary notions and notations.

Let $\mA$ be the set of (forward) action labels, 
ranged over by $a,b,c,d,e,f$. We partition $\mA$ into the set of \emph{strong actions}, written as
$\mSA$, and the set of \emph{weak actions}, written as $\mWA$. Reverse (or past) action labels are members of
$\underline\mA$, with typical members $\un{a},\un b, \un c,\un d, \un e ,\un f$, and represent 
undoing of actions. The set $\mathcal{P}(\mA \cup \underline\mA)$ is ranged over by $L$.

Let $\Keys$ be an infinite set of {\em communication keys} (or {\em keys} for short)
\cite{Irek2007}, ranged over by $k,l, m,n$. The Cartesian product $\mathcal A \times \Keys$, denoted by $\mAK$,
 represents past actions, which are written as $a[k]$ for $a\in \mA$ and $k\in\Keys$. 
Correspondingly, we have the set $\umAK$ that represents undoing of past actions. We use $\alpha, \beta$ to identify actions which are either from $\mA$ or $\mAK$. It would be 
useful to consider sequences of actions or past actions, namely the elements of $(\mA \cup \mAK)^*$, 
which are ranged over by $s,s'$ and sequences of purely past actions, namely the elements of $\mAK^*$, 
which are ranged over by $t,t'$. The empty sequence is denoted by $\epsilon$. We use the notation ``$\alpha$,$s$'' and
``$s$,$s'$'' to denote a concatenation of elements, which can be strings or single actions.

We shall also use two sets of auxiliary action labels, namely the set $(\mA) =\{ (a)\ \mid a\in\mA\}$, and its product with the set of keys, namely $(\mA)\Keys$. These labels will be used in the auxiliary rules when defining
the semantics of CCB. They denote the execution of a weak action, which makes it possible in the SOS rules to force breaking of a bond for those actions only.

The syntax of CCB is given below where $P$ is a process term:

$$P ::=  S \ \bigm\lvert \ S\bydef P \ \bigm\lvert \ (s;b).P \ \bigm\lvert \ P\lvert Q \ \bigm\lvert \ P\restrict L $$

The set of process identifiers (constants) $\PI$ contains typical elements $S$ and~$T$. 
Each process identifier $S$ has a defining equation $S\bydef P$ where $P$ contains only forward 
actions (and no past actions). There is also a special identifier
 $\Nil$, denoting the deadlocked process, which has no defining equation. For restrictions $L \subseteq \mA$ holds.
 
We have a general prefixing operator
$(s;b).P$, where $s$ is a non-empty sequence of actions or past actions. This operator
extends the prefixing operator in \cite{Irek2012}. The action $b$ is a weak action
and it can be omitted, in which case the prefixing is written as $(s).P$ and is called the
\emph{simple prefix}. The simple prefix (which is still a sequence) is the prefixing operator in \cite{Irek2012}. 
Exactly one of the actions in~$s$ in $(s).P$ may be a weak action from $\mWA$. A weak action in $s$ is only allowed for the simple prefix, in the $(s;b)$ operator b is the only allowed weak action. If~$s$ is a sequence that contains   
a single action, then the action is a strong action and the operator 
is the prefixing operator of CCS \cite{Milner1980}.
We omit trailing $\Nil$s so, for example, $(s).\Nil$ is written as $(s)$. The new feature of the operator $(s;b).P$ is the execution of the weak action $b$, which
can happen only after all the actions in $s$ have taken place. Performing $b$ then forces
undoing one of the past actions in $s$ (by the \rulename{concert} rule in Figure~\ref{fig:csos}). 
If a $(s;b)$ operator is followed by another sequence of actions, where all actions in $s$ have already taken place, then there is a non-deterministic choice of either doing $b$ or progressing 
to the next sequence of actions (see \rulename{act1} and \rulename{act2}).

$P\paral Q$ represents two systems $P$ and $Q$ which can perform actions or reverse actions on
their own, or which can interact with each other according to a communication function
$\gamma$. As in the calculus ACP \cite{ACPBook}, the communication function is a partial function 
$\gamma: \mathcal A \times \mathcal A \rightarrow \mathcal A$ which is commutative and associative. The function
$\gamma$ is used in the operational semantics to define when two processes can interact. Processes 
$P$ and $Q$ in $P\paral Q$ can also perform a pair of concerted actions,
which is the new feature of our calculus.  We also have the ACP-like restriction operator 
$\setminus L$, where $L$ is a set of labels. It prevents actions from taking place and, due to 
the synchronisation algebra used, it also blocks communication. If $\gamma(a,b)=c$ then $a.P$ and $b.Q$
cannot communicate in $(a.P\paral b.Q)\setminus c$.

The set $\Proc$ of \emph{process terms} is ranged over by $P,Q$ and $R$. 
In the setting of CCB these terms are simply called \emph{processes}. We define the semantics of our calculus using SOS rules (Figures~\ref{fig:fsos}--\ref{fig:csos}) and rewrite rules (Figure~\ref{fig:reduction}).

We use some predicates and functions, which are formally defined in \cite{KUHN201818}. Informally, a process $P$ is standard, written $\std{P}$, if it contains no past actions (hence no keys). A key $n$ is fresh in $Q$, written $\freshpred{n}(Q)$, if $Q$ contains no past action with the key $n$. Function $\mathsf{k}$ returns the keys in a sequence of actions, 
whereas $\mathsf{keys}$ returns the keys in a process, and $\mathsf{fn}$ gives the actions of a process 
which could be executed.


\begin{figure}
\vspace{-4ex}\[
\begin{array}{ll}
\rulename{act1}\ 
\Rule
{\std{P} \quad \fresh{k}{s,s'}}
{(s,a,s';b).P \xrightarrow{a[k]}(s,a[k],s';b).P}
\qquad &
\rulename{act2}\
\Rule
{P \xrightarrow{a[k]} P' \quad \fresh{k}{t}}
{(t;b).P \xrightarrow{a[k]} (t;b).P'}
\\[15pt]
\rulename{par}\
\Rule
{P \xrightarrow{a[k]} P'\quad \fresh{k}{Q}}
{P \paral Q \xrightarrow{a[k]} P' \paral Q}
\qquad &
\rulename{com}\
\Rule
{P \xrightarrow{a[k]} P' \quad Q \xrightarrow{d[k]} Q'}
{P \paral Q \xrightarrow{c[k]} P' \paral Q'}
\; (*)
%
\\[15pt]
\rulename{res}\
\Rule
{P \xrightarrow{a[k]} P'}
{P\backslash L \xrightarrow{a[k]} P'\backslash L}
\; a \notin L
\qquad &
\rulename{con}\
\Rule
{P \xrightarrow{a[k]} P'}
{S \xrightarrow{a[k]} P'}
\; S \bydef P
\end{array}
\] 
\vspace{-3ex}\caption[Forward SOS rules for CCB.]{Forward SOS rules for CCB. 
The condition (*) is $\gamma(a,d)=c$, and $b \in \mathcal{WA}$. Recall that $s$ is a sequence 
of actions and past actions and $t$ is a sequence of purely past actions.} \label{fig:fsos}
\vspace{-2ex}\end{figure}


\begin{figure}
\vspace{-2ex}\[
\begin{array}{ll}
\rulename{rev act1}\
\Rule
{\std{P} %\quad \fresh{k}{s,s'}
}
{(s,a[k],s';b).P \xrightarrow{\underline{a}[k]}(s,a,s';b).P}
\quad &
\rulename{rev act2}\
\Rule
{P \xrightarrow{\underline{a}[k]} P' %\quad \fresh{k}{t}
}
{(t;b).P \xrightarrow{\underline{a}[k]} (t;b).P'}
\\[15pt]
\rulename{rev par}\
\Rule
{P \xrightarrow{\underline{a}[k]} P'\quad \fresh{k}{Q}}
{P \paral Q \xrightarrow{\underline{a}[k]} P' \paral Q}
\quad &
\rulename{rev com}\
\Rule
{P \xrightarrow{\underline{a}[k]} P' \quad Q \xrightarrow{\underline{d}[k]} Q'}
{P \paral Q \xrightarrow{\underline{c}[k]} P' \paral Q'}
\; (*)
%
\\[15pt]
\rulename{rev res}\
\Rule
{P \xrightarrow{\underline{a}[k]} P'}
{P\backslash L \xrightarrow{\underline{a}[k]} P'\backslash L}
\; \underline{a} \notin L
\quad &
\rulename{rev con}\
\Rule
{P \xrightarrow{\underline{a}[k]} P'}
{P \xrightarrow{\underline{a}[k]} S}
\; S \bydef P'
\end{array}
\]
\vspace{-4ex}\caption[Reverse SOS rules for CCB.]{Reverse SOS rules for CCB. The condition (*) is $\gamma(a,d)=c$, and $b \in \mathcal{WA}$. %Note that $\beta \in \mA \cup \mAK$.
} 
\label{fig:reversesos}
\vspace{-2ex}\end{figure}

The forward and reverse SOS rules for CCB are given in Figures~\ref{fig:fsos} and \ref{fig:reversesos}. 
Figure \ref{fig:csos} contains the SOS rules that define the new concerted actions transitions. 
The rule \rulename{concert} defines when a pair of concerted actions 
takes place. This enables the linking of forming and breaking of bonds, and therefore a degree 
of control over 
the reversing of actions. The modelling in the next section will give examples of the application. 
Note that the \rulename{concert} rule uses \emph{lookahead}~\cite{Uli92}. Lookahead is a property 
of SOS rules, where a variable appears both on the right hand side and on the left hand side of 
a transition in the premises. for example $P'$ and $Q'$ in \rulename{concert}. 
The rule \rulename{concert par} requires that $k$ is fresh in $Q$,
correspondingly as in \rulename{par}. Moreover, we need to ensure that when we reverse $h$ with the key $l$
in $P$ we do not leave out any actions with the key $l$ in $Q$ which make up a multiaction 
communication with the key $l$. Hence, we also include the premise $\fresh{l}{Q}$ in \rulename{concert par}.
The rule \rulename{concert act} requires, correspondingly as \rulename{act}, that $k$ is fresh in $t$.
Our operational semantics guarantees that if a standard process evolves to $(t;b).P$, for some $P$, and
$P$ reverses an action with the key $l$, then $l$ is fresh in $t$. Hence, we do not include $\fresh{l}{t}$
in the premises of \rulename{concert act}.
%
%
Overall, the transitions in Figures~\ref{fig:fsos}--\ref{fig:csos} are labelled with $a[k] \in \mAK$, or with 
$\underline{c}[l] \in \umAK$, or with concerted actions $(a[k], \underline{c}[l])$.

\begin{figure}
\vspace{-1ex}\[
\begin{array}{l}
\rulename{aux1}\ 
\Rule{\std{P} \quad \fresh{k}{t}}
{(t;b).P \xrightarrow{(b)[k]}(t;b[k]).P}
\qquad
\rulename{aux2}\
\Rule
{P \xrightarrow{(b)[k]} P' \quad \fresh{k}{t}}
{(t;b').P \xrightarrow{(b)[k]} (t;b').P'}
\\[15pt]
\rulename{concert}\ 
\Rule
{P\xrightarrow{(b)[k]}P' \quad P'\xrightarrow{\underline{a}[l]}P'' \qquad Q\xrightarrow{\alpha[k]}Q' 
  \quad Q'\xrightarrow{\underline{d}[l]}Q''
 }
{P \paral Q\xrightarrow{\{e[k],\underline{f}[l]\}} P'' \paral Q''} (*)\\[15pt]
\rulename{concert act}\
\Rule
{P \xrightarrow{\{{a}[k], \underline{h}[l]\}} P' \quad \fresh{k}{t}}
{(t;b).P \xrightarrow{\{{a}[k], \underline{h}[l]\}} (t;b).P'}\\[15pt]
\rulename{concert par}\
\Rule
{P \xrightarrow{\{{a}[k], \underline{h}[l]\}} P'\quad \fresh{k}{Q} \quad \fresh{l}{Q}}
{P \paral Q \xrightarrow{\{{a}[k], \underline{h}[l]\}} P' \paral Q}\\[15pt]
\rulename{concert res}\
\Rule
{P \xrightarrow{\{{a}[k], \underline{h}[l]\}} P'}
{P\backslash L \xrightarrow{\{{a}[k], \underline{h}[l]\}} P'\backslash L} (**)
%
\end{array}
\] 
\vspace{-3ex}\caption[SOS rules for concerted actions in CCB.]{SOS rules for concerted actions in CCB. The condition (*) is 1. $\alpha= c \lor \alpha = (c)$ 
and $\exists c\in \mathcal{A} | \gamma(b,c)=e$, and 2. $\gamma(a,d)=f$. 
The condition (**) is $a, \underline{h}  \notin L \cup (L)$. 
Recall that $t \in \mAK^*$, and $b \in \mathcal{WA}$.} \label{fig:csos}
\end{figure}

\begin{figure}
\vspace{-.5ex}\[
\begin{array}{lll}
\rulename{prom}: & (s,a,s';b[k]).P \Rightarrow (s,a[k],s';b).P & \mbox{ if } a \in \mathcal{SA}, b \in \mathcal{WA} 
\\[5pt]
\rulename{move-r}: & (s,a,s',b[k],s'').P \Rightarrow (s,a[k],s',b,s'').P & \mbox{ if } a \in \mathcal{SA}, b \in \mathcal{WA}
\\[5pt]
\rulename{move-l}: & (s,b[k],s',a,s'').P \Rightarrow (s,b,s',a[k],s'').P & \mbox{ if } a \in \mathcal{SA}, b \in \mathcal{WA}
\end{array}
\] 
\vspace{-3ex}\caption[Reduction rules for CCB.]{New reduction rules for CCB. Sequences $s, s', s''$ are members of $(\mathcal{A} \cup \mathcal{AK})^{*}$.} 
\label{fig:reduction}
\end{figure}

Next, we recall the main new rewrite rules for a reduction relation for CCB in Figure~\ref{fig:reduction}.
All the rules can be found in~\cite{KU16,KUHN201818} but here we only give rules for {\em promotion} 
of actions. These are \rulename{prom}, \rulename{move-r}, and \rulename{move-l} which  
promote weak bonds (here~$b$) to strong bonds (here $a$).
The rule \rulename{prom} applies to the full version of our prefix operator (with the ; construct), and
\rulename{move-r} and \rulename{move-l} apply only to the simple prefix.
These three rules are here to model what happens in chemical systems: a bond on a weak action is 
temporary and as soon as there is a strong action that can accommodate that bond (as the result
of concerted actions) the bond establishes itself on the strong action thus releasing the weak action.
In order to align the use of these three rules to what happens in chemical reactions, we insist
that they are used as soon as they becomes applicable, a formal definition is given in 
\cite{KU16,KUHN201818}.

We shall call henceforth the transitions derived by the forward SOS rules the \emph{forward transitions} 
and, the transitions derived by the reverse SOS rules the \emph{reverse transitions}.
Correspondingly, there are the \emph{concerted (action)} transitions. 

\subsubsection{The autoprotolysis of water in CCB}

When modelling the autoprotolysis of water in CCB, we shall model the hydrogen and oxygen atoms as processes $H$ and $O$ as follows, where 
$h,o$ are actions representing the bonding capabilities of the atoms and $n,p$ 
representing negative and positive charges, respectively. $H'$ and $O'$ are process constants, and
$p$ and $n$ are weak actions.
$$\begin{array}{lllllll}
H & \bydef & (h;p).H' & \quad & O & \bydef & (o,o,n).O'
\end{array}$$

The synchronisation function $\gamma$ is as follows:

$$\begin{array}{lllllllll}
\gamma(h,o) & = & ho \qquad &
\gamma(n,p) & = & np \qquad &
\gamma(n,h) & = & nh
\end{array}$$

Each water molecule is a structure consisting of two hydrogen atoms and one oxygen atom 
which are bonded appropriately. We shall use subscripts to distinguish the individual copies of 
atoms and actions; for example $H_1$ is a specific copy of hydrogen defined by $(h_1;p).H'_1$, 
similarly for $O_1$ defined as $(o_1,o_2,n).O_1'$. The atoms are composed with 
the parallel composition operator ``$\mid$'' using the communication keys
(which are natural numbers) to combine actions into bonds. So a water molecule is modelled
by the following process, where the key $1$ shows that $h_1$ of $H_1$ has bonded with
$o_1$ of $O_1$ (correspondingly for key $2$). The restriction $\setminus\{h_1,h_2,o_1,o_2\} $ ensures that these actions cannot happen on their own, but only together with their partners, forming a bond.
$$ ((h_1[1];p).H'_1 \paral (h_2[2];p).H'_2 \paral (o_1[1],o_2[2],n).O'_1)
  \setminus\{h_1,h_2,o_1,o_2\} $$
The system of two water molecules in Figure~\ref{fig:autoprotolysis} is represented 
by the parallel composition of two water processes, where the restriction $\setminus\{n,p\}$ represses actions $n,p$ from taking place separately
by forcing them to combine into bonds (according to $\gamma$).
%
\begin{flalign*}
&(( (h_1[1];p).H'_1 \paral (h_2[2];p).H'_2 \paral (o_1[1],o_2[2],n).O'_1)\setminus\{h_1,h_2,o_1,o_2\} \paral &&\\
&( (h_3[3];p).H'_3 \paral (h_4[4];p).H'_4  \paral (o_3[3],o_4[4],n).O'_2) \setminus\{h_3,h_4,o_3,o_4\} ) \setminus\{n,p\}&&
\end{flalign*}
%
Following a general principle in process calculi in the style of CCB we can move the restrictions to the outside. The rule used can be written as $(P \paral Q) \setminus L = P \setminus L \paral Q$ if the actions of $L$ are not used in $Q$. Applying this gives us a water molecule modelled as follows:
%
\begin{flalign*}
&( (h_1[1];p).H'_1 \paral (h_2[2];p).H'_2 \paral (o_1[1],o_2[2],n).O'_1) \paral (h_3[3];p).H'_3 \paral &&\\
&(h_4[4];p).H'_4  \paral (o_3[3],o_4[4],n).O'_2) ) \setminus\{h_1,h_2,o_1,o_2\}\setminus\{h_3,h_4,o_3,o_4\}\setminus\{n,p\}&&
\end{flalign*}
%
Note the $\underline{h_i}$, $\underline{o_j}$, and $\underline{n}$ are not restricted:  this allows us to break bonds via concerted actions involving these actions. We will see an example of this shortly.
We now leave out the restrictions to improve readability.

Actions $n$ in $O_1$ and $p$ in $H_3$ combine (we use the new key $5$), representing a transfer of a proton from one atom 
of oxygen ($O_2$ in our model) to another one ($O_1$ in our model). As a hydrogen atom consists of a proton and an electron, and the electron stays in such a transfer, it can either be called a proton transfer or the transfer of a (positively charged) hydrogen atom. We perform the transfer of $H_3$ from $O_2$ to $O_1$. The creation of the bond with key $5$ from $O_1$ to $H_3$ forces a break of the bond with key $3$ (between $h_3$ and
$o_3$) due to the property~of the operator $(s;b).P$ discussed earlier. These two reactions happen 
almost simultaneously so we represent them as a pair of \emph{concerted actions}. 
\begin{flalign*}
& (h_1[1];p).H'_1 \paral (h_2[2];p).H'_2 \paral (o_1[1],o_2[2],n).O'_1 \paral 
(h_3[3];p).H'_3 &&\\
&\paral (h_4[4];p).H'_4  \paral (o_3[3],o_4[4],n).O'_2) &&\\
&\xrightarrow{\{ np[5], \underline{h_{3}o_{3}}[3]\}}&&\\
&( (h_1[1];p).H'_1 \paral (h_2[2];p).H'_2 \paral (o_1[1],o_2[2],n\boldsymbol{[5]}).O'_1 \paral 
(\boldsymbol{h_3};p\boldsymbol{[5]}).H'_3 &&\\
&\paral (h_4[4];p).H'_4  \paral (\boldsymbol{o_3},o_4[4],n).O'_2&&
\end{flalign*}
We have now arrived at the state on the right hand side in Figure~\ref{fig:autoprotolysis}.
There are weak bonds between $n$ and $p$ (denoted by key $5$) and \emph{strong} bonds between $h_i$ and $o_j$ for
all appropriate $i,j$. Since $H_3$ is weakly bonded to $O_1$ and its strong capability 
$h_3$ has become available, the bond $5$ gets promoted to the stronger bond, releasing 
the capability $p$ of $H_3$. We represent this change as a rewrite 
and we obtain the following process:
\begin{flalign*}
&( (h_1[1];p).H'_1 \paral (h_2[2];p).H'_2 \paral (o_1[1],o_2[2],n\boldsymbol{[5]}).O'_1 \paral 
(\boldsymbol{h_3};p\boldsymbol{[5]}).H'_3 &&\\
&\paral (h_4[4];p).H'_4  \paral (\boldsymbol{o_3},o_4[4],n).O'_2 &&\\
&\Rightarrow &&\\
& ( (h_1[1];p).H'_1 \paral (h_2[2];p).H'_2 \paral (o_1[1],o_2[2],n[5]).O'_1) \paral (h_3\boldsymbol{[5]};p).H'_3) &&\\
&\paral (h_4[4];p).H'_4  \paral (o_3,o_4[4],n).O'_2&&
\end{flalign*}
Note that we wrote $h_3$, $o_3$ and the key 5, the actions and keys affected by the promotion,
in bold font to improve readability. We shall do correspondingly below.

Oxygen $O_1$ is still blocked, which represents it being fully bonded (and positively charged).
Oxygen  $O_2$ has a free $n$ capability and can remove any of the hydrogens from $O_1$. 
As a result the process can reverse to its original state.

We show this by again transferring $H_3$. We then execute promotion again:
%
\begin{flalign*}
&(( (h_1[1];p).H'_1 \paral (h_2[2];p).H'_2 \paral (o_1[1],o_2[2],n[5]).O'_1) \paral (h_3[5];p).H'_3) &&\\
&\paral (h_4[4];p).H'_4  \paral (o_3,o_4[4],n).O'_2&&\\
&\xrightarrow{\{ np[3], \underline{nh_{3}}[5]\}}&&\\
&(( (h_1[1];p).H'_1 \paral (h_2[2];p).H'_2 \paral (o_1[1],o_2[2],\boldsymbol{n}).O'_1) \paral (\boldsymbol{h_3};\boldsymbol{p[3]}).H'_3) &&\\
&\paral (h_4[4];p).H'_4  \paral (o_3,o_4[4],\boldsymbol{n[3]}).O'_2\\
&\Rightarrow\\
&(( (h_1[1];p).H'_1 \paral (h_2[2];p).H'_2 \paral (o_1[1],o_2[2],\boldsymbol{n}).O'_1) \paral (\boldsymbol{h_3[3]};\boldsymbol{p}).H'_3) &&\\
&\paral (h_4[4];p).H'_4  \paral (\boldsymbol{o_3[3]},o_4[4],\boldsymbol{n}).O'_2
\end{flalign*}
%
This corresponds to the original process.
Putting back restrictions we obtain 
%
\begin{flalign*}
&( (h_1[1];p).H'_1 \paral (h_2[2];p).H'_2 \paral (o_1[1],o_2[2],n).O'_1 \paral (h_3[3];p).H'_3 &&\\
&\paral (h_4[4];p).H'_4  \paral (o_3[3],o_4[4],n).O'_2) \setminus\{h_1,h_2,o_1,o_2\}\setminus\{h_3,h_4,o_3,o_4\}\setminus\{n,p\}&&
\end{flalign*}
%
and then if we apply the movement of restrictions in reverse we get
\begin{flalign*}
&(( (h_1[1];p).H'_1 \paral (h_2[2];p).H'_2 \paral (o_1[1],o_2[2],n).O'_1)\setminus\{h_1,h_2,o_1,o_2\} \paral &&\\
&( (h_3[3];p).H'_3 \paral (h_4[4];p).H'_4  \paral (o_3[3],o_4[4],n).O'_2) \setminus\{h_3,h_4,o_3,o_4\} ) \setminus\{n,p\}&&
\end{flalign*}


\subsection{Bonding Calculus}

In this subsection we recall briefly the Bonding Calculus \cite{NaCo18}, and 
illustrate its expressiveness by modelling the autoprotolysis of water. 

\subsubsection{Definition of the Bonding Calculus}

The abstraction ``processes as interactions'' from process calculi is used in the Bonding Calculus, but processes are not able to communicate values in order to interact. Just like in the BNGL \cite{pmid19399430}, the Bonding Calculus allows the use of molecule sites having the same name, while this is not possible in the $\kappa$-calculus. While the $\kappa$-calculus describes molecules as a set of sites and uses rules to manipulate these sites between two or more molecules, in the  Bonding Calculus a molecule is described by the sequence of operations it can perform on its sites (including also non-deterministic choices), regardless of the form of the other molecules. This allows to use the compositionality of the process calculus.

The syntax of the Bonding Calculus syntax is presented in Figure~\ref{table:syntax}. 
Let us consider the set~$\mathbb{N}$ of natural numbers, the set 
$\mN=\{x,x^+,x^-,\dots\}$ of bond names, the set $\mM=\{a,b,\dots\}$ of 
molecules and the set $\mP=\{P,Q,\ldots\}$ of processes. A multiset over 
$\mN$ is defined as a partial function $N:\mN \rightarrow \N$. In the Bonding 
Calculus each molecule has a unique name, and the bond $x$ between two 
molecules $a$ and $b$ is denoted by $\{a-^x b\}$.

\begin{figure}
\vspace{-2ex}\centering
\bgroup
\def\arraystretch{1.3}
\begin{tabular}{c@{\hspace{2ex}}lll@{\hspace{2ex}}l}
Bonds & $L$ & $::=$&$ \emptyset$ & {\sf (empty)}\\

&& $\shortmid$ &$ \{a-^x b\}$ & {\sf (bond)}\\

&& $\shortmid$ & $ L \uplus L $ & {\sf (union)}\\

Actions & $\alpha$&$::=$&$\overline{x}(b) $ & {\sf (bond)}\\

&& $\shortmid$ & $ \underline{x}(b) $ & {\sf (unbond)}\\

Processes &$P$&$::= $&$\textbf{0} $ & {\sf (empty)}\\ 

&& $\shortmid$ & $ \alpha.P $ & {\sf (action prefix)}\\

&& $\shortmid$ & $ P+Q$ & {\sf (choice)}\\

&& $\shortmid$ & $ P \mid Q$ & {\sf (parallel)}\\

&& $\shortmid$ & $ \textbf{if}\ a \Bumpeq^L b \ \textbf{then}\ P\ \textbf{else}\ Q $ & {\sf (testing)}\\

&& $\shortmid$ & $ A(b_1,\ldots,b_n) $ & {\sf (identifier)}\\

Definition & $A(a_1,\ldots,a_n)$&$::= $& $P$ & {\sf (recursion)}\\

System & $S$ & $::=$ & $ P \; ||\; L$ . \\
\end{tabular}
\egroup
\vspace{-2ex}\caption{Syntax of the Bonding Calculus}\label{table:syntax}
\vspace{-2ex}\end{figure}

A bond prefix $\overline{x}(b)$ is used to indicate the availability of 
a molecule with name~$b$ to create a new bond with name $x$, while an unbond 
prefix $\underline{x}(b)$ indicates the availability of $b$ to destroy an 
existing bond $x$. Creating or breaking a bond leads to an 
update of the global bond memory $L$. As several similar bonds can exist 
between the same molecules, $L$ is actually a multiset of~bonds.

The process $\textbf{0}$ denotes inactivity. The availability to perform an 
action $\alpha$, and then to continue the execution as process $P$ is denoted 
by the process $\alpha.P$. The process $P+Q$ offers a choice 
between the processes $P$ and $Q$, while the process $P \mid Q$ allows the 
execution of processes $P$ and $Q$ in parallel, with possible interactions 
between them by using appropriate actions.

As we work with bonds, we use the function $\Bumpeq: \mathcal{M}\times 
\N^{\mN} \times \mathcal{M} \rightarrow Bool$ to check whether between two 
molecules there exist certain bonds. For example, $a\Bumpeq^N b$ checks for the 
existence of all bonds in $N$ between the molecules $a$ and~$b$; it 
returns true when such bonds exist, and false otherwise. When we consider 
$N=\emptyset$, then $a\Bumpeq^{\emptyset}b$ checks if at least a bond 
exists between the two molecules. When $b=\varepsilon$, then $a\Bumpeq^N 
{\varepsilon}$ checks if $a$ has all of bonds from $N$, regardless of 
the molecules he has them with. The Boolean result $a \Bumpeq^N b$ used 
in the testing process is defined formally as:
\smallskip

$a \Bumpeq^N b=\begin{cases}
\displaystyle(\biguplus_{x \in N} \{a-^x b\}) \in L & N \neq \emptyset~and ~a \neq b \neq \varepsilon\\[15pt]
\displaystyle(\biguplus_{x \in \mN} \{a-^x b\}) \cap L \neq \emptyset & N = \emptyset~and ~a \neq b \neq \varepsilon\\[15pt]
\displaystyle\bigwedge_{x \in N} (|L|_{a,x}=|N|_x) & N \neq \emptyset~and ~a \neq \varepsilon ~and~b = \varepsilon\\[15pt]
\emph{undefined} & \emph{otherwise},
\end{cases}$

\noindent where $|L|_{a,x}$ is the number of bonds containing the molecule 
$a$ and bond name~$x$ that appear in the multiset $L$, while $|N|_x$ is 
the number of occurrences of~$x$ in~$N$.

Depending on the truth value of $a \Bumpeq^N\!\! b $, the process 
$\textbf{if}\;a \Bumpeq^N\!\! b$ $\;\textbf{then}\;P\;\textbf{else}\;Q$ 
executes either $P$ or $Q$.  An identifier $ A(b_1,\ldots,b_n) $ is used 
to provide recursion by creating new instances of processes defined as 
$A(a_1,\ldots,a_n)=P$, where $a_i \neq a_j$ for all $i\neq j \in 
\{1,\ldots,n\}$; the new process is defined as $ A(b_1,\ldots,b_n) 
=P\{b_1/a_1,\ldots,b_n/a_n\}$, where $\{b_i/a_i\}$ denotes the replacement 
of variable $a_i$ by value $b_i$. A system $S$ is given as a 
composition of a process $P$ and the multiset of bonds $L$, written as $P \; || \; L$.

The structural congruence relation $\equiv$ is the least congruence such 
that\linebreak $(\mP,+,{\bf 0})$ and $(\mP,\mid,{\bf 0})$ are commutative monoids 
and the unfolding law\linebreak  $A(b_1,\ldots,b_n) \equiv 
P\{b_1/a_1,\ldots,b_n/a_n\}$ holds whenever $A(a_1,\ldots,a_n)$ = $P$.

The calculus presented in \cite{NaCo18} was intended to model the 
creation and breaking of covalent bonds. In order to be able to model 
both covalent and hydrogen bonds, we apply a minor update to the 
operational semantics in \cite{NaCo18} because we need two instances of the 
rules used to create and to break bonds. The only difference between the 
two instances of the same rule is given by the names of~the bonds 
appearing in the interacting processes, and by the fact that a bond cannot 
be created using the names $x^+$ and $x^-$ if other bonds exist between 
the same molecules; more details about this restriction are given in 
the example below.

\begin{figure}[t]
\begin{center}
\begin{tabular}{c}
\vspace{1ex}
{\sf (CREATE1)} $\dfrac{P=\overline{x}(b).P'+P'' \quad Q= \overline{x}(a).Q'+Q''}{(P\mid Q)\ || \ L \xrightarrow{} (P' \mid Q') \ ||\ L \uplus \{a-^x b\}}$\\[10pt]
\vspace{1ex}
{\sf (CREATE2)} $\dfrac{P=\overline{x^+}(b).P'+P'' \quad Q= \overline{x^-}(a).Q'+Q''\quad a \Bumpeq^{\emptyset} b~is~false~w.r.t.~L}{(P\mid Q)\ || \ L \xrightarrow{} (P' \mid Q') \ ||\ L \uplus \{a-^x b\}}$\\[10pt]
\vspace{1ex}
{\sf (REMOVE1)} $\dfrac{P=\underline{x}(b).P'+P'' \quad Q= \underline{x}(a).Q'+Q'' \quad a \Bumpeq^x b~is~true~w.r.t.~L }{(P\mid Q)\ || \ L \xrightarrow{} (P' \mid Q') \ || \ L \backslash \{a-^x b\}}$\\[10pt]
\vspace{1ex}
{\sf (REMOVE2)} $\dfrac{P=\underline{x^+}(b).P'+P'' \quad Q= \underline{x^-}(a).Q'+Q'' \quad a \Bumpeq^N b~is~true~w.r.t.~L }{(P\mid Q)\ || \ L \xrightarrow{} (P' \mid Q') \ || \ L \backslash \{a-^x b\}}$\\[10pt]
\vspace{1ex}
{\sf (PAR)} $ \dfrac{P\ || \ L\xrightarrow{} P'\ || \ L}{(P\mid Q)\ || \ L\xrightarrow{} (P' \mid Q) \ || \ L}$\\[10pt]
\vspace{1ex}
{\sf (TRUE)} $\dfrac{a \Bumpeq^N b~is~true~w.r.t.~L}{(\textbf{if}\;a \Bumpeq^N b \;\textbf{then}\;P\;\textbf{else}\;
Q)\ || \ L  \xrightarrow{} P\ || \ L}$\\[10pt]
\vspace{1ex}
{\sf (FALSE)} $\dfrac{a \Bumpeq^N b~is~false~w.r.t.~L}{(\textbf{if}\;a \Bumpeq^N b \;\textbf{then}\;P\;\textbf{else}\;
Q)\ || \ L  \xrightarrow{} Q\ || \ L}$\\[10pt]

\vspace{1ex}
{\sf (IDE)} $\dfrac{P\{b_1/a_1,\ldots,b_n/a_n\} \xrightarrow{} P'}{A(b_1,\ldots,b_n) \xrightarrow{} P'}$ \ if \ $A(a_1,\ldots,a_n) =P$\\[10pt]

{\sf (STRUCT)} $\dfrac{S_1 \rightarrow S'_1 \quad S_1 \equiv S_2 \quad S_2 \rightarrow S'_2}{S'_1 \rightarrow S'_2}$

\end{tabular}
\end{center}
  \vspace{-2ex}\caption{Operational Semantics of the Bonding Calculus.}
  \label{table:semantics}
\vspace{-4ex}
\end{figure}

The operational semantics of the Bonding Calculus is given in Figure~\ref{table:semantics}. The rules {\sf (CREATE1)} and {\sf (CREATE2)} describe the creation of a 
new bond $\{a-^x b\}$, while the rules {\sf (REMOVE1)} and {\sf (REMOVE2)} 
describe the breaking of a bond $\{a-^x b\}$. If there exist two bonds 
$\{a-^x b\}$ in~$L$, then any of these bonds is broken. The rule 
{\sf (PAR}) is used to compose processes in parallel, while the rules 
{\sf (TRUE}) and {\sf (FALSE}) choose one of the branches of the testing 
process based on the result of the checking. The rule {\sf (IDE)} describes 
the recursion, while the {\sf (STRUCT)} rule indicates the fact that we reason 
up to the structural congruence.


\subsubsection{The autoprotolysis of water in the Bonding Calculus}We use two types of bond names, namely $c$ and $h$, 
to stand for the covalent and hydrogen bonds, respectively. Using our  
calculus, the system composed of two molecules of water is described by:

\begin{center}
$MolOxy_2(O_1) \mid \MolHy_1(H_1) \mid \MolHy_1(H_2) $
\end{center}
\begin{center}
$\mid \MolOxy_2(O_2) \mid \MolHy_1(H_3) \mid \MolHy_1(H_4) $
\end{center}
\begin{center}
$\mid\mid \{O_1 -^c H_1, O_1 -^c H_2, O_2 -^c H_3, O_2 -^c H_4\}$
\end{center}


\noindent 
where the molecules are those of hydrogen and oxygen that are described below:
\vspace{1mm}

$\MolHy_0(H_i) = \overline{c}(H_i).\MolHy_1(H_i)$
\vspace{1mm}

$\MolHy_1(H_i) = \underline{c}(H_i).\MolHy_0(H_i) + \overline{h^+}(H_i).\MolHy_2(H_i)$;
\vspace{1mm}

$\MolHy_2(H_i) = \underline{c}(H_i).\overline{c}(H_i).\underline{h^+}(H_i).\MolHy_{1}(H_i)$.
\vspace{1mm}

$\MolOxy_0(O_i) = \overline{c}(O_i).\MolOxy_1(O_i)$;
\vspace{1mm}

$\MolOxy_1(O_i) = \underline{c}(O_i).\MolOxy_0(O_i) +\overline{c}(O_i).\MolOxy_2(O_i)$;
\vspace{1mm}

$\MolOxy_2(O_i) = \underline{c}(O_i).\MolOxy_1(O_i) +\overline{h^-}(O_i).\MolOxy_3(O_i)$.
\vspace{1mm}

$\MolOxy_3(O_i) = \underline{h^-}(O_i).\MolOxy_2(O_i)$.
\vspace{1mm}

\noindent 
Each molecule of water is a structure consisting of one molecule of oxygen 
and two molecules of hydrogen which are properly bonded. For example, the process 
$\MolOxy_2(O_1) \mid \MolHy_1(H_1) \mid \MolHy(H_2) $ together with the 
bonds $\{O_1 -^c H_1, O_1 -^c H_2\}$ model one molecule of water. We use 
unique names for the molecules given as $O_i$ (for oxygen) and $H_i$ (for 
hydrogen), while the processes having the names $\MolHy_i$ and $\MolOxy_i$ 
identify processes modelling hydrogen and oxygen molecules with~$i$ bonds, 
respectively. For example, the process $MolOxy_1(O_i)$ can either create or break 
bonds, and this is why we use the operator $+$ to describe such a  
(non-deterministic) choice.

Now we present the steps of one of the possible sequences of reactions modelling the 
autoprotolysis of water. The system of two molecules of water can be 
rewritten as follows (where we extend the definitions for the processes 
that will interact in the next step, and bold the actions to be executed):

\begin{center}$\underline{c}(O_1).\MolOxy_1(O_1) +{\bf \overline{h^-}(O_1)}.\MolOxy_3(O_1) \mid \MolHy_1(H_1) \mid \MolHy_1(H_2) $
\end{center}

\begin{center}$\mid \MolOxy_2(O_2) \mid \MolHy_1(H_3) \mid \underline{c}(H_4).
\MolHy_0(H_4) + {\bf \overline{h^+}(H_4)}.\MolHy_2(H_4)$
\end{center}

\begin{center}$\mid\mid \{O_1 -^c H_1, O_1 -^c H_2, O_2 -^c H_3, O_2 -^c H_4\}$
\end{center}

\noindent 
This leads to the next system, where we again bold the processes to be~executed:
\begin{center}$\MolOxy_3(O_1) \mid \MolHy_1(H_1) \mid \MolHy_1(H_2) $
\end{center}

\begin{center}$\mid {\bf \underline{c}(O_2)}.\MolOxy_1(O_2) +\overline{h^-}(O_2).\MolOxy_3(O_1) \mid \MolHy_1(H_3)$
\end{center}

\begin{center}$ \mid {\bf \underline{c}(H_4)}.\overline{c}(H_4).\underline{h^+}(H_4).\MolHy_{1}(H_4)$
\end{center}

\begin{center}$\mid\mid \{O_1 -^c H_1, O_1 -^c H_2, O_1-^h H_4,O_2 -^c H_3, O_2 -^c H_4\}$
\end{center}

\noindent 
The creation of the hydrogen bond forces the break of the other bond in 
which the hydrogen molecule $H_4$ is involved. This leads to the following
system containing the $H_3O$ and $HO$ molecules:

\begin{center}$\MolOxy_3(O_1) \mid \MolHy_1(H_1) \mid \MolHy_1(H_2) $\end{center}

\begin{center}$\mid \underline{c}(O_2).\MolOxy_0(O_2) +{\bf \overline{c}(O_2)}.\MolOxy_2(O_2)$\end{center}

\begin{center}$ \mid \MolHy_1(H_3)$ $ \mid {\bf \overline{c}(H_4)}.\underline{h^+}(H_4).\MolHy_{1}(H_4)$\end{center}

\begin{center}$\mid\mid \{O_1 -^c H_1, O_1 -^c H_2, O_1-^h H_4,O_2 -^c H_3\}$\end{center}

\noindent 
Since some bonds are weaker, the system is evolving to:

\begin{center}${\bf \underline{h^-}(O_1)}.\MolOxy_2(O_1) \mid \MolHy_1(H_1) \mid \MolHy_1(H_2) $\end{center}

\begin{center}$\mid \MolOxy_2(O_2)$ $ \mid \MolHy_1(H_3)$ $ \mid {\bf \underline{h^+}(H_4)}.\MolHy_{1}(H_4)$\end{center}

\begin{center}$\mid\mid \{O_1 -^c H_1, O_1 -^c H_2, O_1-^h H_4,O_2 -^c H_3, O_2 -^c H_4\}$\end{center}

\noindent 
followed by the breaking of the hydrogen bond $O_1-^h H_4$:

\begin{center}$\MolOxy_2(O_1) \mid \MolHy_1(H_1) \mid \MolHy_1(H_2) $\end{center}

\begin{center}$\mid \MolOxy_2(O_2)$ $ \mid \MolHy_1(H_3)$ $ \mid \MolHy_{1}(H_4)$\end{center}

\begin{center}$\mid\mid \{O_1 -^c H_1, O_1 -^c H_2, O_2 -^c H_3, O_2 -^c H_4\}$\end{center}

\noindent 
The obtained system contains again two water molecules of water.

\subsection{Reversing Petri Nets}
In this subsection we present Reversing Petri Nets~\cite{RPNs} (RPNs, pronounced as `reversing Petri nets'), an extension of Petri nets
developed for the modelling reversing computations, and we employ the formalism
to model the autoprotolysis of water. 

\subsubsection{Definition of RPNs}

We consider
an extension of reversing Petri nets suitable for describing chemical reactions by allowing multiple tokens of the same type as well as the possibility for 
transitions to break bonds. Thus, a transition may simultaneously create
and/or destroy bonds, and its reversal results in the opposite effect. Formally, a Reversing Petri net
is defined as follows:

\begin{definition}{\rm
		A \emph{\PN}(RPN) is a tuple $(P,T,  A, A_V, B, F)$ where:
		\begin{enumerate}
			\item $P$ is a finite set of \emph{places} and
			$T$ is a finite set of \emph{transitions}.
			\item $A$ is a finite set of \emph{base} or \emph{token types} ranged over by $a, b,\ldots$.
			$\overline{A} = 
			\{\overline{a}\mid a\in A\}$ contains a ``negative"  version for each token type. We assume that
			for any token type $a$ there may exist a finite number of \emph{token instances}. 
			We write $a_1,\ldots,$ for
			instances of type $a$ and $A_I$ for the set of all token instances. 
			\item $A_V$ is a finite set of \emph{token variables}. We write $\type(v)$ for the type
			of variable $v$ and assume that $\type(v) \in A$ for all $v\in A_V$.
			\item $B\subseteq A\times A$ is a finite set of undirected \emph{bond} types ranged over
			by $\beta,\gamma,\ldots$. We use the notation $a \bond b$ for a bond $(a,b)\in B$.  
			$\overline{B} = \{\overline{\beta}\mid \beta\in B\}$ contains a ``negative" version for 
			each bond type. $B_I\subseteq A_I\times A_I$ is a finite set of \emph{bond instances},
			where we write $\beta_i$ 
			for elements of $B$.
			\item $F : (P\times T  \cup T \times P)\rightarrow {\cal P}( A_V \cup (A_V \times A_V) \cup \overline{A}
			\cup \overline{B}) $ 
			is a set of directed labelled \emph{arcs}.
		\end{enumerate}
}\end{definition}

A reversing Petri net is built on the basis of a set of \emph{tokens} or \emph{bases}. These
are organised in a set of token types $A$, where each token type is associated with a set of token instances.
Token instances correspond to the basic entities that occur in a system and they may occur as 
stand-alone elements but as computation proceeds they may also merge together to form \emph{bond 
	instances}. 
Places and transitions have the standard meaning and are connected
via directed arcs, which are labelled by a set of elements from $A_V \cup (A_V \times A_V) \cup \overline{A}
\cup \overline{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 RPN is portrayed as a directed bipartite graph where token instances are indicated by $\bullet$, places by
circles, transitions by boxes, and bond instances by lines between token instances. 



Before we recall the semantics of RPNs we need to introduce some notation. Note that in 
what follows we omit the discussion of negative tokens and negative bonds as they are not relevant to our
case study.  
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
$\guard{t}  =   \bigcup_{x\in P} F(x,t)$ 
for the union of all labels on the
incoming arcs of  transition $t$, 
and $\effects{t}  =   \bigcup_{x\in P} F(t,x)$
for the union of all labels on the 
outgoing arcs of transition $t$. 
\begin{definition}\label{well-formed}{\rm 
		A \PN is \emph{well-formed}, if for all $t\in T$:
		\begin{enumerate}
			\item $A_V\cap \guard{t} = A_V\cap \effects{t}$,
			\item $ F(t,x)\cap F(t,y)\cap A_V=\emptyset$ for all $x,y\in P$, $x\neq y $. 
		\end{enumerate}
}\end{definition}
Thus, a \PN is well-formed if (1) whenever a variable exists in
the incoming arcs of a transition then it also exists on the outgoing arcs, which implies that transitions do not
erase tokens, and  (2) 
tokens/bonds cannot be cloned into more than one outgoing places.

As with standard Petri nets the association of token/bond instances to places is called a \emph{marking}  such that 
$M: P\rightarrow 2^{A_I\cup B_I}$, where we assume that if $(u,v)\in M(x)$ then $u, v\in M(x)$. 
In addition, we employ the notion of a \emph{history}, which~assigns a memory to each
transition $H : T\rightarrow \mathbb{N}$. 
Intuitively, a history of $H(t) = 0$ for some $t \in T$ captures that the transition has not taken place, or 
every execution of it has been reversed, and a history
of $ H(t)=k, k>0$, captures that the transition had $k$ forward executions that have not been  reversed.
Note that $H(t)>1$ may
arise due to the consecutive execution of the transition with different token
instances. A pair of a marking and a history, $\state{M}{H}$, describes a \emph{state} of a RPN 
with $\state{M_0}{H_0}$ the initial state, where $H_0(t) = 0$ for all $t\in T$. 

Finally, we define $\connected(a_i,C)$, where $a_i\in A_I$ and $C\subseteq 2^{A_I\cup B_I}$,
to be the token instances connected
to $a_i$  as well as the bonds creating these connections according to 
set $C$. 

\paragraph{Forward Execution.}
During the forward execution of a transition in a RPN, 
a set of tokens and bonds, as specified by the incoming arcs of the transition, are selected and
moved to the outgoing places of the transition, as specified by the transition's outgoing arcs, possibly
forming or destructing bonds, as necessary. Due to the presence of multiple instances of the same token
type, it is possible that different token instances are selected during the transition's execution.  


A transition is forward-enabled in a state $\state{M}{H}$ of a \PN if there exists a selection of token instances 
available at the incoming places of the transition 
matching the requirements  on the transitions incoming arcs. Formally:

\begin{definition}\label{fenabled}{\rm
		Given a \RPN $(P,T, A, A_V, B, F)$, a state $\state{M}{H}$, and a transition $t$, we say that $t$ is 
		\emph{forward-enabled} in $\state{M}{H}$  if there exists a surjective function 
		$U:\guard{t}\cap A_V\rightarrow A_I$ such that:
		
		\begin{enumerate}
			\item  for all $v\in\guard{t}$, if $\type(v) = a$	then $\type(U(v))=a$
			\item for all $a\in F(x,t)$, then $U(a)\in M(x)$ and for all $(a,b)\in F(x,t)$, then $(U(a),U(b))\in M(x)$, 
			\item for all
			$(a,b)\in \effects{t}-\guard{t}$ then $(U(a),U(b))\not\in M(x)$ for all $x\in\circ t$.
		\end{enumerate}
}\end{definition}

Thus, $t$ is enabled in state $\state{M}{H}$ if  (1) there is a type-respecting assignment of token instances
to the variables on the incoming edges, with (2) the token instances originating from the appropriate
input places of the transition and  connected with
bonds as required by the variable bonds occurring on the incoming edges, and (3) if a bond
occurs in the outgoing edges of the transition but not the incoming ones, then the selected instances
associated with the bond's variables should not be bonded together in the incoming places
of the transition (thus transitions do not recreate bonds). We refer to $U$ as a forward enabling 
assignment.

To execute a transition $t$ according to an enabling assignment $U$, 
the selected token instances, along with their connected components,
are relocated to the outgoing places of the transition as specified
by the outgoing arcs, with bonds created and destructed accordingly. 
Furthermore,
the history of the executed transition is increased by one.
\begin{definition}{\rm \label{forward}
		Given a \RPN $(P,T,  A, A_V, B, F)$, a state $\langle M, H\rangle$, and an
		enabling assignment $U$, we write $\state{M}{H}
		\trans{t} \state{M'}{H'}$
		where for all $x\in P$:
		\[
		M'(x) =   M(x)- \bigcup_{a\in f(x,t)} \connected(U(a), M(x)) 
		\cup  \bigcup_{a\in f(t,x),U(a)\in M(y)} \connected(U(a),S)\]
		where $S= (M(y)
		-\{(U(a),U(b))\mid (a,b)\in F(y,t)\})\cup \{ (U(a),U(b))\mid (a,b)\in F(t,x) \}$
		\[
		\hspace{0.2in}\mbox{and}\hspace{0.2in}
		H'(t') = \left\{
		\begin{array}{ll}
		H(t')+1, \hspace{1cm} \textrm{ if } t' = t  \; \\
		H(t'), \hspace{1.5cm}  \;\textrm{ otherwise }
		\end{array}
		\right.			\]	
}\end{definition} 


\paragraph{Reversing Execution.}
We now move on to  reversing transitions. 
A transition can be reversed in a certain state if it has been previously executed and 
there exist token instances in its output places 
that match the requirements on its outgoing arcs. Specifically, we define the notion of reverse 
enabledness as follows:
\begin{definition}\label{renabled}{\rm
		Consider a \RPN $(P,T, A, A_V, B, F)$, a state $\state{M}{H}$, and a transition $t$.
		We say that $t$ is \emph{reverse-enabled} in $\state{M}{H}$ if (1)  $H(t)\neq 0$, and (2)
		there exists a surjective function 
		$W:\effects{t}\cap A_V\rightarrow  A_I$ such that:
		\begin{enumerate}
			\item  for all
			$v\in\effects{t}$, if $\type(v) = a$
			then $\type(W(v))=a$, 
			\item for all $a\in F(t,x)$, then $W(a)\in M(x)$ and for all $(a,b)\in F(t,x)$, then $(W(a),W(b))\in M(x)$, 
			\item  for all $(a,b)\in \guard{t} - \effects{t}$ then $(W(a),W(b))\not\in M(x)$ for all $x\in\circ t$.
		\end{enumerate}
}\end{definition}

Thus, a transition $t$ is reverse-enabled in $\state{M}{H}$ if  
(1) the transition has been executed and (2) there exists a type-respecting assignment of token instances,
from the instances in the out-places of the transition, to the variables on the outgoing
edges of the transition, and where the instances are connected with bonds as required by
the transition's outgoing edges.  Also we do not recreate existing bonds when going backwards. 
We refer to $W$ as a reversal enabling assignment.
To implement the reversal of a transition $t$ according to a reversal enabling assignment $W$, 
the selected instances are relocated from  the outgoing places of the transition to the incoming places,
as specified
by the incoming arcs of the transition, with bonds created and destructed accordingly.

\begin{definition}\label{causal}{\rm
		Given a \RPN $(P,T, A, A_V, B, F)$, 
		a state $\langle M, H\rangle$, and a transition $t$ reverse-enabled in $\state{M}{H}$  with 
		$W$ a reversal enabling assignment, we write $ \state{M}{H}
		\rtrans{t} \state{M'}{H'}$   where for all $x$:
		\[
		M'(x) =   M(x)- \bigcup_{a\in f(t,x)} \connected(W(a), M(x)) 
		\cup  \bigcup_{a\in f(x,t),W(a)\in M(y)} \connected(W(a),S)\]
		where $S= (M(y)
		-\{(W(a),W(b))\mid (a,b)\in F(t,y)\})\cup \{ (W(a),W(b))\mid (a,b)\in F(x,t) \}$
		\[
		\hspace{0.3in}\mbox{and}\hspace{0.3in}
		H'(t') = \left\{
		\begin{array}{ll}
		H(t') - 1, \hspace{0.3cm} \;\;\textrm{ if } t' = t  \; \\
		H(t'),\hspace{1cm}  \;\textrm{ otherwise }
		\end{array}
		\right.
		\]
}\end{definition}	



\begin{figure}
	\centering
	\subfigure{\includegraphics[width=10cm]{model.png}}\\
	\vspace{-0.25cm}
	\subfigure{\includegraphics[width=.5cm]{arrowt1.png}}
	\subfigure{\includegraphics[width=10cm]{aftert1.png}}\\\vspace{-0.25cm}
	\subfigure{\includegraphics[width=.5cm]{arrowt2.png}}
	\subfigure{\includegraphics[width=10cm]{aftert2.png}}\\	\caption{RPN model of the formation of a water molecule.}
	\label{RPNmodel}
\end{figure}

\begin{figure}
        \centering
        \subfigure{\includegraphics[width=.5cm]{arrowt1.png}}
        \subfigure{\includegraphics[width=.5cm]{arrowt2.png}}
        \subfigure{\includegraphics[width=10cm]{aftert22.png}}\\\vspace{-0.25cm}
        \subfigure{\includegraphics[width=.5cm]{arrowt3.png}}
        \subfigure{\includegraphics[width=10cm]{aftert3.png}}\\\vspace{-0.25cm}
        \subfigure{\includegraphics[width=.5cm]{arrowt3r.png}}
        \subfigure{\includegraphics[width=10cm]{aftert3r.png}}
        \caption{RPN model of the execution of the autoprotolysis of water.}
        \label{execution}
\end{figure}


\noindent
\textbf{The autoprotolysis of water in RPNs } Figure~\ref{RPNmodel} shows the graphical representation of the forming of a water molecule as a RPN.
In this model, we assume two token types, $H$ for hydrogen
and $O$ for oxygen. They are instantiated via four token instances of $H$ ($H_1$, $H_2$, $H_3$, and $H_4$) and two token instances of
$O$, ($O_1$ and $O_2$). The net consists of five places and three transitions and the edges between
them are associated with token variables and bonds, where we assume that $\type(o)=\type(o_1)=\type(o_2) = O$
and $\type(h)=\type(h_1)=\type(h_2)=\type(h_3)=\type(h_4)=H$. 
Looking at the transitions, transition $t_1$ models the formation of a bond between a hydrogen
token and an oxygen token. Precisely, the transition stipulates a selection of two such
molecules with the use
of variables $o$ and $h$ on the incoming arcs of the transition which are bonded
together, as described in the outgoing arc of the transition.
Subsequently, transition $t_2$ completes
the formation of a water molecule by selecting an oxygen token from place $x$ and
a hydrogen token from place $v$ and forming a bond between them, placing the resulting component at place $y$. Note that the selected oxygen instance in this transition will be connected to a hydrogen token via a bond 
created by transition $t_1$; this bond is preserved and the component resulting from the creation of
the new $o-h$ bond will be transferred to place $y$.
Finally, transition $t_3$ models the autoprotolysis reaction: assuming the existence of two distinct oxygen
instances, as required by the variables $o_1$ and $o_2$ on the incoming arc of the transition, connected
with hydrogen instances as specified in $F(y,t_3)$, the transition breaks the bond $o_2-h_3$ and forms the
bond  $o_1-h_3$.  As such, assuming the existence of two water molecules at place $y$, the transition
will form  a hydronium  (H$_3^+$O) and a hydroxin (OH$^-$) molecule in place $z$ of the net.
The reversibility semantics of RPNs ensures that  reversing the transition $t_3$ will result in the re-creation
of  two water molecules placed at $y$, while the use of variables allows the formation of water molecules consisting
of different bonds between the hydrogen and oxygen instances. 

The first net in Figure~\ref{execution}  shows the system after the execution of transition $t_1$ with enabling assignment $U(h)=H_1$, $U(o)=O_1$. Note
that the term $[1]$ written over transition $t_1$ captures that at this point $H(t_1)=1$ 
since the transition has been executed once.
This notation is generally used for histories in the graphical representation with occasional
missing histories corresponding to histories equal to $0$.
Subsequently,
we have the model after execution of transition $t_2$ with enabling assignment $U(h)=H_2$,
$U(o)=O_1$, creating the bond $O_1-H_2$, thus forming the first water molecule. A second
execution of transitions $t_1$ and $t_2$ results in the second molecule of water in the system,
placed again at place $y$, as shown in the third net in the figure. At this state, transition
$t_3$ is forward-enabled and,  with enabling assignment $U(o_1)=O_1, U(o_2)=O_2, U(h_1)=H_1, 
U(h_2)=H_2,U(h_3)=H_3,U(h_4)=H_4$, we have the creation of the hydronium and hydroxide
depicted at place $z$ in the fourth net of the figure. At this stage, transition $t_3$ is
now reverse-enabled and the last net in the figure illustrates the state resulting after
reversing $t_3$ with reversal enabling assignment $W(o_1)=O_1, W(o_2)=O_2, W(h_1)=H_1, 
W(h_2)=H_3,W(h_3)=H_2,W(h_4)=H_4$.


\section{Evaluation}
\label{sec:evaluation}

We have presented three formalisms which can be used to model chemical reactions. 
CCB is a reversible version of ACP that employs communication keys to record executed actions.
Its main feature is a mechanism to link forming and breaking of bonds, which gives rise to 
a type of explicit reversibility we call ``locally controlled reversibility''. We have modelled 
a simple covalent chemical reaction in CCB. A similar modelling approach can be used to model 
more complex atoms and reactions, for example, involving carbon atoms \cite{KUHN201818}. 
Finally, CCB can also be used to model reactions beyond simple chemical reactions \cite{merevcomp2018}. 
In CCB, we can actually distinguish different instances of the same atom or molecule, and of
identical actions in a process via the use of subscripts. As mentioned above, the reverse reaction 
in the autoprotolysis of water can work by transferring any of the hydrogens of the hydronium. 
When reversing the reaction in CCB, instead of the transition in Section~\ref{sec:ccb}, we could 
also have done this (writing the transition and the rewrite together):
%
\begin{flalign*}
&(( (h_1[1];p).H'_1 \paral (h_2[2];p).H'_2 \paral (o_1[1],o_2[2],n[5]).O'_1) \paral (h_3[5];p).H'_3) &&\\
&\paral (h_4[4];p).H'_4  \paral (o_3,o_4[4],n).O'_2&&\\
&\xrightarrow{\{ np[3], \underline{nh_{1}}[1]\}} \Rightarrow &&\\
&(( (\boldsymbol{h_1[3]};p).H'_1 \paral (h_2[2];p).H'_2 \paral (\boldsymbol{o_1[5]},o_2[2],\boldsymbol{n}).O'_1) \paral (h_3[5];p).H'_3) &&\\
&\paral (h_4[4];p).H'_4  \paral (\boldsymbol{o_3[3]},o_4[4],\boldsymbol{n}).O'_2
\end{flalign*}
%
The result is different from that in Section~\ref{sec:ccb}, but identical from a chemical point of view, since the hydrogens are all identical. On the other hand a technique called isotopic labelling can be used to trace atoms by using different isotopes of, in this case hydrogen, confirming that the different options happen in reality. In CCB, we can trace the atoms as well as show which results are identical from a chemical point of view (see Section 6.5 of \cite{KUHN201818}).

The Bonding Calculus is suitable for modelling in a natural way the autoprotolysis of water by using only bond and unbond actions. Simulations by using a software platform can describe the dynamics of the bonding systems, and so it is possible to test the validity of some underlying assumptions. Also, we can verify various properties of the bonding compounds described by using the calculus.


Reversing Petri Nets are Petri net structures that assume tokens to be distinct and persistent. During the execution of transitions individual tokens can be bonded/unbonded with each other, and the creation/destruction of these bonds is considered to be the effect of a transition, whereas their destruction/creation is the effect of the transition's reversal. Reversing Petri Nets are a natural choice to model and analyse biochemical reaction systems, such as the autoprotolysis of water, which by nature
has multi-party interactions, is inherently concurrent, and features reversible behaviour. 
In particular, the feature of token multiplicity and
the use of variables allows to non-deterministically
select different combinations of atoms of a particular element when creating molecules. Also the ability
of 
transitions to break bonds allows to model concerted actions where, for example, a transition simultaneously
destroys  a water molecule and creates a hydronium whose  reversal results in the opposite effect. Moreover,
the collective token interpretation adopted in the framework, treating all tokens of the same type
as equivalent, allows the reaction to reverse into two different water molecules than the original ones,
i.e. using different instances of the atoms (as is possible in CCB).
Note that the presented model abstracts away the positive/negative charge of the atoms and
captures the existence of electrons by the enabledness of transitions. A model at a lower
level of abstraction would be possible by introducing tokens to represent the electrons  bonded to the associated
atom tokens to illustrate the relevant charges. 


The three formalisms presented can model our example fairly well but, as expected, 
there are some differences. In order to evaluate each formalism, we consider as first criterion if all 
chemically valid interactions between the compounds of the reaction can be represented well in 
our formalisms. 
CCB shows the linked forming and breaking of bonds.
RPNs can also express these concerted actions,
since a transition enables the simultaneous creation and destruction of bonds. 
In the Bonding Calculus, this link is not expressed. Each of the formalisms 
can perform the forward reaction using any of the hydrogens involved. CCB and RPNs can perform 
the reverse reaction by transferring arbitrary hydrogens, whereas the Bonding Calculus in  the reverse
reaction permits only the transfer of exactly those hydrogens that were used in the forward reaction. 
All models presented use subscripts and enable the tracking of atoms.

The other criterion for assessing the suitability of our formalisms for the modelling of chemical reactions
is to ask if they enable in the produced model any transitions that actually do not occur in reality. 
Each formalism does not permit a $H_3O^+$ molecule to be formed directly. CCB allows 
one reaction which is not realistic: 
If there are many water molecules and therefore several hydroxide and water molecules at the same time, 
it is possible that the remaining hydrogen is transferred from the hydroxide to a water. In reality, 
this is not possible since the hydroxide is strongly negatively charged and no hydrogen bond can form.
Due to the nondeterministic behaviour of processes written with the `+' operator, such as those for
hydrogen and oxygen in Subsection~3.2, the Bonding Calculus also presents the same problem.
However, this is not the case for RPNs since, on the one hand, a transition's conditions make restrictions
on the types of molecules
that will participate in a transition firing or its reversal and, on the other hand, places impose a form of locality
for molecules. For instance, in the autoprotolysis example, each place is the location of specific types of molecules,
e.g., transition $t_3$ modelling the autoprotolysis reaction is only applied on water molecules and its reversal
only on pairs of a hydronium and a hydroxide molecule, as required.

There are a number of software tools  that can aid simulation and analysis for our formalisms. Regarding the Bonding Calculus, we can simulate various bonding descriptions by
using an existing software platform called UPPAAL (as shown in [1]). For CCB, there 
is a simulation tool presented in \cite{merevcomp2018}. It allows a much closer form 
of representation of chemical notation than that possible with a typical programming language.
Reversing Petri nets have been shown to be closely related to Coloured Petri Nets, as a subset 
of the former model has been encoded into the latter~\cite{RPNtoCPN}. 
Thus, an algorithmic translation can be implemented that transforms RPNs to CPNs in an automated
manner using the transformation techniques discussed in~\cite{RPNtoCPN}. This allows RPNs to 
exploit tools such as CPNTools that support traditional models of Petri nets. 

\section{Conclusion}
\label{sec:conclusion}
We have presented the Calculus of Covalent Bonding, the Bonding Calculus, and Reversing
Petri Nets as models of chemical reactions and reversible processes in general. We have shown
that they can all model the out-of-causal-order reversibility present in such reactions. We have also noted 
that the two process calculi allow few reactions which do not happen in reality. This is due to 
the modelling that abstracts away from some chemical properties of atoms and molecules such as, for example,
spacial arrangement and distance between molecules. 
In future work, we plan to develop these formalisms further and apply
them to the modelling and reasoning about reversible biochemical reactions and processes.

\addcontentsline{toc}{chapter}{Bibliography}

\begin{thebibliography}{10}
\providecommand{\url}[1]{\texttt{#1}}
\providecommand{\urlprefix}{URL }
\providecommand{\doi}[1]{https://doi.org/#1}

\bibitem{NaCo18}
Aman, B., Ciobanu, G.: Bonding calculus. Natural Computing  \textbf{17}(4),
  823--832 (2018)

\bibitem{DBLP:journals/nc/BaldanCMS10}
Baldan, P., Cocco, N., Marin, A., Simeoni, M.: Petri nets for modelling
  metabolic pathways: a survey. Natural Computing  \textbf{9}(4),  955--989
  (2010)

\bibitem{RPNtoCPN}
Barylska, K., Gogoli\'{n}ska, A., Mikulski, {\L}., Philippou, A., Pi{\c
  a}tkowski, M., Psara, K.: Reversing computations modelled by coloured {P}etri
  nets. In: Proceedings of ATAED 2018. {CEUR} Workshop Proceedings, vol.~2115,
  pp. 91--111 (2018)

\bibitem{PNbiology}
Bl{\"a}tke, M.A., Heiner, M., Marwan, W.: Petri nets in systems biology.
  Technical Report, Otto-von-Guericke University Magdeburg  (2011)

\bibitem{DBLP:journals/bib/Chaouiya07}
Chaouiya, C.: Petri net modelling of biological networks. Briefings in
  Bioinformatics  \textbf{8}(4),  210--219 (2007)

\bibitem{CiocchettaBiopepa}
Ciocchetta, F., Hillston, J.: Bio-{PEPA}: A framework for the modelling and
  analysis of biological systems. Theoretical Computer Science
  \textbf{410}(33-34),  3065--3084 (2009)

\bibitem{danoscausality}
Danos, V., Feret, J., Fontana, W., Harmer, R., Krivine, J.: Rule-based
  modelling of cellular signalling. In: Caires, L., Vasconcelos, V.T. (eds.)
  CONCUR 2007 - Concurrency Theory, Lecture Notes in Computer Science,
  vol.~4703, pp. 17--41. Springer (2007)

\bibitem{danos2004ccsr}
Danos, V., Krivine, J.: Reversible communicating systems. In: Gardner, P.,
  Yoshida, N. (eds.) CONCUR 2004 - Concurrency Theory, Lecture Notes in
  Computer Science, vol.~3170, pp. 292--307. Springer (2004)

\bibitem{pmid19399430}
Faeder, J.R., Blinov, M.L., Hlavacek, W.S.: {{R}ule-based modeling of
  biochemical systems with {B}io{N}et{G}en}. Methods in Molecular Biology
  \textbf{500},  113--167 (2009)

\bibitem{biocham}
Fages, F., Soliman, S., Chabrier-Rivier, N.: Modelling and querying interaction
  networks in the biochemical abstract machine {BIOCHAM}. Journal of Biological
  Physics and Chemistry  \textbf{4},  64--73 (2004)

\bibitem{ACPBook}
Fokkink, W.: Introduction to Process Algebra. Springer (2000)

\bibitem{DBLP:journals/jsamas/HofestadtH94}
Hofest{\"{a}}dt, R.: A {P}etri net application of metabolic processes. Journal
  of System Analysis, Modeling and Simulation  \textbf{16},  113--122 (1994)

\bibitem{DBLP:journals/isb/HofestadtT98}
Hofest{\"{a}}dt, R., Thelen, S.: Quantitative modeling of biochemical networks.
  In Silico Biology  \textbf{1}(1),  39--53 (1998)

\bibitem{merevcomp2018}
Kuhn, S.: Simulation of base excision repair in the calculus of covalent
  bonding. In: Karri, J., Ulidowski, I. (eds.) Reversible Computation, 10th
  International Conference, RC 2018, Lecture Notes in Computer Science, vol.
  11106, pp. 123--129. Springer (2018)

\bibitem{KU16}
Kuhn, S., Ulidowski, I.: A calculus for local reversibility. In: Devitt, S.,
  Lanese, I. (eds.) Reversible Computation, 8th International Conference, RC
  2016, Lecture Notes in Computer Science, vol.~9720, pp. 20--35. Springer
  (2016)

\bibitem{KUHN201818}
Kuhn, S., Ulidowski, I.: Local reversibility in a calculus of covalent bonding.
  Science of Computer Programming  \textbf{151}(Supplement C),  18--47 (2018)

\bibitem{Lanese_controllingreversibility}
Lanese, I., Mezzina, C.A., Schmitt, A., Stefani, J.B.: Controlling
  reversibility in higher-order pi. In: Katoen, J.P., K{\"o}nig, B. (eds.)
  CONCUR 2011 - Concurrency Theory, Lecture Notes in Computer Science,
  vol.~6901, pp. 297--311. Springer (2011)

\bibitem{Lanese_controlled}
Lanese, I., Mezzina, C.A., Stefani, J.B.: Controlled reversibility and
  compensations. In: Gl{\"u}ck, R., Yokoyama, T. (eds.) Reversible Computation,
  4th International Workshop, RC 2012, Lecture Notes in Computer Science,
  vol.~7581, pp. 233--240. Springer (2013)

\bibitem{LaneseMS10}
Lanese, I., Mezzina, C.A., Stefani, J.B.: Reversing higher-order pi. In:
  Gastin, P., Laroussinie, F. (eds.) CONCUR 2010 - Concurrency Theory. Lecture
  Notes in Computer Science, vol.~6269, pp. 478--493. Springer (2010)

\bibitem{DBLP:journals/nc/MatsunoNM11}
Matsuno, H., Nagasaki, M., Miyano, S.: Hybrid {P}etri net based modeling for
  biological pathway simulation. Natural Computing  \textbf{10}(3),  1099--1120
  (2011)

\bibitem{Milner1980}
Milner, R.: A Calculus of Communicating Systems, Lecture Notes in Computer
  Science, vol.~92. Springer (1980)

\bibitem{DBLP:journals/jamia/PelegRA05}
Peleg, M., Rubin, D.L., Altman, R.B.: Using {P}etri net tools to study
  properties and dynamics of biological systems. {Journal of the American
  Medical Informatics Association}  \textbf{12}(2),  181--199 (2005)

\bibitem{RPNs}
Philippou, A., Psara, K.: Reversible computation in petri nets. In: Kari, J.,
  Ulidowski, I. (eds.) Reversible Computation - 10th International Conference,
  {RC} 2018, Leicester, UK, September 12-14, 2018, Proceedings. Lecture Notes
  in Computer Science, vol. 11106, pp. 84--101. Springer (2018)

\bibitem{RC19}
Philippou, A., Psara, K., Siljak, H.: Controlling reversibility in reversing
  {P}etri nets with application to wireless communications. In: Thomsen, M.K.,
  Soeken, M. (eds.) Reversible Computation - 11th International Conference,
  {RC} 2019. Lecture Notes in Computer Science, vol. 11497, pp. 238--245.
  Springer (2019)

\bibitem{Irek2007}
Phillips, I., Ulidowski, I.: Reversing algebraic process calculi. The Journal
  of Logic and Algebraic Programming  \textbf{73}(1-2),  70--96 (2007)

\bibitem{irekconcur2013}
Phillips, I., Ulidowski, I.: Reversibility and asymmetric conflict in event
  structures. In: D'Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013 -
  Concurrency Theory, Lecture Notes in Computer Science, vol.~8052, pp.
  303--318. Springer (2013)

\bibitem{Irek2013}
Phillips, I., Ulidowski, I., Yuen, S.: Modelling of bonding with processes and
  events. In: Dueck, G.W., Miller, D.M. (eds.) Reversible Computation, 5th
  International Conference, RC 2013, Lecture Notes in Computer Science,
  vol.~7948, pp. 141--154. Springer (2013)

\bibitem{Irek2012}
Phillips, I., Ulidowski, I., Yuen, S.: A reversible process calculus and the
  modelling of the {ERK} signalling pathway. In: Gl{\"u}ck, R., Yokoyama, T.
  (eds.) Reversible Computation, 4th International Workshop, RC 2012, Lecture
  Notes in Computer Science, vol.~7581, pp. 218--232. Springer (2013)

\bibitem{DBLP:journals/fuin/Popova-ZeugmannHK05}
Popova{-}Zeugmann, L., Heiner, M., Koch, I.: Time {P}etri nets for modelling
  and analysis of biochemical networks. Fundamenta Informaticae
  \textbf{67}(1-3),  149--162 (2005)

\bibitem{PriamiStochasticPi}
Priami, C.: Stochastic $\pi$-calculus. The Computer Journal  \textbf{38}(7),
  578--589 (1995)

\bibitem{betabinders}
Priami, C., Quaglia, P.: Beta binders for biological interactions. In: Danos,
  V., Schachter, V. (eds.) Computational Methods in Systems Biology. pp.
  20--33. Springer (2005)

\bibitem{DBLP:conf/ismb/ReddyML93}
Reddy, V.N., Mavrovouniotis, M.L., Liebman, M.N.: Petri net representations in
  metabolic pathways. In: Proceedings of the 1st International Conference on
  Intelligent Systems for Molecular Biology. pp. 328--336. {AAAI} (1993)

\bibitem{RegevBioambients}
Regev, A., Panina, E.M., Silverman, W., Cardelli, L., Shapiro, E.: Bioambients:
  an abstraction for biological compartments. Theoretical Computer Science
  \textbf{325}(1),  141--167 (2004)

\bibitem{Regev2004}
Regev, A., Shapiro, E.: The $\pi$-calculus as an abstraction for biomolecular
  systems. In: Ciobanu, G., Rozenberg, G. (eds.) Modelling in Molecular
  Biology. pp. 219--266. Springer (2004)

\bibitem{PNs}
Reisig, W.: Understanding Petri Nets - Modeling Techniques, Analysis Methods,
  Case Studies. Springer (2013)

\bibitem{Uli92}
Ulidowski, I.: Equivalences on observable processes. In: Proceedings of the 7th
  Annual IEEE Symposium on Logic in Computer Science. pp. 148--159. IEEE (1992)

\bibitem{irekNGC2018}
Ulidowski, I., Phillips, I., Yuen, S.: Reversing event structures. New
  Generation Comput.  \textbf{36}(3),  281--306 (2018)

\bibitem{DBLP:journals/isb/VossHK03}
Voss, K., Heiner, M., Koch, I.: Steady state analysis of metabolic pathways
  using {P}etri nets. In Silico Biology  \textbf{3}(3),  367--387 (2003)

\end{thebibliography}
\bibliographystyle{splncs04}

\end{document}