1 Introduction
1.1 Contributions
1.2 Outline
2 Modelling
2.1 DNA walker systems
-
V is the set of vertices, with\(V= V_{{ INIT}} \cup V_{{ NORM}} \cup V_{{ FORK}} \cup V_{{ JOIN}} \cup V_{{ FINAL}}\), andand all vertex sets pairwise disjunctive.
-
\(V_{{ INIT}} = \{v_0\}\)—the unique initial anchorage,
-
\(V_{{ NORM}}\)—the vertex set of normal anchorages,
-
\(V_{{ FORK}}\)—the vertex set of fork anchorages,
-
\(V_{{ JOIN}}\)—the vertex set of join anchorages,
-
\(V_{{ FINAL}}\)—the vertex set of final anchorages,
-
-
E is the set of undirected edges with \(E \subset \left( V \times V\right) \). The initial vertex \(v_0\) and final vertices have one adjacent edge, normal vertices have two adjacent edges, and junction vertices (either fork or join) have three adjacent edges.
-
\({ In}\) is a set of Boolean variables, and \({ literals}(In)\) yields the set of all value assignments over In.
-
L is a labelling function with \(L{:} V {\setminus } V_{{ FINAL}} \rightarrow { literals}(In) \cup \{\epsilon \}\).
-
\({ Out}\) is an output function with \({ Out}: V_{{ FINAL}} \rightarrow \{T,F\}\), assigning a truth value to each final vertex. □
-
All undirected edges have exactly one direction which corresponds to a step directed from the init vertex to one of the final vertices.
-
By definition, the walker can never leave a final node; however this cannot be deduced from the undirected graph.
-
Binary decision trees do not require join anchorages.
-
There has to be at least one final vertex. Usually the graph will contain at least two final vertices, with each truth value occurring at least once.
-
DSD graphs with exactly one final vertex labelled with true allow for composability, e.g., exploiting origami tiles.
-
The empty label \(\epsilon \) permits unblockable anchorages and is typically not displayed. The unique initial anchorage \(v_0\) should be labelled with \(\epsilon \).
-
The definition given in Dannenberg (2016) does not distinguish between fork and join, and it assigns \({ literals}(in)\) to edges; we assign them to vertices.
2.2 Petri nets
-
P and T are finite, non-empty, and disjoint sets. P is the set of places, and T is the set of transitions.
-
\(f:\left( (P\times T\right) \cup \left( T\times P\right) )\rightarrow N_0\) defines the set of directed arcs, weighted by non-negative integer values.
-
\(m_0:P\rightarrow N_0\) gives the initial marking. □
-
A transition t is enabled in a marking m, written as \(m[t\rangle \), if \(\forall p \in {\scriptstyle ^\bullet } t: m(p) \ge f(p,t)\), else disabled.
-
A transition t, which is enabled in m, may fire.
-
When t in m fires, a new marking \(m'\) is reached, written as \({m} {\xrightarrow {\text {t}}} {m'}\), with$$\begin{aligned} \forall p \in P : m'(p) = m(p) - f(p,t) + f(t,p). \end{aligned}$$
-
The firing happens atomically. □
-
Unguided scenario: one token is removed from A, because the walker leaves A, and one token is kept, because A can be re-visited,
-
“Burnt-bridges” scenario: two tokens are removed from A, because the walker leaves A, and A can not be re-visited.
2.2.1 Stepping distance
2.2.2 Fault model
2.3 Coloured Petri nets
2.3.1 Encoding the vertices
2.3.2 Distance metrics
2.3.3 Encoding the walker steps
2.3.4 Blocking of anchorages and fault model
2.3.5 Comparing both Petri net modelling approaches
3 Identification of leakage transitions
3.1 Place indexing
-
The unique place of type INIT has to have exactly one successor by definition. The successor of INIT gets the same index, i.e.,1, and the successor is added to the queue. The transition from INIT to its successor is part of a (linear) track, thus we add a tuple of (\({1,1,{ TRACK}}\)) to the known transition types.
-
For binary forward branching, a node c of type FORK has 3 short distance neighbours, one corresponds to the predecessor and the others to the two branches the computational path may take. The first of the two successors \({c}^{\circ }_0\) gets an index that is two times the index of c. Then \({c}^{\circ }_0\) is added to the queue. The second successor \({c}^{\circ }_1\) gets an index that is two times the index of c plus one. Then \({c}^{\circ }_1\) is added to the queue. The transitions from c to its successors are FORK transitions, so we add two triples (c, \({c}^{\circ }_i\), FORK) to the known transition types.
-
Binary backward branching takes place on a node c of type JOIN and as such c has 3 short distance neighbours, two predecessors and one successor. When the algorithm reaches c, it may happen that two of the neighbours are not indexed yet. In this case we are not able to decide which one is the predecessor and which one is the successor, so we postpone that decision and treat both places as if they each would be a successor. The successor gets the same index as c and is added to the queue. The transitions between c and its successor are of type TRACK, i.e.,the tuple of both indices and type TRACK is added to the known transition types.
-
A node of type NORM in a linear track has exactly two short distance neighbours, one corresponds to the predecessor, and one to the successor node. But there are several cases to deal with.In each of the previous cases, the transition between c and its successor is of type JOIN or TRACK, i.e., a triple of both indices and type JOIN or TRACK is added to the known transition types.1.The successor is not indexed yet and is of type JOIN. So it gets an index two times of c, and the transition must be of type JOIN too. The successor is added to the queue.2.The successor is not indexed yet and is not of type JOIN. So it gets the same index as c, because it is on the same track. Thus the transition is of type TRACK. The successor is added to the queue.3.The index of the successor is smaller than the index of c and the successor is of type JOIN. So we have reached an already visited backward branch and add the tuple of indices and type JOIN to the known transition types.4.The index of the successor is smaller than the index of c and the successor is not of type JOIN. So we override the successor’s index and add it to the queue, because we are backtracking to a previously visited track.A normal node may have 3 short distance neighbours in the case of leak transitions. In this situation we have to take care of several cases.In the first four cases, the transitions between c and its successor are of type JOIN or TRACK, i.e., tuples of both indices and type JOIN or TRACK are added to the known transition types.1.The successor is not indexed yet and is of type JOIN, so it gets an index two times of c and the transitions must be of type JOIN too, the successor is added to the queue and is additionally marked.2.The successor is not indexed yet and is not of type JOIN, so it gets the same index as c, because they are on the same track. Thus the transitions are of type TRACK and the successor is added to the queue and is additionally marked.3.The successor is marked and is of type JOIN, so we have reached an already visited backward branch and add a tuple of the indices and type JOIN to the known transition types.4.The successor is marked and is not of type JOIN, so we overwrite the successor’s index, if it is smaller, because we reached a corner with shortcut transitions.5.The successor is not marked; thus the transition must be a leak transition. The transitions from c to its successors are LEAK transitions, so we add two triples (c, \({c}^{\circ }_i\), LEAK) to the known transition types.
-
A node of type FINAL has only one short distance neighbour, which is then a predecessor, so there are no more nodes to investigate.
3.2 Transition classification
-
The pre-place and post-place of a TRACK transition t have the same index, forming a linear track, i.e.,\({ index}({t}^{\bullet }) = { index}({}^{\bullet }t)\).
-
For the indices of the pre- and post-place of a FORK transition t, it holds either \({ index}({t}^{\bullet }) = 2\cdot { index}({}^{\bullet }t)\) or \({ index}({t}^{\bullet }) = 2\cdot { index}({}^{\bullet }t) + 1\).
-
For the indices of the pre- and post-place of a JOIN transition t, it holds either \({ index}({t}^{\bullet }) = 2\cdot { index}({}^{\bullet }t)\) or \({ index}({t}^{\bullet }) < { index}({}^{\bullet }t)\).
-
There is one precisely defined case of LEAK transitions—a leak that follows directly after a fork. Thus, any transition satisfying \({ index}({t}^{\bullet }) = { index}({}^{\bullet }t) + 1\) or \({ index}({}^{\bullet }t) = { index}({t}^{\bullet }) - 1\) is a LEAK transition. However, depending on the layout, a leak can occur anywhere between two places having different indices.
3.3 Case study
Short | Medium | Long |
\(\varSigma \)
| |
---|---|---|---|---|
Track | 64 | 51 | 51 | 166 |
Fork | 12 | 30 | 54 | 96 |
Join | 8 | 17 | 33 | 58 |
Leak | 8 | 36 | 98 | 142 |
Short | Medium | Long |
\(\varSigma \)
| |
---|---|---|---|---|
Track | 66 | 57 | 57 | 180 |
Fork | 12 | 34 | 62 | 108 |
Join | 8 | 20 | 30 | 58 |
Leak | 2 | 20 | 58 | 80 |
3.4 Implementation
4 Analysis techniques
4.1 Qualitative analysis
-
\(V_{{\mathcal {N}}} := [m_0 \rangle \) is the set of nodes,
-
\(E_{{\mathcal {N}}} := \{\, (m, t, m') \mid m, m' \in [m_0 \rangle , t \in T: {m} {\xrightarrow {\text {t}} }{m'} \}\) is the set of arcs. □
-
A Petri net is k-bounded iff there is no node in the reachability graph with a token number larger than k in any place.
-
A Petri net is reversible iff the reachability graph is strongly connected.
-
A Petri net is free of dead states iff the reachability graph does not contain terminal nodes, i.e., nodes without outgoing arcs.
-
In order to decide liveness, the reachability graph has to be partitioned into strongly connected components (SCC), i.e., maximal sets of strongly connected nodes. A SCC is called terminal if no other SCC is reachable in the partitioned graph. A transition is live iff it is included in all terminal SCCs of the partitioned reachability graph. A Petri net is live iff this holds for all transitions.
-
2-bounded: an anchorage can be unblocked (1 token), and host the walker (1 token) at the same time; no more moving tokens do exist;
-
not reversible: which is an immediate consequence of the “burnt-bridges” scenario, causing acyclic reachability graphs;
-
generally, not free of dead states: a walker can be trapped in a non-final vertex without any neighbouring vertex free to be visited;
-
not live: while all transition can occur once in some behaviour, none of them will ever have a chance to fire twice in the “burnt-bridges” scenario.
4.2 Stochastic analysis
4.2.1 Transient analysis
FINAL
anchorages at time point \(\tau \).CORRECT
FINAL
anchorage according to its input values at time point \(\tau \).DEADLOCK
describes the set of dead states.CONDITION
of the walker to have reached the CORRECT
FINAL
anchorage according to its input values given that it has reached any of the FINAL
anchorages at time point \(\tau \).4.2.2 Reward analysis
4.2.3 Performability analysis
4.2.4 Case study
Short | Medium | Long |
\(\varSigma \)
| |
---|---|---|---|---|
Track | 9.897 | 0.282 | 0.202 | 10.354 |
Fork | 1.694 | 0.163 | 0.172 | 2.029 |
Join | 1.208 | 0.139 | 0.168 | 1.515 |
Leak | 0.483 | 0.189 | 0.311 | 0.983 |
Short | Medium | Long |
\(\varSigma \)
| |
---|---|---|---|---|
Track | 10.693 | 0.354 | 0.253 | 11.300 |
Fork | 1.669 | 0.183 | 0.206 | 2.058 |
Join | 1.286 | 0.170 | 0.170 | 1.626 |
Leak | 0.114 | 0.135 | 0.195 | 0.444 |
4.2.5 Design trade-off
-
Objective 1: reduce number of leakage transitions (as more leakage transitions increase the probability of getting the wrong result).
-
Objective 2: reduce length of tracks (as longer tracks increase the deadlock probability).