* (70) M. F. Brown, “Theory of spin-lattice relaxation in lipid bilayers and biological membranes. 2H and 14N quadrupolar relaxation,” J. Chem. Phys. 77, 1576-1599 (1982).
  * (71) S-T. Lai, P. Palting, Y-N. Chiu, and H. J. Silverstone, “On the summations involving Wigner rotation matrix elements,” J. Math. Chem. 24, 123-132 (1998).
  * (72) R. van Wageningen, “Explicit polynomial expressions for finite rotation operators,” Nucl. Phys. 60, 250-263 (1964).
  * (73) T. A. Weber and S. A. Williams, “Spin-matrix polynomials and the rotation operator for arbitrary spin,” J. Math. Phys. 6, 1980-1983 (1965).
  * (74) R. H. Albert, “Still another way to calculate representations of the three-dimensional pure rotation group,” Proc. Camb. Phil. Soc. 63, 273-275 (1967).
  * (75) A. J. Torruella, “Representations of the three-dimensional rotation group by the direct method,” J. Math. Phys. 16, 1637-1642 (1975).
  * (76) D. Kusnezov, “Exact matrix expansions for group elements of SU(n),” J. Math. Phys. 36, 898-906 (1995).
  * (77) T. L. Curtright, D. B. Fairlie, and C. K. Zachos, “A compact formula for rotations as spin matrix polynomials,” SIGMA 10, 084 (2014).
  * (78) W. Happer, “A partial-wave expansion of the rotation operator,” Ann. Phys. (NY) 48, 579-591 (1968).
  * (79) D. A. Varshalovich, A. N. Moskalev, and V. K. Khersonskii, “Demonstration of rotation group using the $(\psi,{\bf\hat{n}})$ parameters,” Izv. akad. nauk. SSSR ser. Fiz. 38, 1711-1726 (1974).
  * (80) G. S. Agarwal, “Relation between atomic coherent-state representation, state multipoles, and generalized phase-space distributions,” Phys. Rev. 24, 2889-2896 (1981).
  * (81) K. Husimi, “Some formal properties of the density matrix,” Proc. Phys. Math. Soc. Jpn. 22, 264-314 (1940).
  * (82) E. Ambler, J. C. Eisenstein, and J. F. Schooley, “Traces of products of angular momentum matrices,” J. Math. Phys. 3, 118-130 (1962).
  * (83) M. Keller, “Spin-1 behavior of systems of dipolar coupled pairs of spin-1/2 nuclei,” Adv. Magn. Reson. 12, 183-246 (1988).
  * (84) I. D. Ryabov, “On the generation of operator equivalents and the calculation of their matrix elements,” J. Magn. Reson. 140, 141-145 (1999).
  * (85) G. G. Ohlsen, “Polarization transfer and spin correlation experiments in nuclear physics,” Rep. Progr. Phys. 35, 717-801 (1972).
  * (86) F. Li, C. Braun and A. Garg, “The Weyl-Wigner-Moyal formalism for spin,” Europhys. Lett. 102, ????? (2013).
  * (87) J. Schwinger, “On angular momentum,” United States Atomic Energy Commission Technical Report NYO-3071 (1952).
  * (88) J. Schwinger, “On angular momentum,” in Quantum Theory of Angular Momentum, edited by L. C. Biedenharn and H. van Dam (Academic Press New York,1965).
  * (89) J. Schwinger, On Angular Momentum (Dover, New York, 2015).
  * (90) J. Schwinger, L. L. DeRaad Jr., K. A. Milton, and W. Tsai, Classical Electrodynamics (Perseus Books, Cambridge, 1989).
  * (91) A. Garg, Classical Electromagnetism in a Nutshell (Princeton University Press, Princeton, 2012).
  * (92) R. Courant and D. Hilbert, Methods of Mathematical Physics, Volume I (Interscience, New York, 1953).
  * (93) This generating function formula can be found on p. 542 of Appendix A in Courant and Hilbert. couranth  Courant and Hilbert couranth  acknowledge W. Magnus for the appendix, which according to them “is based on unpublished notes by G. Herglotz.”
  * (94) A. P. Prudnikov, Yu. A. Brychkov, O. I. Marichev, Integrals and Series. Volume 2. Special Functions (Gordon and Breach, New York, 1986).
  * (95) Wolfram Research, Mathematica, (www.wolfram.com), 2004.
  * (96) M. Rotenberg, R. Bivins, N. Metropolis, and J. K. Wooten, Jr., The 3-j and 6-j Symbols (MIT Press, Cambridge, 1959).
  * (97) Given the equivalence between Chebyshev polynomials and Clebsch-Gordan coefficients, the finite difference expression for the Chebyshev polynomials in this table implies that Clebsch-Gordan coefficients are also related to finite differences. varshal1:ang
  * (98) In the notation of this article, ${\bf J}^{2}={\bf J}\cdot{\bf J}\equiv\kappa=j(j+1)$.


# Unrestricted Error-Type Codebook Generation for Error Correction Code in DNA
Storage Inspired by NLP

Yi Lu1, Yun Ma1, Chenghao Li2, Xin Zhang 3, Guangxiang Si4  1 School of
Mathematical Sciences, Capital Normal University, Beijing, China,
<EMAIL_ADDRESS>2 Liangjiang International College,
Chongqing University of Technology, Chongqing, China,
<EMAIL_ADDRESS>3 Institute of Systems Biomedicine, Peking
University, Beijing, China Email<EMAIL_ADDRESS>4 School of Biological
Science and Medical Engineering, Southeast University, Nanjing, China.
<EMAIL_ADDRESS>
###### Abstract

THIS PAPER IS ELIGIBLE FOR THE STUDENT PAPER AWARD.
Recently, DNA storage has surfaced as a promising alternative for data
storage, presenting notable benefits in terms of storage capacity, cost-
effectiveness in maintenance, and the capability for parallel replication.
Mathematically, the DNA storage process can be conceptualized as an insertion,
deletion, and substitution (IDS) channel. Due to the mathematical complexity
associated with the Levenshtein distance, creating a code that corrects for
IDS remains a challenging task. In this paper, we propose a bottom-up
generation approach to grow the required codebook based on the computation of
Edit Computational Graph (ECG) which differs from the algebraic constructions
by incorporating the Derivative-Free Optimization (DFO) method. Specifically,
this approach is regardless of the type of errors. Compared the results with
the work for 1-substitution-1-deletion and 2-deletion, the redundancy is
reduced by about 30-bit and 60-bit, respectively. As far as we know, our
method is the first IDS-correcting code designed using classical Natural
Language Process (NLP) techniques, marking a turning point in the field of
error correction code research. Based on the codebook generated by our method,
there may be significant breakthroughs in the complexity of encoding and
decoding algorithms.

##  I Introduction

###  I-A Background and Motivation

DNA, as the most natural form of information storage, presents numerous
advantages over traditional storage mediums[1, 2], notably its high storage
density and low maintenance costs, which establish it as an ideal medium for
long-term information storage. Due to the characteristics of the DNA storage
medium, it is susceptible to environmental factors and experimental errors,
leading to data inaccuracies. Therefore, error correction codes become crucial
in DNA storage[3, 4].

Despite advancements in correcting deletion errors, challenges persist [5].
These include constructing minimal-redundancy deletion codes that allow
efficient decoding, improving existential redundancy bounds, and efficiently
addressing a mix of deletions and substitutions. Although some research [6, 3]
has proposed codes combining the mentioned deletion and substitution codes,
the quest for more redundancy-efficient methods continues.

The string-to-string correction problem [7, 8, 9] as a tpoic in NLP has been
extensively researched in the past and plays a crucial role in various fields,
just as we have seen, such as, spell checking, auto-correction, search engines
and information retrieval. In NLP tasks, at least a correct corpus is needed
as an evaluation criterion, but there is no such criterion in coding theory.
We only need to consider how to efficiently generate the codebook.

Currently, there is little literature [10, 11] discussing the generation of
codebooks. However, the method in literature [11] is only designed to address
errors related to edit distance. Moreover, it is challenging to generate long
sequences through top-down filtering. While the approach in literature [10]
focuses exclusively on substitution-type errors. The codebook generated by our
method is capable of handling errors involving p-substitution-q-deletion.
Furthermore, this method has the potential to generate a codebook tailored to
the maximum errors for different nucleotides.

###  I-B An Overview of Our Solution

A bottom-up approach to generate the codebook by iteration is adopted,
avoiding inefficient brute-force searches in $4^{n}$ arbitrary sequences.
Utilizing derivative-free optimization (DFO) methods [12], we optimize
redundancy to an acceptable range while meeting error correction requirements.
Once the codebook is obtained, there is no need to generate a new one unless
there is a demand for improvement in the current codebook. We can encode the
input binary sequence segment-wise based on the codebook index. The decoding
and error correction processes have been extensively studied in classical
literature [13, 14, 15, 16]. Therefore, this paper will focuse solely on the
generation of the codebook.

In order to generate the desired codebook, the first step is to design a ”loss
function” called ECG, that reflects how much the current codebook achieve the
need of error correction in each step. For the overall loss, we can consider
it as the sum of the losses between each pair of distinct sequences. When
designing this algorithm, we need to ensure that it satisfies the following
points:

  * •

Residues of Feasible Edit Counts. Differing from sequence matching and
sequence similarity, what we consider here is all feasible edits between two
sequences, providing sufficient indication for the redundancy to be added in
each iterative step. The entire computation is still implemented based on
dynamic programming [7]. At the same time, it is necessary to return a non-
negative value for residues, which is used to determine how many operations
are remaining until the completion of the distance calculation.

  * •

Constrained Edit Information. This idea [17] takes into account the impact of
the maximal number of substitution, insertion, and deletion on the computation
of edit information. Due to the varied distribution of errors associated with
different nucleotides [2], a more stringent constraint, considering the
limitations on different types of editing counts for various nucleotides, is
worth considering. This implies a reduction in the volume of the error ball,
thereby holding great potential for enhancing the redundancy of the encoding.

  * •

Incremental Computation. Increasing efficiency as the string length grows, we
have the concept of incremental computation for edit distance [18]. This
involves calculating additional edit information based solely on the previous
step’s results, rather than re-evaluating from the start.

  * •

Lazy Evaluation. Although insertions and deletions can affect the positions of
sequence matches, once the upper bounds for insertion and deletion counts are
determined, it is unnecessary to calculate all positions [19].

Based on the ECG mentioned above, after defining the maximum error scenario
and codebook size, we can iteratively generate the codebook. We start by
initializing a set of empty sequences. Next, for each sequence, we enter a
loop of two steps: generation of candidate, selection of the optimal
candidates and result concatenation,

  * •

Generation of candidate: In DNA storage, there is often a requirement for
compatibility, such as GC balance and run length. This requirement can be
addressed during candidate generation [20, 21].

  * •

Selection of the optimal candidates: Due to the discrete nature of sequences,
the process of selecting the optimal candidates for maximal code rate should
involve DFO .

Input: $n,EOI,EQ$Initialization of Codebook $C$$Loss==0$Candidates
GenerationOptimal SelectionResult ConcatenationOutput $C$YN Figure 1: Workflow
of codebook generation

###  I-C Arrangement

We outline the section arrangement of this paper.

In the next sectionII, we introduce the concepts and symbols relevant to this
paper. In SectionIII, the ECG (Edit Computational Graph) algorithm and its
implementation using bitwise operations are introduced. Then, we present the
process of encoding generation. In this paper, the focus is primarily on
utilizing the Monte Carlo method as the optimization algorithm. In SectionV,
we provide a rough analysis of its time and space complexity. We conclude the
paper in SectionVI.

##  II Basic Concepts and Notations

In this paper, we state several symbols:

Symbol |  Meaning
---|---
$\Sigma_{q}$ |  q-alphabet with q elements.
C |  A codebook over $\Sigma_{q}$ .
$l(C)$ |  The length of each sequence in $C$.
$\lvert C\rvert$ |  Size of codebook.
$n(C)$ |  The number of binary bits which $C$ can represent .
$r(C)$ |  The redundancy of C.

Concretely, we use the symbols $\Sigma_{2}=\\{0,1\\}$ and
$\Sigma_{4}=\\{A,G,C,T\\}$ to represent alphabets of binary symbols and
nucleotide symbols, respectively.

Naturally, a metric is a measure of the degree of distinction between two
sequences.

###### Definition II.1

The metric of a sequence is the following mapping

$d:\Sigma^{n}\times\Sigma^{n}\rightarrow\mathbb{R}_{\geq 0},$

satisfying the following property: $\forall x,y,z\in\Sigma^{n}$

  * •

Non-negativity: $d(x,y)\geq 0$.

  * •

Identity: $d(x,y)=0\Leftrightarrow x=y.$

  * •

Symmetry: $d(x,y)=d(y,x).$

  * •

Triangle Inequality: $d(x,y)\leq d(x,z)+d(z,y).$

Specifically, there are several types of metric,

We can define a ”ball” in sequence metric space.

###### Definition II.2

A(n) (error) ball in the code space of sequence $s$ and radius $r$ is defined
as follow:

$B(s;r)=\\{s^{\prime}\in\Sigma^{|s|}:d(s,s^{\prime})\leq r\\}.$

For any $C$, if it exhibits a low enough level of ambiguity, it implies a
certain error-correcting capability. Thus for a given number $r$ and metric
$d$, the following conditions will be satisfied:

$B(s_{1};r)\cap B(s_{2};r)=\emptyset,\forall s_{1},s_{2}\in C,s_{1}\neq
s_{2}.$ (1)

Therefore, we have the following proposition.

###### Proposition II.1

Let $C$ be a codebook. $r$ and $d$ are the same as above and satisfy the
Condition 1. Then,

  * •

If $d=d_{H}$, $C$ possesses the capability to correct $r$ substitution errors,
i.e.

$\forall s_{1},s_{2}\in C,d_{H}(s_{1},s_{2})\geq 2r+1.$

  * •

If $d=d_{L}$, $C$ possesses the capability to correct $r$ edit (the sum of
substitution, insertion, and deletion errors) errors, i.e.

$\forall s_{1},s_{2}\in C,d_{L}(s_{1},s_{2})\geq 2r+1.$

  * •

If $d=d_{LCS}$, $C$ possesses the capability to correct $r$ insertion, and
deletion (sum) errors, i.e.

$\forall s_{1},s_{2}\in C,d_{LCS}(s_{1},s_{2})\geq 2r+1.$

However, the concept of a metric replaces dissimilarity with numerical values,
much like a “projection”, leading to the loss of a substantial amount of
information.

###### Example II.1

We define a codebook $C\subset\Sigma_{4}^{10}$ to be capable of correcting
simultaneous occurrences of $2$ substitution errors, $1$ insertion error and
$1$ deletion error. In fact, for $s_{1}=TCTTCTTCCG,s_{2}=TCCGCAGAAT$,
$s_{1},s_{2}\in C$, we cannot edit $s_{1}$ to $s_{2}$ within $4sub-2ins-2del$.
However, $d_{L}(s_{1},s_{2})=7$, and if we take the Levenshtein distance,

$B(s_{1};4)\cap B(s_{2};4)\neq\emptyset.$

Therefore, we cannot simply combine all editing methods into a single value
for analysis.

Let’s first introduce several symbols to represent different editing methods.

###### Definition II.3

All of the operations are based on $\Sigma_{4}$.We use
$[\textbf{SUB}],[\textbf{INS}],[\textbf{DEL}]$ to present the class of
substitution, insertion and deletion respectively. In each class, we have

  * •

$[\textbf{SUB}]=\\{\textbf{SUB}({c_{1}},{c_{2}}):c_{1},c_{2}\in\Sigma_{4}\\}\cup\\{\textbf{SUB}({*},{*})\\},$

  * •

$[\textbf{INS}]=\\{\textbf{INS}({c}):c\in\Sigma_{4}\\}\cup\\{\textbf{INS}({*})\\},$

  * •

$[\textbf{DEL}]=\\{\textbf{DEL}({c}):c\in\Sigma_{4}\\}\cup\\{\textbf{DEL}({*})\\},$

where $*$ means the absence of distinction of specific characters.

###### Definition II.4

Edit of Interest (EOI) is defined as an ordered array comprising elements in
$[\textbf{SUB}]$, $[\textbf{INS}]$, and $[\textbf{DEL}]$ classes, arranged in
sequential order.

Correspondingly, the maximum occurrence count for each edit is referred to as
the Edit Quota (EQ). $EQ$ is represented as an array, where each position
aligns with the respective operation in $EOI$.

Feasible Edit Count (FEC) refers to the tuple representing the count of
feasible edits generated during the editing process for a given $EOI$ and
$EQ$.

###### Example II.2

Let $s_{1}=AGC,s_{2}=AGG$, and
$EOI=([\textbf{SUB}],[\textbf{INS}],[\textbf{DEL}]),EQ=(1,1,1)$. So the
feasible edit count from $s_{1}$ to $s_{2}$ is $(1,0,0),(0,1,1)$.

Generally, we have the following proposition:

###### Proposition II.2

Given $EOI,EQ$, for a codebook $C$ to correct errors defined by $EQ$, any two
sequences, $s_{1},s_{2}\in C,s_{1}\neq s_{2}$, must satisfy: it is impossible
to edit $s_{1}$ into $s_{2}$ within $2*EQ$ operations or fewer.

This proposition is the generalization of Condition 1. The question of
calculating the ”edit reachability” within $EQ$ and effective calculation
methods will be discussed in the next section.

##  III Edit Computational Graph and Bit Encoding

The name ”Edit Computational Graph” comprises two elements. Firstly, ”edit”
emphasizes the specific editing operations under consideration. Secondly,
”computational graph” refers to a Directed Acyclic Graph (DAG), a term
commonly used in machine learning. ”Graph” essentially offers a statement of
the workflow for our algorithm. In this context, it signifies the use of a
similar DAG structure for computing information related to edits.

###  III-A Introduction of ECG

###### Definition III.1

Given $n\in\mathbb{Z}_{>0}$, $EOI$ (Edit of Interest) and $EQ$ (Edit Quota),
along with any two sequences $s_{1},s_{2}\in\Sigma_{4}^{n}$, we denote their
Edit Computational Graph as $\textbf{ECG}({s_{1}},{s_{2};EOI,EQ})$ or
$\textbf{ECG}({s_{1}},{s_{2}})$ if there is no ambiguity. The ECG consists of
two components: vertices ($V$) and edges ($E$).

Each node can be labeled with $(i,j)$, indicating all FECs within $EQ$ used to
transform $s_{1}[:i]$ to $s_{2}[:j]$.

Each edge represents different transitions for all FECs. For node $(i,j)$, let
$[\epsilon]$ be nothing to do, we have

$\begin{cases}(i-1,j-1)\rightarrow(i,j):\epsilon,&s_{1}[i]==s_{2}[j];\\\
\begin{cases}(i-1,j-1)\rightarrow(i,j):[\textbf{SUB}],\\\
(i-1,j)\rightarrow(i,j):[\textbf{DEL}],\\\
(i,j-1)\rightarrow(i,j):[\textbf{INS}],\end{cases}&s_{1}[i]!=s_{2}[j].\end{cases}$

As illustrated in the Figure2.

$(i-1,j)$$(i,j)$$(i,j-1)$$(i-1,j-1)$DeletionInsertionSubstitution(a) When
$s_{1}[i]!=s_{2}[j]$

$(i-1,j)$$(i,j)$$(i,j-1)$$(i-1,j-1)$No error(b) When $s_{1}[i]==s_{2}[j]$

Figure 2: State transitions on different edges. (a) represents the case of
$s_{1}[i]!=s_{2}[j]$ and (b) shows the case of $s_{1}[i]==s_{2}[j]$.

###### Example III.1

We assume $EOI=\\{\textbf{SUB},\textbf{INS},\textbf{DEL}\\}$ and $EQ=(4,2,2)$.
Suppose $s_{1}[i]!=s_{2}[j]$ and the data at each node are:

  * •

$(i-1,j):\\{(0,0,0),(4,1,1),(1,2,1),(1,1,2)\\};$

  * •

$(i,j-1):\\{(0,0,0),(4,1,1),(1,2,1),(1,1,2)\\};$

  * •

$(i-1,j-1):\\{(0,0,0),(4,1,1),(1,2,1),(1,1,2)\\};$

From $(i-1,j)$ to $(i,j)$, add $1$ to the coordinates corresponding to DEL and
add it to $(i,j)$. Then

$(i,j):\\{(0,0,1),(4,1,2),(1,2,2)\\}.$

Since $(1,1,3)$ is overflow, it is not added.

Next, from $(i,j-1)$ to $(i,j)$, we have

$(i,j):\\{(0,0,1),(4,1,2),(1,2,2),(0,1,0),(4,2,1)\\}.$

Note that the set does not retain duplicate elements.

Finally, from $(i-1,j-1)$ to $(i,j)$, we have

$\displaystyle(i,j):\\{$ $\displaystyle(0,0,1),(4,1,2),(1,2,2),$
$\displaystyle(0,1,0),(4,2,1),(1,0,0),$ $\displaystyle(2,2,1),(2,1,2)\\}.$

Furthermore, if $s_{1}[i]==s_{2}[j]$, then

$(i,j):\\{(0,0,0),(4,1,1),(1,2,1),(1,1,2)\\},$

which is same as $(i-1,j-1)$.

The case of such nodes may not happen in reality, but this is just an
intuitive example to demonstrate the data flow. Through the above example, we
summarize the following key points that the ECG should have.

  * •

Finiteness: The number of all FECs retained by each node is finite, at most
not exceeding $L=\prod_{i}(EQ[i]+1).$

  * •

Non-redundancy: Each node retains non-repeating FECs, meaning that all FECs
held by each node are distinct.

  * •

Boundedness: For any FEC $\alpha$ and any $i$ in $[|EQ|]$, $\alpha[i]$ is
nonnegative and bounded by $EQ[i].$ Otherwise, discard FECs with overflowed
coordinates.

  * •

Edge-Dependency: For any FEC, the updated coordinates are only related to the
traversed edges (Figure2).

  * •

Monotonicity: For any FEC, whenever passing through an edge with operations
($s_{1}[i]!=s_{2}[j]$), there must be an increase in certain coordinates.

###  III-B Bit Encoding and Algorithms

In order to efficiently achieve the aforementioned objectives, we encode all
of the FEC of a node using a bit with length $L$, and corresponding state
transitions are implemented using bitwise operations.

###### Definition III.2

Given base $EQ$, we define index encode

$\varphi:[L]\rightarrow\prod_{i\in[|EQ|]}[EQ[i]]$

and index decode

$\psi:\prod_{i\in[|EQ|]}[EQ[i]]\rightarrow[L]$

as a pair of mutually inverse bijections, where

$\varphi(i)[k]=\begin{cases}i\mod{EQ[0]},&k=0\\\ \lfloor
i/(\prod_{j=0}^{k-1}EQ[j])\rfloor\mod{EQ[k]},&\text{otherwise}\end{cases},$

and assume $(a_{0},a_{1},...,a_{|EQ|})\in\prod_{i\in[|EQ|]}[EQ[i]]$

$\psi((a_{0},a_{1},...,a_{|EQ|}))=a_{0}+\sum_{i=1}^{|EQ|-1}a_{i}(\prod_{j=0}^{i-1}EQ[j]).$

For the node $(i,j)$ , all its FECs are denoted as
$\beta(i,j)\in\Sigma_{2}^{L}$, satisfying the following conditions:

$\beta(i,j)[k]=\begin{cases}1&\varphi(i)\in(i,j)\\\
0&\varphi(i)\notin(i,j)\end{cases}.$

###### Example III.2

Recall the ExampleIII.1. $L=(4+1)(2+1)(2+1)=45$ and
$\beta(i,j)=01010000\;01000000\;01000001\;01000000\;00000000\;01010\in\Sigma_{2}^{L},$
when $s_{1}[i]!=s_{2}[j]$.

###### Definition III.3

The Edit Mask (EM) and the Shift Amount (SA) associated to $EOI,EQ$ are two
list defined below:

$EM[i]\in\Sigma_{2}^{L},EM[i][k]=\begin{cases}1&\varphi(k)[i]<EQ[i],\\\
0&\varphi(k)[i]==EQ[i],\end{cases}$ $SA[i]=\begin{cases}1&i=0,\\\
SA[i-1]*(EQ[i-1]+1)&i>0.\end{cases}$

Based on DefinitionIII.2 and DefinitionIII.3, we can provide a description of
the updated state transition algorithm for FEC (Algorithm1):

For the bit array of each node $\beta\in\Sigma_{2}^{L}$, we introduce a loss
function here to facilitate the latter generation algorithm.

###### Definition III.4

Given $EOI,EQ$, a loss function of bit array with regard to all FECs of a node
$\textbf{Loss}({\beta})$ is defined as follows:

$\displaystyle\textbf{Loss}:\Sigma_{2}^{L}$
$\displaystyle\rightarrow[L]\cup\\{L\\}$ $\displaystyle\beta$
$\displaystyle\mapsto L-min\\{i:\beta[i]==1\\}.$

###### Example III.3

Fix $s_{1},s_{2},EOI,EQ$,

  * •

if $s_{1}==s_{2}$, then $\beta(n,n)[0]=1,\textbf{Loss}({\beta(n,n)})=L;$

  * •

if $s_{1}$ cannot be edited into $s_{2}$ under the $EQ$ condition, then
$\forall k\in[L],\beta(n,n[k]=0,\textbf{Loss}({\beta(n,n)})=0.$

In coding theory, insertion and deletion edits significantly alter sequence
structure, so it is necessary to compute
$q=max\\{|[\textbf{INS}]|,|[\textbf{DEL}]|\\}$.

As a consequence, when calculating the ECG, it is also not necessary to
compare every position of the two sequences, as illustrated in Figure3.

Figure 3: Sequence alignment procedure in ECG at step $k$. If $k<q$, we just
start from the index $0$.

As a variant of sequence alignment algorithm, its basic idea is based on the
dynamic programming algorithm. For the dynamic programming matrix, we
implement a more space-efficient approach as illustrated in the figure.

$(k,k)$$(k-1,k)$$(k,k-1)$$...$$...$$...$$(k+1,k+1)$$(k,k+1)$$(k+1,k)$$...$$...$$\vdots$$\vdots$
Figure 4: Structure of dynamic programming matrix with size $2\times(2q+1)$.
Each element of the matrix is a bitarray of vertex in graph.

So we have Algorithm2 in appendix.

The following Figure5 is a flowchart illustrating the iteration process of ECG
at a specific step.

Figure 5: The flow chart of ECG iteration process.

##  IV Scheme of Codebook Generation

The performance of this scheme relies heavily on optimization and candidate
generation. To demonstrate that the scheme can accomplish the codebook
generation task, only Monte Carlo methods were employed for implementation:
generate several suffixes at random and select the option with the least loss.

Based on [21], we present Algorithm3 here as a reference, ensuring that each
iteration’s candidate maintains a certain GC-balance and run length.

##  V Analysis

###  V-A Redundancy

For whether error corrections can be achieved, we can calculate by constrained
edit distance. Therefore, we mainly analyze redundancy.

We have

$n(C)=\log_{2}(\lvert C\rvert).$

And the redundancy of $C$ is

$r(C)=n\log_{2}(q)-n(C).$

Since our approach generates sequences based on the size of codebook $C$, when
comparing with other methods, we adopt the codebook-redundancy comparison
approach.

###  V-B Complexity

The overall complexity is composed of two aspects

  * •

The computation of ECG.

  * •

The computation of codebook generation.

Fixed the number of $m=|C|$, the required codebook $C$ grows iteratively step
by step. In this process, ECG needs to be computed independently
$\frac{m(m-1)}{2}$ times. The steps of candidate generation and optimal
selection heavily depend on the specific implementation, and therefore, this
part is not within the scope of the discussion.

Next, we will focus our attention on the analysis of ECG.

For space complexity, we use a $2\times(2q+1)$ matrix to preserve the
intermediate result, where $q$ is the maximal number of ins/del. The size of
each element of the matrix depends on the setting of $EQ$, which is $L/8$,
$L=\prod_{i}(EQ[i]+1)$. Thus, the space complexity is at least $O(qLm^{2})$.

In terms of time complexity, let’s first count how many nodes need to be
traversed,

$\sum_{i=0}^{q}(2i+1)+(2q+1)(n-q-1)=n(2q+1)-q(q+1).$

The number of transitions (Algorithm1) each node needs to perform is $|EQ|$,
and the complexity of single transition is $O(3\lceil L/|Byte|\rceil)=O(L)$
(Bit operations are parallel for each bit in a byte). Hence, the computational
complexity for a single ECG calculation is at most

$O((n(2q+1)-q(q+1))(|EQ|L))=O(nqL|EQ|),q\ll n,$

and the minimum complexity for one iteration of codebook generation is
$O(m^{2}n(2q+1)-q(q+1))$.

###  V-C Result

Experimental data were obtained with the following equipment TableII.

We conducted tests on the codebook for correcting single-substitution single-
deletion errors, comparing the results with the state-of-the-art outcomes[3].
The comparison results are illustrated in the Figure6.

Because the actual runtime varies depending on the specific candidate
selection and optimization strategies, here, only a reference is provided
TableI.

For additional results, please refer to our GitHub.

##  VI Conclusions

In conclusion, this study has tackled the challenges associated with error
correction codes for DNA storage by transforming them into a problem analogous
to spell correction in natural language processing (NLP). By presenting a
novel approach to construct a codebook, the complexities of efficient
encoding, decoding, and error correction are alleviated. What was once a
formidable task of generating a highly redundant codebook is now reframed as a
puzzle akin to playing Go, offering a plethora of methods for resolution,
reminiscent of the strategies employed by AlphaGo. In the scenario of error
correction requirements with low hardware dependence, such as error correction
codes for DNA storage, a general approach is proposed, eliminating the need to
spend time constructing algorithms.

The proposed algorithm successfully mitigates the obstacles associated with
individual bit consideration. However, it is important to note that challenges
persist when addressing burst errors, and further discussion and exploration
are warranted in this context. Future research endeavors should delve into
refining the algorithm to encompass and effectively handle scenarios involving
burst errors. This advancement will contribute to the continued evolution of
DNA storage technologies, ensuring their robustness and effectiveness in
diverse contexts.

## References

  * [1] Y. Dong, F. Sun, Z. Ping, Q. Ouyang, and L. Qian, “Dna storage: research landscape and future prospects,” _National Science Review_ , p. 1092–1107, Jun 2020. [Online]. Available: http://dx.doi.org/10.1093/nsr/nwaa007
  * [2] L. Organick, S. D. Ang, Y.-J. Chen, R. Lopez, S. Yekhanin, K. Makarychev, M. Z. Racz, G. Kamath, P. Gopalan, B. Nguyen _et al._ , “Random access in large-scale dna data storage,” _Nature biotechnology_ , vol. 36, no. 3, pp. 242–248, 2018. [Online]. Available: http://dx.doi.org/10.1038/nbt.4079
  * [3] I. Smagloy, L. Welter, A. Wachter-Zeh, and E. Yaakobi, “Single-deletion single-substitution correcting codes,” in _2020 IEEE International Symposium on Information Theory (ISIT)_ , Jun 2020. [Online]. Available: http://dx.doi.org/10.1109/isit44484.2020.9174213
  * [4] K. Cai, Y. M. Chee, R. Gabrys, H. M. Kiah, and T. T. Nguyen, “Correcting a single indel/edit for dna-based data storage: Linear-time encoders and order-optimality,” _IEEE Transactions on Information Theory_ , vol. 67, no. 6, p. 3438–3451, Jun 2021. [Online]. Available: http://dx.doi.org/10.1109/tit.2021.3049627
  * [5] J. Sima, N. Raviv, M. Schwartz, and J. Bruck, “Error correction for dna storage,” _arXiv: 2310.01729_ , Oct 2023.
  * [6] W. Song and K. Cai, “Non-binary two-deletion correcting codes and burst-deletion correcting codes,” _IEEE Transactions on Information Theory_ , vol. 69, no. 10, June 2023. [Online]. Available: http://dx.doi.org/10.1109/TIT.2023.3285012
  * [7] R. A. Wagner and M. J. Fischer, “The string-to-string correction problem,” _Journal of the ACM_ , p. 168–173, Jan 1974. [Online]. Available: http://dx.doi.org/10.1145/321796.321811
  * [8] F. J. Damerau, “A technique for computer detection and correction of spelling errors,” _Communications of the ACM_ , vol. 7, no. 3, p. 171–176. [Online]. Available: http://dx.doi.org/10.1145/363958.363994
  * [9] K. Kukich, “Techniques for automatically correcting words in text,” _ACM Computing Surveys_ , p. 377–439, Dec 1992. [Online]. Available: http://dx.doi.org/10.1145/146370.146380
  * [10] C. Wu, “Designing communication systems via iterative improvement: error correction coding with bayes decoder and codebook optimized for source symbol error,” _arXiv: 1805.07429_ , May 2018.
  * [11] A. Guo, S. Sun, X. Wei, M. Wei, and X. Chen, “Dodo-code: a deep levenshtein distance embedding-based code for ids channel and dna storage,” _arXiv: 2312.12717_ , Dec 2023.
  * [12] J. Larson, M. Menickelly, and S. M. Wild, “Derivative-free optimization methods,” _Acta Numerica_ , p. 287–404, May 2019. [Online]. Available: http://dx.doi.org/10.1017/s0962492919000060
  * [13] R. Kashyap and B. Oommen, “An effective algorithm for string correction using generalized edit distances—i. description of the algorithm and its optimality,” _Information Sciences_ , vol. 23, no. 2, p. 123–142, Jan 1981. [Online]. Available: http://dx.doi.org/10.1016/0020-0255(81)90052-9
  * [14] J. L. Peterson, “Computer programs for detecting and correcting spelling errors,” _Communications of the ACM_ , vol. 23, no. 12, p. 676–687, Dec 1980. [Online]. Available: http://dx.doi.org/10.1145/359038.359041
  * [15] B. Oommen and R. Loke, “Pattern recognition of strings with substitutions, insertions, deletions and generalized transpositions,” _Pattern Recognition_ , vol. 30, no. 5, p. 789–800, May 1997. [Online]. Available: http://dx.doi.org/10.1016/s0031-3203(96)00101-x
  * [16] B. J. Oommen and R. K. S. Loke, _Noisy subsequence recognition using constrained string editing involving substitutions, insertions, deletions and generalized transpositions_ , Jan 1995, p. 116–123. [Online]. Available: http://dx.doi.org/10.1007/3-540-60697-1_94
  * [17] B. Oommen, “Constrained string editing,” _Information Sciences_ , vol. 40, no. 3, p. 267–284, Dec 1986. [Online]. Available: http://dx.doi.org/10.1016/0020-0255(86)90061-7
  * [18] S. R. Kim and K. Park, _A Dynamic Edit Distance Table_ , Jan 2000, p. 60–68. [Online]. Available: http://dx.doi.org/10.1007/3-540-45123-4_7
  * [19] L. Allison, “Lazy dynamic-programming can be eager,” _Information Processing Letters_ , vol. 43, no. 4, pp. 207–212, 1992. [Online]. Available: https://www.sciencedirect.com/science/article/pii/0020019092902027
  * [20] D. Knuth, “Efficient balanced codes,” _IEEE Transactions on Information Theory_ , vol. 32, no. 1, p. 51–53, Jan 1986. [Online]. Available: http://dx.doi.org/10.1109/tit.1986.1057136
  * [21] Y. Liu, X. He, and X. Tang, “Capacity-achieving constrained codes with gc-content and runlength limits for dna storage,” in _2022 IEEE International Symposium on Information Theory (ISIT)_ , Jun 2022. [Online]. Available: http://dx.doi.org/10.1109/isit50566.2022.9834494

##  Appendix A

Data: FEC bit array of the source node$\beta$; Type of edge $T$; FEC bit array
of the target node $\beta^{\prime}$

Result: FEC bit array of the target node $\beta^{\prime}$

Obtain the indices $I\subseteq[|EOI|]$ of all edits belonging to the class
$T$;

if  _$T!=\epsilon$_ then

Initiate a bit array $\alpha$;

for  _$i\in I$_ do

$\alpha\leftarrow bitAnd(\beta,EM[i])$;

$\alpha\leftarrow ShiftHight(\alpha,SA[i])$;

$\beta^{\prime}\leftarrow bitOr(\beta^{\prime},\alpha)$;

end for

end if

else

$\beta^{\prime}\leftarrow\beta$;

end if

Algorithm 1 Transition of FEC

Data: $EOI,EQ,EM,SA,q$

Input: String $s_{1},s_{2}\in\Sigma_{4}^{n}$;Start index of string $i_{0}$;
End index of string $i_{1}$; Last residue $m$; Start index of row $r_{0}$

Result: Residue $m^{\prime}$; Next index of row $r_{1}$

$m^{\prime}=Deepcopy(m)$ ;

for  _$i\in\\{i_{0},...,i_{1}-1\\}$_ do

$d\leftarrow min\\{q,i\\}$;

for  _$j\in\\{-2d,...,1\\}$_ do

$idx1\leftarrow(i+\lfloor j/2\rfloor)*(j\mod{2})$;

$idx2\leftarrow(i+\lfloor j/2\rfloor)*((j+1)\mod{2})$;

$bias\leftarrow\lfloor j/2\rfloor*(-1)^{(j\mod{2})}$;$row\leftarrow
i-i_{0}+r_{0}$;$col\leftarrow q+bias$;

if  _$s_{1}[idx1]==s_{2}[idx2]$_ then

// Trans is Algorithm1 (source node, edge type, target node)

$Trans(m[row-1,col],\epsilon,m[row,col])$ ;

end if

else

$tmp\leftarrow AllZeroBitArray\in\Sigma_{2}^{L}$;

if  _ $(s_{1}[idx1]\neq\text{' '})\&\&(s_{2}[idx2]\neq\text{' '})$_ then

// Substitution

$Trans(m[row-1,col],\textbf{SUB},tmp)$ ;

end if

if  _$(idx1!=0)\ &\&(col<2q)$_ then

// Deletion

$Trans(m[row+(-1\text{ if }bias<0\text{ else }0),col+1],\textbf{DEL},tmp)$ ;

end if

if  _$(idx2!=0)\ &\&(col>0)$_ then

// Insertion

$Trans(m[row+(-1\text{ if }bias>0\text{ else }0),col-1],\textbf{INS},tmp)$ ;

end if

end if

$m^{\prime}[row,col]\leftarrow tmp$;

end for

end for

$r_{1}\leftarrow r_{0}+i_{1}-i_{0}$ ;

Algorithm 2 Algorithm ECG

Data: $s,run,bal,L_{1},L_{2}$

Result: $C$

$capGC=bal*(L_{1}+L_{2})$;

Initialize a list $A=\\{s[n-L_{1}:]\\}$ and empty list $B=[]$;

while  _$A\neq\emptyset$_ do

$item=A.pop(0)$;

if  _$item.len()==L_{2}$_ then

$C.append(item)$;

continue;

end if

$itemLastNuc=item[-1]$;

$itemLastRun=item.lastRun()$ the run number of the last nucleotide;

$itemGCcount=item.countGC()$ ;

for  _$tail\in S$_ do

$tailRun=tail.len()$;

$tailNuc=tail[0]$;

if  _$tailNuc==G$ or $C$ and $itemGCcount+tailRun>capGC$_ then

continue;

end if

if  _$tailNuc==A$ or $T$ and $L_{1}-itemGCcount+tailRun>L_{1}+L_{2}-capGC$_
then

continue;

end if

if  _$lastNuc==itemLastNuc$ and $itemLastRun+tailRun\geq run$_ then

continue;

end if

$B.append(concatenate(item,tail))$;

end for

$A=B$;

$B=\emptyset$;

end while

Algorithm 3 Candidate Generation $5$$10$$15$$10$$20$$30$$40$$50$Size of CodebookRedundancy$r(C)$$r(C^{\prime})$ Figure 6: Comparison graph with state-of-the-art results [3]. Our approach computes three times for different codebook sizes and returns the length of the sequence $n$. The state-of-the-art result is $10log(n)+3log(q)+11,q=4$. Augmental Length | 2 | 3 | 4 | 5 | 8
---|---|---|---|---|---
Time Consumption(s) | 35.72 | 29.23 | 29.39 | 25.21 | 24.82
Sequence Length | 16 | 15 | 16 | 15 | 16
Redundancy | 27 | 25 | 27 | 25 | 27
TABLE I: The time consumption table regarding the generation of a codebook capable of handling single-substitution single-deletion. Processor: |  Intel(R) Core(TM) i7-7700HQ CPU @ 2.80GHz 2.80 GHz.
---|---
Memory (RAM): |  16.0 GB (15.9 GB available).
System Type: |  64-bit operating system, x64-based processor.
Python Version: |  3.7.3
Number of threads used |  1.
TABLE II: Device Parameters


Let $\M=(\Sta_{\M},\step{}_{\M},\uparrow_{\M})$, then there exists a finite set of atoms $K\subset\Atom$ such that, for every $(s,a,d,e,M,t)\in{\step{}_{\M}}$, and for every $K\mbox{-automorphism}\,\pi_K$, we have $\pi_K(s,a,d,e,M,t)\in{\step{}_{\M}}$. It follows that the transition system $\T(\M)$ is legal.

§ THE $\PI$-CALCULUS

*Transition systems of the $\pi$-calculus
The $\pi$-calculus was proposed by Milner, Parrow and Walker [18] as a language to specify processes with link mobility. In this paper, we shall consider the version presented in the textbook by Sangiorgi and Walker [20], excluding the match prefix.

We presuppose a countably infinite set $\N$ of names; we use strings of lower case letters for elements of $\N$.
The prefixes, processes and summations of the $\pi$-calculus are, respectively, defined by the following grammar:

\begin{align*}
\pi\      & \coloneqq\ \outcap{x}{y}\ \mid\ \incap{x}{z}\ \mid\ \taucap \qquad (x,y,z\in \N)\\
P\    & \coloneqq\ M\ \mid\  P\parc P\ \mid\ \restr{z}{P}\ \mid\ \repl{P}\\
M\   & \coloneqq\ \nil\ \mid\ \pref{\pi}P \mid\ M \altc M\enskip.
\end{align*}

We use $P\{z/y\}$ to denote a $\pi$-term obtained by substituting every occurrence of $y$ to $z$ in $P$.

An $\alpha$-conversion between $\pi$-terms is defined in [20] as a finite number of renaming of bound names. We write $P\aeq Q$ if $P$ and $Q$ are two $\pi$-terms that are $\alpha$-convertible.

We define the operational behaviour of $\pi$-terms by means of the structural operational semantics in Fig. <ref>, in which $\piact{}$ ranges over the set of actions of the $\pi$-calculus.

The transition system associated with a $\pi$-term is defined as follows:

Let $P$ be a $\pi$-term. $\T(P)=(\Sta_{P},\step{}_{P},\uparrow_{P})$ is the transition system associated with $P$, where

* $\Sta_{P}$ is the set of $\alpha$-equivalence classes of all reachable $\pi$-terms from $P$ by the operational semantics;

* $\step{}_{P}$ is the set of transitions between $\alpha$-equivalence classes of all reachable $\pi$-terms; and

* $\uparrow_{P}$ is the $\alpha$-equivalence class of $P$.

$\mathrm{PREFIX}\quad\inference{\,}{\tau.P\step{\tau}P}\quad \inference{}{\overline{x}y.P\step{\overline{x}y}P}\quad\inference{}{x(y).P\step{xz}P\{z/y\}}$

%%$\mathrm{MISMATCH}\quad\inference{P\step{\alpha}P',\,x\neq y}{if\,x\neq y\,then\,P\step{\alpha}P'}$\\
\quad\mathrm{PAR_L}\quad\inference{P\step{\piact{}}P'}{P\parc{Q}\step{\piact{}}P'\parc{Q}}\,\bn{\piact{}}\cap \fn{Q}=\emptyset$

\mathrm{CLOSE_L}\quad\inference{P\step{\overline{x}(z)}P',\,Q\step{xz}Q'}{P\parc{Q}\step{\tau}\restr{z}{(P'\parc{Q'})}}\,z\notin \fn{Q}$

\mathrm{OPEN}\quad\inference{P\step{\overline{x}z}P'}{(z)P\step{\overline{x}(z)}P'}\,z\neq x$

%  \quad\inference{P\mid !P\step{\piact{}}P'}{!P\step{\piact{}}P'}
\quad\inference{P\step{\piact{}}P'}{\repl{P}\step{\piact{}}P'\parc\repl{P}}
\quad\inference{P\step{\outact{x}{y}}P',\,P\step{\inact{x}{y}}P''}{\repl{P}\step{\tauact{}}(P'\parc P'')\parc\repl{P}}
\quad\inference{P\step{\boutact{x}{z}}P',\,P\step{\inact{x}{z}}P''}{\repl{P}\step{\tauact}\restr{z}{(P'\parc P'')}\parc\repl{P}}$

$\mathrm{ALPHA}\quad\inference{P\step{\piact{}}P'}{Q\step{\piact{}}P'}\,Q\aeq P$.

Operational rules for the $\pi$-calculus

*Proof of Corollary <ref>

We use $\N$ to denote the countable set of names used in the $\pi$-calculus, and we suppose that $\N=\Atom$. We suppose that $P$ is an arbitrary $\pi$-calculus process. We use $\fn{P}$ to denote the set of free names involved in $P$ and $\bn{P}$ to denote the set of bound names involved in $P$.

By Theorem <ref>, it is sufficient to show that for every $\pi$-calculus process $P$, the transition system $\T(P)$ is an effective legal transition system with atoms. The transition system is effective by the effectiveness of structural operational semantics of the $\pi$-calculus. Therefore, by Definition <ref>, it is sufficient to show that there is a finite set $K\subset\N$ such that $K$ is a support of $\T(P)$. We let $\T(P)=(\Sta_{\pi},\step{}_{\pi},P)$ be an $\Atau$ labelled transition system, and we take $K=\fn{P}\cup\{\tau\}$. Note that $\Sta_P$ is the set of $\pi$-terms and $\Atau$ is the set of labels, and hence $\Sta_{\pi}$ is a set with atoms and $\Atau$ is an orbit-finite set with atoms. To show that $K$ is a support of $\T(P)$, we only need to show that for every $(s,a,t)\in\step{}_{\pi}$, and for every $K$-automorphism $\pi_K$, $\pi_K(s,a,t)\in\step{}_{\pi}$.

We let $\pi_K$ be an arbitrary $K$-automorphism, and we show that $\pi_K(P)$ is an $\alpha$-conversion of $P$, i.e., $\pi_K(P)\aeq P$. We show it by a structural induction on $P$.
In the base case, $P=\nil$, then it is trivial that $\pi_K(P)=\nil\aeq P$.

For the step case, we distinguish with 7 cases.

* If $P=\pref{\tau}P'$, by induction hypothesis, we have $\pi_K(P')\aeq P'$. Hence, we have $\pi_K(\pref{\tau}P')=\pref{\tau}\pi_K(P')\aeq \pref{\tau}P'=P$.

* If $P=\pref{\outcap{x}{y}}P'$, by induction hypothesis, we have $\pi_K(P')\aeq P'$. Moreover, $x,y\in\fn{P}\in K$. Hence, we have $\pi_K(\pref{\outcap{x}{y}}P')=\pref{\outcap{x}{y}}\pi_K(P')\aeq \pref{\outcap{x}{y}}P'=P$.

* If $P=\pref{\incap{x}{y}}P'$, by induction hypothesis, we have $\pi_K(P')\aeq P'$. Moreover, $x\in\fn{P}\in K$. Hence, we have $\pi_K(\pref{\incap{x}{y}}P')=\pref{\incap{x}{\pi_K(y)}}\pi_K(P')\aeq\pref{\incap{x}{y}}P'=P$.

* If $P=P_1+P_2$, by induction hypothesis, we have $\pi_K(P_1)\aeq P_1,\,\pi_K(P_2)\aeq P_2$. Hence, we have $\pi_K(P_1+P_2)=\pi_K(P_1)+\pi_K(P_2)\aeq P_1+P_2=P$.

* If $P=P_1\parc P_2$, by induction hypothesis, we have $\pi_K(P_1)\aeq P_1,\,\pi_K(P_2)\aeq P_2$. Hence, we have $\pi_K(P_1\parc P_2)=\pi_K(P_1)\parc \pi_K(P_2)\aeq P_1\parc P_2=P$.

* If $P=\restr{z}{P'}$, by induction hypothesis, we have $\pi_K(P')\aeq P'$. Moreover, $\pi_K(z)=z'\notin K$. Hence, we have $\pi_K(\restr{z}{P'})=\restr{z'}{\pi_K(P')}\aeq \restr{z}{P'}=P$.

* If $P=\repl{P'}$, by induction hypothesis, we have $\pi_K(P')\aeq P$. Hence, we have $\pi_K(\repl{P'})=\repl{\pi_K(P')}\aeq \repl{P'}=P$.

By structural induction, we have shown that for every $K$-automorphism $\pi_K$, $\pi_K(P)\aeq P$. Therefore, we have $\pi_K(P)\in\Sta_{\pi}$. Hence, $K$ is a support of $\Sta_{\pi}$.

Next we still let $\pi_K$ be an arbitrary $K$-automorphism, and we show that for every transition $P\step{\piact}_{\pi}Q\in\step{}_{\pi}$, it satisfies that $\pi_K(P\step{\piact}_{\pi}Q)\in\step{}_{\pi}$ by an induction on the structural operational semantics of the $\pi$ calculus.

We construct a proof tree according to the structural operational semantics in Figure <ref> for every transition $(P,\piact,Q)\in\step{}_{\pi}$. The induction hypothesis is that, if $(P,\piact,Q)$ is induced from a set of transitions $\mathit{Pre}(P,\piact,Q)\subset\step{}_{\pi}$ , then for every transition $(P_i,\piact_i,Q_i)\in\mathit{Pre}(P,\piact,Q)$, there is $\pi_K(P_i,\piact_i,Q_i)\in\step{}_{\pi}$.
For the base case, the $\nil$ process cannot do any transition, then the property trivially holds. For the step case, we distinguish with several cases as follows.

* If the transition is $\pref{\tauact}P\step{\tauact}_{\pi}P$, then we have $\pi_K(\pref{\tauact}P)\step{\pi_K(\tauact)}_{\pi}\pi_K(P)$.

* If the transition is $\pref{\outcap{x}{y}}P\step{\outact{x}{y}}_{\pi}P$, then we have $\pi_K(\pref{\outcap{x}{y}}P)\step{\pi_K(\outact{x}{y})}_{\pi}\pi_K(P)$.

* If the transition is $\pref{\incap{x}{y}}P\step{\outact{x}{z}}_{\pi}P\{z/y\}$, then we have $\pi_K(\pref{\incap{x}{y}}P)\step{\pi_K(\inact{x}{z})}_{\pi}\pi_K(P\{z/y\})$.

* If the transition is $P_1+P_2\step{\piact}_{\pi}Q$, then there are two cases

* if $P_1\step{\piact}_{\pi}Q$. By induction hypothesis, we have $\pi_K(P_1)\step{\pi_K(\piact)}_{\pi}\pi_K(Q)$. Hence, we have $\pi_K(P_1+P_2)\step{\pi_K(\piact)}_{\pi}\pi_K(Q)$.

* If $P_2\step{\piact}_{\pi}Q$. The proof is symmetric with the previous case.

* If the transition is $P_1\parc P_2\step{\piact}_{\pi}Q_1\parc P_2$, then we have $P_1\step{\piact}_{\pi}Q_1$ and $\bn{\piact}\cap\fn{P_2}=\emptyset$. By induction hypothesis, we have $\pi_K(P_1)\step{\pi_K(\piact)}_{\pi}\pi_K(Q_1)$. Moreover, there is $\bn{\pi_K(\piact)}\cap\fn{\pi_K(P_2)}=\emptyset$. Hence we have $\pi_K(P_1\parc P_2)\step{\pi_K(\piact)}_{\pi}\pi_K(Q_1\parc P_2)$.

* If the transition is $P_1\parc P_2\step{\piact}_{\pi}P_1\parc Q_2$. The  proof is symmetric with the previous case.

* If the transition is $P_1\parc P_2\step{\tauact}_{\pi}Q_1\parc Q_2$, then we have $P_1\step{\outact{x}{y}}_{\pi}Q_1,\,P_2\step{\inact{x}{y}}_{\pi}Q_2$ (or the symmetrical case). By induction hypothesis, we have $\pi_K(P_1)\step{\pi_K(\outact{x}{y})}_{\pi}\pi_K(Q_1)$ and $\pi_K(P_2)\step{\pi_K(\inact{x}{y})}_{\pi}\pi_K(Q_2)$. Hence we have $\pi_K(P_1\parc P_2)\step{\pi_K(\tauact)}_{\pi}\pi_K(Q_1\parc Q_2)$.

* If the transition is $P_1\parc P_2\step{\tauact}_{\pi}\restr{z}{(Q_1\parc Q_2)}$, then we have $P_1\step{\boutact{x}{z}}_{\pi}Q_1$, $P_2\step{\inact{x}{z}}_{\pi}Q_2$, and $z\notin\fn{P_2}$ (or the symmetrical case). By induction hypothesis, we have $\pi_K(P_1)\step{\pi_K(\boutact{x}{z})}_{\pi}\pi_K(Q_1)$ and $\pi_K(P_2)\step{\pi_K(\inact{x}{z})}_{\pi}\pi_K(Q_2)$. Moreover, there is $\pi_K(z)\notin\fn{\pi_K(P_2)}$. Hence, we have $\pi_K(P_1\parc P_2)\step{\pi_K(\tauact)}_{\pi}\pi_K(\restr{z}{(Q_1\parc Q_2)})$.

* If the transition is $\restr{z}{P}\step{\piact}_{\pi}\restr{z}{Q}$, then we have $P\step{\piact}_{\pi} Q$ and $z\notin \piact$. By induction hypothesis, we have $\pi_K(P)\step{\pi_K(\piact)}_{\pi}\pi_K(Q)$. Moreover, there is $\pi_K(z)\notin\pi_K(\piact)$. Hence, we have $\pi_K(\restr{z}{P})\step{\pi_K(\piact)}_{\pi}\pi_K(\restr{z}{Q})$.

* If the transition is $\restr{z}{P}\step{\boutact{x}{z}}_{\pi}Q$, then we have $P\step{\outact{x}{z}}Q$, and $z\neq x$.  By induction hypothesis, we have $\pi_K(P)\step{\pi_K(\outact{x}{z})}_{\pi}\pi_K(Q)$. Moreover, there is $\pi_K(z)\neq\pi_K(x)$. Hence, we have $\pi_K(\restr{z}{P})\step{\pi_K(\boutact{x}{z})}_{\pi}\pi_K(Q)$.

* If the transition is $\repl{P}\step{\piact}_{\pi}Q\parc \repl{P}$, then we have $P\step{\piact}_{\pi}Q$. By induction hypothesis, we have $\pi_K(\repl{P})\step{\pi_K(\piact)}_{\pi}\pi_K(Q)$. Hence we have  $\pi_K(P)\step{\pi_K(\piact)}_{\pi}\pi_K(Q\parc \repl{P})$.

* If the transition is $\repl{P}\step{\tauact}_{\pi}(Q_1\parc Q_2)\parc \repl{P}$, then we have $P\step{\outact{x}{y}}_{\pi}Q_1$, and $P\step{\inact{x}{y}}_{\pi}Q_2$. By induction hypothesis, we have $\pi_K(P)\step{\pi_K(\outact{x}{y})}_{\pi}\pi_K(Q_1)$, and $\pi_K(P)\step{\pi_K(\inact{x}{y})}_{\pi}\pi_K(Q_2)$. Hence we have  $\pi_K(P)\step{\pi_K(\tauact)}_{\pi}\pi_K((Q_1\parc Q_2)\parc \repl{P})$.

* If the transition is $\repl{P}\step{\tauact}_{\pi}\restr{z}{(Q_1\parc Q_2)}\parc \repl{P}$, then we have $P\step{\boutact{x}{z}}_{\pi}Q_1$, and $P\step{\inact{x}{z}}_{\pi}Q_2$. By induction hypothesis, we have $\pi_K(P)\step{\pi_K(\boutact{x}{z})}_{\pi}\pi_K(Q_1)$, and $\pi_K(P)\step{\pi_K(\inact{x}{z})}_{\pi}\pi_K(Q_2)$. Hence we have  $\pi_K(P)\step{\pi_K(\tauact)}_{\pi}\pi_K(\restr{z}{(Q_1\parc Q_2)}\parc \repl{P})$.

* If the transition is $P\step{\piact}_{\pi} Q$, and $P\aeq P_1$, then $P_1\step{\piact}_{\pi} Q$. By induction hypothesis $\pi_K(P_1)\step{\pi_K(\piact)}_{\pi} \pi_K(Q)$. Moreover, using the statement $\pi_K(P)\aeq P$, we have $\pi_K(P)\aeq P\aeq P_1\aeq\pi_K(P_1)$. Hence, we have $\pi_K(P)\step{\pi_K(\piact)}_{\pi}\pi_K(Q)$.

Using the induction on the depth of the proof tree of the transition, we have shown that for every transition $P\step{\piact}_{\pi}Q$, we have $\pi_K(P)\step{\pi_K(\piact)}_{\pi}\pi_K(Q)$. We conclude that $K$ is a support of $\step{}_{\pi}$. Therefore, the transition system $\T(P)$ is an effective legal transition system with atoms.

As a consequence of Theorem <ref>, for every $\pi$-calculus process $P$, the transition system $\T(P)$ is nominally executable.

§ MCRL2

*Proof of Corollary <ref>

Consider the following mCRL2 specification:

\begin{eqnarray*}
&&\mathit{act\, num:\, Nat};\\
&&\mathit{init\,sum\, v:\, Nat\, .\, num(2 * v)};
\end{eqnarray*}

It defines a transition system that includes a set of transitions from the initial state labelled by all even natural numbers as follows:

\begin{equation*}
\{(\uparrow,2n,\downarrow)\mid n\in\mathbb{N}\}
\enskip.
\end{equation*}

This transition system does not have a finite support, therefore, it is not nominally executable.