Related publications: [DKTT13, DKTT14, DHK13, BK15]
Deoxyribonucleic acid (DNA) is most commonly known as the material that makes up the genetic code. Nowadays, DNA can be bought cheaply in a made-to-order fashion. The purified DNA strands are delivered within days after the order is made. Two complementary strands of DNA form, when mixed in solution, the well-known helix shape.
This case study considers a so-called DNA walker, which is a man-made molecular motor. The walker moves over a track of anchorages, which are strands of DNA tethered to a surface. Different types of stepping mechanisms and walkers have been published. For an overview, see the publications on molecular motors below and the references therein. An artificial molecular motor mimics the functionality of naturally occurring proteins such as kinesin or dynein. Within a cell, such proteins transport cargo over microtubials, which span across the cell.We focus on the ability of DNA walker systems to perform computation by evaluating deterministic Boolean functions, which we call DNA walker circuits. We develop a PRISM model of DNA walker circuits based on experimental data. Probabilistic model checking is then used to analyse the reliability and performance of a number of circuits. For full details, see [DKTT13, DKTT14]. The case study also makes use of the implementation of fast adaptive uniformisation [MWDH10] described in [DHK13], in addition to standard uniformisation [Jen53] and simulation-based model checking [HLMP04].
Following on from this work, we also develop a Stochastic Petri Net model of the same DNA walker circuit. We use statistical model checking implemented in Cosmos [BBDHP15] to analyse a number of properties. For further details see [BK15].
The walker under consideration here was demonstrated to work in the following papers:
In the PRISM model, each transition corresponds to a single step taken by the walker. In reality, the single step has multiple phases. The stepping mechanism works as follows:
In the model, two sources of error affect the walker. Firstly, the walker can jump to anchorages that are not directly adjacent. This can cause the walker to change direction, and eventually the walker could end up without any intact anchoraches in reach. In this case the walker is deadlocked, as it can no longer move. Deadlock is unfavourable from a computational point of view, as we cannot distinguish between an ongoing DNA walker computation and one that is deadlocked. A second mode of error occurs in the blockade mechanism. Before the walker steps, we assume each blocked anchorage has a fixed and uniform probability to fail. When a blocked anchorage fails, it becomes unblocked, and the walker may step onto it. This can delay the walker, divert it to an unintended anchorage, or cause it to deadlock.
We provide PRISM models for four DNA walker circuits, which can be found here. Three of the circuits are based on designs used in experiments, the fourth circuit is an XOR circuit that is developed separately.
The stepping behaviour of the walker is modelled using rate constants (b) that were estimated by Wickham et al. based on measurements on a straight track, which we call the control circuit (d). The predictions from the PRISM model match the measurements from the control circuit well, and we use these rate constants without further fitting. We do, however, fit a failure rate for blockades using single-junction tracks. The second circuit is the single-junction circuit, which we use to fit the failure rate for the blocked anchorages. The third circuit is the double-junction circuit, which is used to assess the quality of the model. For more details on the modelling we refer to [DKTT13, DKTT14].
The control circuit (d) consists of 8 anchorages in a straight line, with the walker starting at one end and an absorbing anchorage placed at the end. There are three variations to the basic circuit. In the first, anchorage 4 is omitted. In the second, anchorages 4 and 5 are omitted. In the third, anchorage 7 is omitted.
The second circuit (a) is a single-junction circuit, which consists of 12 anchorages and comes in three variants. In the R-variant, there is a single anchorage blocked on the left branch. The R-squared variant has two anchorages blocked on the left branch, while the L/R variant has a single blockade on both branches of the junction.
The third circuit (c) is a double-junction circuit, which consists of 28 anchorages, where, on each branch of the junction, two blocked anchorages occur. For this circuit, there are 4 variants, each corresponding to the possible inputs: RR, RL, LR and LL. For the input RR, the blockades corresponding to R and R' unblock, causing the walker to move right at the first and second junction, and so on for the other inputs.
For all circuits we compute the expected number of steps and the probability for the walker to deadlock. All properties are evaluated at T=200 min. For the control circuit, we also compute the probability for the walker to be on the second anchorage and the probability for it to be on the final absorbing anchorage.
// Probability for the walker to deadlock at T=200 min P=? [ F[200*60,200*60] "deadlock" ] // Expected number of step for the walker at T=200 min R{"steps"}=? [ C<=200*60 ] // Probability for the walker to be on the second anchorage P=? [ F[12000,12000] (w1=2) ] // Probability for the walker to be on the final anchorage P=? [ F[12000,12000] (w1=8) ]
For the single-junction and double-junction circuits, we compute the probability for the walker to make it to any absorbing anchorage and the probability for the walker to make it to the intended anchorage. For the double-junction circuit this property can be expressed as:
// Probability for the walker to make it onto any anchorage P = ? [F[200*60,200*60] (w1=17)|(w1=20)|(w1=25)|(w1=28) ] // Probability to make it to the intended anchorage for input LL P = ? [F[200*60,200*60] (w1=17) ] // Probability to make it to the intended anchorage for input RL P = ? [F[200*60,200*60] (w1=20) ] // Probability to make it to the intended anchorage for input LR P = ? [F[200*60,200*60] (w1=25) ] // Probability to make it to the intended anchorage for input RR P = ? [F[200*60,200*60] (w1=28) ]
This case study uses three solution methods implemented in PRISM, see PRISM manual. For the control circuit, we use standard uniformisation with the default hybrid engine settings. For the single-junction circuit, we use the fast adaptive uniformisation method with the parameters faudelta=1E-10 and fauepsilon=1E-8. For the double-junction circuit, we use simulation-based model checking, which estimates the value of the probability by generating 10^5 paths with depth of at most 50.
The solution method is chosen based on the sizes of the state spaces for each circuit. For the control circuit, the state space does not exceed 200 states and standard uniformisation is efficient and accurate. The single-junction circuit also has a small state space, no greater than 6,000 states, but the high initial rate used to model blockade failure makes the fast adaptive uniformisation method the preferred option here. The states with high exit rates are eventually discarded from the significant state space by the fast adaptive uniformisation method. As a result, fewer iterations are required compared to the standard uniformisation method. Note that the control track uses no blockades, and does not have high initial rates. The number of states that the fast adaptive uniformisation method keeps in memory for the single-junction is about half the reachable state space, and the method attains a good level of accuracy.
For the double-junction circuit, the size of the state space is larger, and the hybrid engine fails to build the model even after increasing the default memory allocation by an order of magnitude. For this circuit, simulation-based verification yields a good approximation after checking 10^5 paths against each property, which takes 27 seconds. For simulation-based model checking, we may construct a confidence interval to inspect the quality of the result. For the probability of the walker making it to any absorbing anchorage, PRISM reports the 95% interval to be 0.90224 +/- 0.00184, and we are confident that the true value of the property is indeed close to 0.90224. On a technical level, we note that this interval is not guaranteed to contain the true value of the property. At the chosen confidence level, we expect that, with a rate of one in twenty, the constructed intervals do not contain the true value of the property. We now try the fast adaptive uniformisation method on the double-junction circuit. Using faudelta=1E-8, the method explores 312,124 states within 40 seconds, but loses almost 2% of the probability space. Using faudelta=1E-9, the method explores 616,805 states in 94 seconds, and loses just over 0.4% in probability mass. When we set -faudelta=1E-10, the method explores 1,271,840 states and loses 0.11% probability mass.
The results are summarised below.
| Model | Filename | Time (s) | States | F2 | F8 | Deadlock | Steps | |
| Control - full track | control | 1.6 | 172 | 0.00262 | 0.96183 | 0.00322 | 6.87551 | |
| Control - no S4 | controlMissing1 | 1.6 | 50 | 0.00677 | 0.85281 | 0.00023 | 5.51422 | |
| Control - no S4,5 | controlMissing2 | 1.6 | 13 | 0.01941 | 0.59170 | 0.01941 | 3.85504 | |
| Control - no S7 | controlMissing7 | 1.6 | 82 | 0.00541 | 0.17510 | 0.03059 | 5.14486 |
| Model | Filename | Time (s) | States | Finish | Finish-correct | Deadlock | Steps | Lost | |
| Single-junction R | track12Block1 | 2.0 | 2714 | 0.97090 | 0.75933 | 0.00084 | 7.05668 | 8.81E-7 | |
| Single-junction R^2 | track12Block2 | 3.2 | 2659 | 0.95913 | 0.81370 | 0.00158 | 7.05668 | 9.27E-7 | |
| Single-junction L | track12BlockBoth | 3.1 | 2608 | 0.92037 | 0.46019 | 0.00063 | 6.56451 | 9.61E-7 |
| Model | Filename | Time (s) | States | Finished | Finished-correct | Deadlock | Steps | |
| Double-junction RR | track28LLDouble | 25.3 | - | 0.90224 | 0.69529 | 0.01105 | 11.739 | |
| Double-junction RL | track28LRDouble | 24.7 | - | 0.88959 | 0.65805 | 0.01645 | 11.775 | |
| Double-junction LR | track28RLDouble | 24.8 | - | 0.89150 | 0.65730 | 0.01675 | 11.776 | |
| Double-junction LL | track28RRDouble | 24.9 | - | 0.90161 | 0.69661 | 0.01013 | 11.742 |
The XOR circuit evaluates the exclusive OR of inputs X,Y. Two end nodes represent the TRUE and FALSE evaluation. By adding the input X, ¬Y, the path labelled correspondingly is opened up, and the walker reaches the value TRUE. Two variations on the circuit are included in the case study: a larger version of the circuit and a version that uses single blockades instead of double blockades.
The PRISM model for the xor(X,Y) circuit can be found below. It was automatically generated by pre-processing software that translates a circuit description into a PRISM model. The anchorages are represented by the variables "stator", and the location of the walker is stored in variable "w1". The rates depend mainly on the distance between the walker and the anchorage. For details see [DKTT13].
ctmc const double failureRate; module walker stator1 : [0..1] init 1; stator2 : [0..1] init 1; stator3 : [0..1] init 1; stator4 : [0..1] init 1; stator5 : [0..1] init 1; stator6 : [0..1] init 0; stator7 : [0..1] init 0; stator8 : [0..1] init 0; stator9 : [0..1] init 0; stator10 : [0..1] init 0; stator11 : [0..1] init 0; stator12 : [0..1] init 0; stator13 : [0..1] init 0; stator14 : [0..1] init 1; stator15 : [0..1] init 1; stator16 : [0..1] init 0; stator17 : [0..1] init 0; stator18 : [0..1] init 0; stator19 : [0..1] init 0; stator20 : [0..1] init 0; stator21 : [0..1] init 0; w1 : [0..21] init 1; // w1=0 is sinkstat for deadlocks blockade2: [0..1] init 0; blockade3 : [0..1] init 0; blockade4 : [0..1] init 0; blockade5 : [0..1] init 0; blockade14 : [0..1] init 0; blockade15 : [0..1] init 0; [block2] blockade2=0 -> 1000000.0 * failureRate : (blockade2'=1) & (stator2'=0) + 1000000.0 * (1.0 - failureRate ) : (blockade2'=1); [block3] blockade3=0 -> 1000000.0 * failureRate : (blockade3'=1) & (stator3'=0) + 1000000.0 * (1.0 - failureRate ) : (blockade3'=1); [block4] blockade4=0 -> 1000000.0 * failureRate : (blockade4'=1) & (stator4'=0) + 1000000.0 * (1.0 - failureRate ) : (blockade4'=1); [block5] blockade5=0 -> 1000000.0 * failureRate : (blockade5'=1) & (stator5'=0) + 1000000.0 * (1.0 - failureRate ) : (blockade5'=1); [block14] blockade14=0 -> 1000000.0 * failureRate : (blockade14'=1) & (stator14'=0) + 1000000.0 * (1.0 - failureRate ) : (blockade14'=1); [block15] blockade15=0 -> 1000000.0 * failureRate : (blockade15'=1) & (stator15'=0) + 1000000.0 * (1.0 - failureRate ) : (blockade15'=1); [step] w1=1 & stator2=0 -> 0.0029999999999999996 : (w1'=2) & (stator2'=1); [step] w1=1 & stator3=0 -> 5.9999999999999995E-5 : (w1'=3) & (stator3'=1); [step] w1=1 & stator4=0 -> 2.9999999999999997E-5 : (w1'=4) & (stator4'=1); [step] w1=1 & stator5=0 -> 5.9999999999999995E-5 : (w1'=5) & (stator5'=1); [step] w1=1 & stator6=0 -> 2.9999999999999997E-5 : (w1'=6) & (stator6'=1); [step] w1=1 & stator7=0 -> 5.999999999999999E-6 : (w1'=7) & (stator7'=1); [step] w1=1 & stator8=0 -> 2.9999999999999997E-5 : (w1'=8) & (stator8'=1); [step] w1=1 & stator9=0 -> 2.9999999999999997E-5 : (w1'=9) & (stator9'=1); [step] w1=1 & stator10=0 -> 2.9999999999999997E-5 : (w1'=10) & (stator10'=1); [step] w1=1 & stator11=0 -> 2.9999999999999997E-5 : (w1'=11) & (stator11'=1); [step] w1=1 & stator12=0 -> 5.9999999999999995E-5 : (w1'=12) & (stator12'=1); [step] w1=1 & stator13=0 -> 0.0029999999999999996 : (w1'=13) & (stator13'=1); [step] w1=1 & stator14=0 -> 2.9999999999999997E-5 : (w1'=14) & (stator14'=1); [step] w1=1 & stator15=0 -> 5.9999999999999995E-5 : (w1'=15) & (stator15'=1); [step] w1=1 & stator16=0 -> 2.9999999999999997E-5 : (w1'=16) & (stator16'=1); [step] w1=1 & stator17=0 -> 5.999999999999999E-6 : (w1'=17) & (stator17'=1); [step] w1=1 & stator18=0 -> 2.9999999999999997E-5 : (w1'=18) & (stator18'=1); [step] w1=1 & stator19=0 -> 2.9999999999999997E-5 : (w1'=19) & (stator19'=1); [step] w1=1 & stator20=0 -> 2.9999999999999997E-5 : (w1'=20) & (stator20'=1); [step] w1=1 & stator21=0 -> 2.9999999999999997E-5 : (w1'=21) & (stator21'=1); [step] w1=2 & stator1=0 -> 0.009 : (w1'=1) & (stator1'=1); [step] w1=2 & stator3=0 -> 0.009 : (w1'=3) & (stator3'=1); [step] w1=2 & stator4=0 -> 1.7999999999999998E-4 : (w1'=4) & (stator4'=1); [step] w1=2 & stator5=0 -> 1.7999999999999998E-4 : (w1'=5) & (stator5'=1); [step] w1=2 & stator6=0 -> 1.7999999999999998E-4 : (w1'=6) & (stator6'=1); [step] w1=2 & stator7=0 -> 8.999999999999999E-6 : (w1'=7) & (stator7'=1); [step] w1=2 & stator8=0 -> 8.999999999999999E-5 : (w1'=8) & (stator8'=1); [step] w1=2 & stator9=0 -> 8.999999999999999E-5 : (w1'=9) & (stator9'=1); [step] w1=2 & stator10=0 -> 8.999999999999999E-5 : (w1'=10) & (stator10'=1); [step] w1=2 & stator11=0 -> 8.999999999999999E-5 : (w1'=11) & (stator11'=1); [step] w1=2 & stator12=0 -> 8.999999999999999E-5 : (w1'=12) & (stator12'=1); [step] w1=2 & stator13=0 -> 1.7999999999999998E-4 : (w1'=13) & (stator13'=1); [step] w1=2 & stator14=0 -> 8.999999999999999E-5 : (w1'=14) & (stator14'=1); [step] w1=2 & stator15=0 -> 8.999999999999999E-5 : (w1'=15) & (stator15'=1); [step] w1=2 & stator16=0 -> 8.999999999999999E-5 : (w1'=16) & (stator16'=1); [step] w1=2 & stator17=0 -> 8.999999999999999E-6 : (w1'=17) & (stator17'=1); [step] w1=2 & stator18=0 -> 1.7999999999999998E-4 : (w1'=18) & (stator18'=1); [step] w1=2 & stator19=0 -> 8.999999999999999E-5 : (w1'=19) & (stator19'=1); [step] w1=2 & stator20=0 -> 1.7999999999999998E-4 : (w1'=20) & (stator20'=1); [step] w1=2 & stator21=0 -> 1.7999999999999998E-4 : (w1'=21) & (stator21'=1); [step] w1=3 & stator1=0 -> 1.7999999999999998E-4 : (w1'=1) & (stator1'=1); [step] w1=3 & stator2=0 -> 0.009 : (w1'=2) & (stator2'=1); [step] w1=3 & stator4=0 -> 0.009 : (w1'=4) & (stator4'=1); [step] w1=3 & stator5=0 -> 1.7999999999999998E-4 : (w1'=5) & (stator5'=1); [step] w1=3 & stator6=0 -> 8.999999999999999E-5 : (w1'=6) & (stator6'=1); [step] w1=3 & stator7=0 -> 8.999999999999999E-6 : (w1'=7) & (stator7'=1); [step] w1=3 & stator8=0 -> 8.999999999999999E-5 : (w1'=8) & (stator8'=1); [step] w1=3 & stator13=0 -> 8.999999999999999E-5 : (w1'=13) & (stator13'=1); [step] w1=3 & stator17=0 -> 8.999999999999999E-6 : (w1'=17) & (stator17'=1); [step] w1=3 & stator18=0 -> 8.999999999999999E-5 : (w1'=18) & (stator18'=1); [step] w1=3 & stator19=0 -> 1.7999999999999998E-4 : (w1'=19) & (stator19'=1); [step] w1=3 & stator20=0 -> 1.7999999999999998E-4 : (w1'=20) & (stator20'=1); [step] w1=3 & stator21=0 -> 0.009 : (w1'=21) & (stator21'=1); [step] w1=4 & stator1=0 -> 8.999999999999999E-5 : (w1'=1) & (stator1'=1); [step] w1=4 & stator2=0 -> 1.7999999999999998E-4 : (w1'=2) & (stator2'=1); [step] w1=4 & stator3=0 -> 0.009 : (w1'=3) & (stator3'=1); [step] w1=4 & stator5=0 -> 0.009 : (w1'=5) & (stator5'=1); [step] w1=4 & stator6=0 -> 1.7999999999999998E-4 : (w1'=6) & (stator6'=1); [step] w1=4 & stator7=0 -> 8.999999999999999E-6 : (w1'=7) & (stator7'=1); [step] w1=4 & stator8=0 -> 8.999999999999999E-5 : (w1'=8) & (stator8'=1); [step] w1=4 & stator13=0 -> 8.999999999999999E-5 : (w1'=13) & (stator13'=1); [step] w1=4 & stator18=0 -> 8.999999999999999E-5 : (w1'=18) & (stator18'=1); [step] w1=4 & stator19=0 -> 8.999999999999999E-5 : (w1'=19) & (stator19'=1); [step] w1=4 & stator20=0 -> 1.7999999999999998E-4 : (w1'=20) & (stator20'=1); [step] w1=4 & stator21=0 -> 1.7999999999999998E-4 : (w1'=21) & (stator21'=1); [step] w1=5 & stator1=0 -> 1.7999999999999998E-4 : (w1'=1) & (stator1'=1); [step] w1=5 & stator2=0 -> 1.7999999999999998E-4 : (w1'=2) & (stator2'=1); [step] w1=5 & stator3=0 -> 1.7999999999999998E-4 : (w1'=3) & (stator3'=1); [step] w1=5 & stator4=0 -> 0.009 : (w1'=4) & (stator4'=1); [step] w1=5 & stator6=0 -> 0.009 : (w1'=6) & (stator6'=1); [step] w1=5 & stator7=0 -> 1.7999999999999997E-5 : (w1'=7) & (stator7'=1); [step] w1=5 & stator8=0 -> 8.999999999999999E-5 : (w1'=8) & (stator8'=1); [step] w1=5 & stator9=0 -> 8.999999999999999E-5 : (w1'=9) & (stator9'=1); [step] w1=5 & stator13=0 -> 8.999999999999999E-5 : (w1'=13) & (stator13'=1); [step] w1=5 & stator20=0 -> 8.999999999999999E-5 : (w1'=20) & (stator20'=1); [step] w1=5 & stator21=0 -> 8.999999999999999E-5 : (w1'=21) & (stator21'=1); [step] w1=6 & stator1=0 -> 8.999999999999999E-5 : (w1'=1) & (stator1'=1); [step] w1=6 & stator2=0 -> 1.7999999999999998E-4 : (w1'=2) & (stator2'=1); [step] w1=6 & stator3=0 -> 8.999999999999999E-5 : (w1'=3) & (stator3'=1); [step] w1=6 & stator4=0 -> 1.7999999999999998E-4 : (w1'=4) & (stator4'=1); [step] w1=6 & stator5=0 -> 0.009 : (w1'=5) & (stator5'=1); [step] w1=6 & stator7=0 -> 9.0E-4 : (w1'=7) & (stator7'=1); [step] w1=6 & stator8=0 -> 1.7999999999999998E-4 : (w1'=8) & (stator8'=1); [step] w1=6 & stator9=0 -> 8.999999999999999E-5 : (w1'=9) & (stator9'=1); [step] w1=6 & stator10=0 -> 8.999999999999999E-5 : (w1'=10) & (stator10'=1); [step] w1=6 & stator13=0 -> 8.999999999999999E-5 : (w1'=13) & (stator13'=1); [step] w1=6 & stator21=0 -> 8.999999999999999E-5 : (w1'=21) & (stator21'=1); [step] w1=8 & stator1=0 -> 8.999999999999999E-5 : (w1'=1) & (stator1'=1); [step] w1=8 & stator2=0 -> 8.999999999999999E-5 : (w1'=2) & (stator2'=1); [step] w1=8 & stator3=0 -> 8.999999999999999E-5 : (w1'=3) & (stator3'=1); [step] w1=8 & stator4=0 -> 8.999999999999999E-5 : (w1'=4) & (stator4'=1); [step] w1=8 & stator5=0 -> 8.999999999999999E-5 : (w1'=5) & (stator5'=1); [step] w1=8 & stator6=0 -> 1.7999999999999998E-4 : (w1'=6) & (stator6'=1); [step] w1=8 & stator7=0 -> 9.0E-4 : (w1'=7) & (stator7'=1); [step] w1=8 & stator9=0 -> 0.009 : (w1'=9) & (stator9'=1); [step] w1=8 & stator10=0 -> 1.7999999999999998E-4 : (w1'=10) & (stator10'=1); [step] w1=8 & stator11=0 -> 1.7999999999999998E-4 : (w1'=11) & (stator11'=1); [step] w1=8 & stator12=0 -> 8.999999999999999E-5 : (w1'=12) & (stator12'=1); [step] w1=8 & stator13=0 -> 1.7999999999999998E-4 : (w1'=13) & (stator13'=1); [step] w1=8 & stator14=0 -> 8.999999999999999E-5 : (w1'=14) & (stator14'=1); [step] w1=9 & stator1=0 -> 8.999999999999999E-5 : (w1'=1) & (stator1'=1); [step] w1=9 & stator2=0 -> 8.999999999999999E-5 : (w1'=2) & (stator2'=1); [step] w1=9 & stator5=0 -> 8.999999999999999E-5 : (w1'=5) & (stator5'=1); [step] w1=9 & stator6=0 -> 8.999999999999999E-5 : (w1'=6) & (stator6'=1); [step] w1=9 & stator7=0 -> 1.7999999999999997E-5 : (w1'=7) & (stator7'=1); [step] w1=9 & stator8=0 -> 0.009 : (w1'=8) & (stator8'=1); [step] w1=9 & stator10=0 -> 0.009 : (w1'=10) & (stator10'=1); [step] w1=9 & stator11=0 -> 1.7999999999999998E-4 : (w1'=11) & (stator11'=1); [step] w1=9 & stator12=0 -> 1.7999999999999998E-4 : (w1'=12) & (stator12'=1); [step] w1=9 & stator13=0 -> 8.999999999999999E-5 : (w1'=13) & (stator13'=1); [step] w1=9 & stator14=0 -> 8.999999999999999E-5 : (w1'=14) & (stator14'=1); [step] w1=10 & stator1=0 -> 8.999999999999999E-5 : (w1'=1) & (stator1'=1); [step] w1=10 & stator2=0 -> 8.999999999999999E-5 : (w1'=2) & (stator2'=1); [step] w1=10 & stator6=0 -> 8.999999999999999E-5 : (w1'=6) & (stator6'=1); [step] w1=10 & stator7=0 -> 8.999999999999999E-6 : (w1'=7) & (stator7'=1); [step] w1=10 & stator8=0 -> 1.7999999999999998E-4 : (w1'=8) & (stator8'=1); [step] w1=10 & stator9=0 -> 0.009 : (w1'=9) & (stator9'=1); [step] w1=10 & stator11=0 -> 0.009 : (w1'=11) & (stator11'=1); [step] w1=10 & stator12=0 -> 1.7999999999999998E-4 : (w1'=12) & (stator12'=1); [step] w1=10 & stator13=0 -> 1.7999999999999998E-4 : (w1'=13) & (stator13'=1); [step] w1=10 & stator14=0 -> 1.7999999999999998E-4 : (w1'=14) & (stator14'=1); [step] w1=10 & stator15=0 -> 8.999999999999999E-5 : (w1'=15) & (stator15'=1); [step] w1=11 & stator1=0 -> 8.999999999999999E-5 : (w1'=1) & (stator1'=1); [step] w1=11 & stator2=0 -> 8.999999999999999E-5 : (w1'=2) & (stator2'=1); [step] w1=11 & stator7=0 -> 8.999999999999999E-6 : (w1'=7) & (stator7'=1); [step] w1=11 & stator8=0 -> 1.7999999999999998E-4 : (w1'=8) & (stator8'=1); [step] w1=11 & stator9=0 -> 1.7999999999999998E-4 : (w1'=9) & (stator9'=1); [step] w1=11 & stator10=0 -> 0.009 : (w1'=10) & (stator10'=1); [step] w1=11 & stator12=0 -> 0.009 : (w1'=12) & (stator12'=1); [step] w1=11 & stator13=0 -> 1.7999999999999998E-4 : (w1'=13) & (stator13'=1); [step] w1=11 & stator14=0 -> 1.7999999999999998E-4 : (w1'=14) & (stator14'=1); [step] w1=11 & stator15=0 -> 8.999999999999999E-5 : (w1'=15) & (stator15'=1); [step] w1=11 & stator16=0 -> 8.999999999999999E-5 : (w1'=16) & (stator16'=1); [step] w1=12 & stator1=0 -> 1.7999999999999998E-4 : (w1'=1) & (stator1'=1); [step] w1=12 & stator2=0 -> 8.999999999999999E-5 : (w1'=2) & (stator2'=1); [step] w1=12 & stator7=0 -> 8.999999999999999E-6 : (w1'=7) & (stator7'=1); [step] w1=12 & stator8=0 -> 8.999999999999999E-5 : (w1'=8) & (stator8'=1); [step] w1=12 & stator9=0 -> 1.7999999999999998E-4 : (w1'=9) & (stator9'=1); [step] w1=12 & stator10=0 -> 1.7999999999999998E-4 : (w1'=10) & (stator10'=1); [step] w1=12 & stator11=0 -> 0.009 : (w1'=11) & (stator11'=1); [step] w1=12 & stator13=0 -> 0.009 : (w1'=13) & (stator13'=1); [step] w1=12 & stator14=0 -> 0.009 : (w1'=14) & (stator14'=1); [step] w1=12 & stator15=0 -> 1.7999999999999998E-4 : (w1'=15) & (stator15'=1); [step] w1=12 & stator16=0 -> 8.999999999999999E-5 : (w1'=16) & (stator16'=1); [step] w1=12 & stator17=0 -> 8.999999999999999E-6 : (w1'=17) & (stator17'=1); [step] w1=12 & stator18=0 -> 8.999999999999999E-5 : (w1'=18) & (stator18'=1); [step] w1=13 & stator1=0 -> 0.009 : (w1'=1) & (stator1'=1); [step] w1=13 & stator2=0 -> 1.7999999999999998E-4 : (w1'=2) & (stator2'=1); [step] w1=13 & stator3=0 -> 8.999999999999999E-5 : (w1'=3) & (stator3'=1); [step] w1=13 & stator4=0 -> 8.999999999999999E-5 : (w1'=4) & (stator4'=1); [step] w1=13 & stator5=0 -> 8.999999999999999E-5 : (w1'=5) & (stator5'=1); [step] w1=13 & stator6=0 -> 8.999999999999999E-5 : (w1'=6) & (stator6'=1); [step] w1=13 & stator7=0 -> 8.999999999999999E-6 : (w1'=7) & (stator7'=1); [step] w1=13 & stator8=0 -> 1.7999999999999998E-4 : (w1'=8) & (stator8'=1); [step] w1=13 & stator9=0 -> 8.999999999999999E-5 : (w1'=9) & (stator9'=1); [step] w1=13 & stator10=0 -> 1.7999999999999998E-4 : (w1'=10) & (stator10'=1); [step] w1=13 & stator11=0 -> 1.7999999999999998E-4 : (w1'=11) & (stator11'=1); [step] w1=13 & stator12=0 -> 0.009 : (w1'=12) & (stator12'=1); [step] w1=13 & stator14=0 -> 1.7999999999999998E-4 : (w1'=14) & (stator14'=1); [step] w1=13 & stator15=0 -> 1.7999999999999998E-4 : (w1'=15) & (stator15'=1); [step] w1=13 & stator16=0 -> 1.7999999999999998E-4 : (w1'=16) & (stator16'=1); [step] w1=13 & stator17=0 -> 8.999999999999999E-6 : (w1'=17) & (stator17'=1); [step] w1=13 & stator18=0 -> 8.999999999999999E-5 : (w1'=18) & (stator18'=1); [step] w1=13 & stator19=0 -> 8.999999999999999E-5 : (w1'=19) & (stator19'=1); [step] w1=13 & stator20=0 -> 8.999999999999999E-5 : (w1'=20) & (stator20'=1); [step] w1=13 & stator21=0 -> 8.999999999999999E-5 : (w1'=21) & (stator21'=1); [step] w1=14 & stator1=0 -> 8.999999999999999E-5 : (w1'=1) & (stator1'=1); [step] w1=14 & stator2=0 -> 8.999999999999999E-5 : (w1'=2) & (stator2'=1); [step] w1=14 & stator8=0 -> 8.999999999999999E-5 : (w1'=8) & (stator8'=1); [step] w1=14 & stator9=0 -> 8.999999999999999E-5 : (w1'=9) & (stator9'=1); [step] w1=14 & stator10=0 -> 1.7999999999999998E-4 : (w1'=10) & (stator10'=1); [step] w1=14 & stator11=0 -> 1.7999999999999998E-4 : (w1'=11) & (stator11'=1); [step] w1=14 & stator12=0 -> 0.009 : (w1'=12) & (stator12'=1); [step] w1=14 & stator13=0 -> 1.7999999999999998E-4 : (w1'=13) & (stator13'=1); [step] w1=14 & stator15=0 -> 0.009 : (w1'=15) & (stator15'=1); [step] w1=14 & stator16=0 -> 1.7999999999999998E-4 : (w1'=16) & (stator16'=1); [step] w1=14 & stator17=0 -> 8.999999999999999E-6 : (w1'=17) & (stator17'=1); [step] w1=14 & stator18=0 -> 8.999999999999999E-5 : (w1'=18) & (stator18'=1); [step] w1=15 & stator1=0 -> 1.7999999999999998E-4 : (w1'=1) & (stator1'=1); [step] w1=15 & stator2=0 -> 8.999999999999999E-5 : (w1'=2) & (stator2'=1); [step] w1=15 & stator10=0 -> 8.999999999999999E-5 : (w1'=10) & (stator10'=1); [step] w1=15 & stator11=0 -> 8.999999999999999E-5 : (w1'=11) & (stator11'=1); [step] w1=15 & stator12=0 -> 1.7999999999999998E-4 : (w1'=12) & (stator12'=1); [step] w1=15 & stator13=0 -> 1.7999999999999998E-4 : (w1'=13) & (stator13'=1); [step] w1=15 & stator14=0 -> 0.009 : (w1'=14) & (stator14'=1); [step] w1=15 & stator16=0 -> 0.009 : (w1'=16) & (stator16'=1); [step] w1=15 & stator17=0 -> 1.7999999999999997E-5 : (w1'=17) & (stator17'=1); [step] w1=15 & stator18=0 -> 8.999999999999999E-5 : (w1'=18) & (stator18'=1); [step] w1=15 & stator19=0 -> 8.999999999999999E-5 : (w1'=19) & (stator19'=1); [step] w1=16 & stator1=0 -> 8.999999999999999E-5 : (w1'=1) & (stator1'=1); [step] w1=16 & stator2=0 -> 8.999999999999999E-5 : (w1'=2) & (stator2'=1); [step] w1=16 & stator11=0 -> 8.999999999999999E-5 : (w1'=11) & (stator11'=1); [step] w1=16 & stator12=0 -> 8.999999999999999E-5 : (w1'=12) & (stator12'=1); [step] w1=16 & stator13=0 -> 1.7999999999999998E-4 : (w1'=13) & (stator13'=1); [step] w1=16 & stator14=0 -> 1.7999999999999998E-4 : (w1'=14) & (stator14'=1); [step] w1=16 & stator15=0 -> 0.009 : (w1'=15) & (stator15'=1); [step] w1=16 & stator17=0 -> 9.0E-4 : (w1'=17) & (stator17'=1); [step] w1=16 & stator18=0 -> 1.7999999999999998E-4 : (w1'=18) & (stator18'=1); [step] w1=16 & stator19=0 -> 8.999999999999999E-5 : (w1'=19) & (stator19'=1); [step] w1=16 & stator20=0 -> 8.999999999999999E-5 : (w1'=20) & (stator20'=1); [step] w1=18 & stator1=0 -> 8.999999999999999E-5 : (w1'=1) & (stator1'=1); [step] w1=18 & stator2=0 -> 1.7999999999999998E-4 : (w1'=2) & (stator2'=1); [step] w1=18 & stator3=0 -> 8.999999999999999E-5 : (w1'=3) & (stator3'=1); [step] w1=18 & stator4=0 -> 8.999999999999999E-5 : (w1'=4) & (stator4'=1); [step] w1=18 & stator12=0 -> 8.999999999999999E-5 : (w1'=12) & (stator12'=1); [step] w1=18 & stator13=0 -> 8.999999999999999E-5 : (w1'=13) & (stator13'=1); [step] w1=18 & stator14=0 -> 8.999999999999999E-5 : (w1'=14) & (stator14'=1); [step] w1=18 & stator15=0 -> 8.999999999999999E-5 : (w1'=15) & (stator15'=1); [step] w1=18 & stator16=0 -> 1.7999999999999998E-4 : (w1'=16) & (stator16'=1); [step] w1=18 & stator17=0 -> 9.0E-4 : (w1'=17) & (stator17'=1); [step] w1=18 & stator19=0 -> 0.009 : (w1'=19) & (stator19'=1); [step] w1=18 & stator20=0 -> 1.7999999999999998E-4 : (w1'=20) & (stator20'=1); [step] w1=18 & stator21=0 -> 1.7999999999999998E-4 : (w1'=21) & (stator21'=1); [step] w1=19 & stator1=0 -> 8.999999999999999E-5 : (w1'=1) & (stator1'=1); [step] w1=19 & stator2=0 -> 8.999999999999999E-5 : (w1'=2) & (stator2'=1); [step] w1=19 & stator3=0 -> 1.7999999999999998E-4 : (w1'=3) & (stator3'=1); [step] w1=19 & stator4=0 -> 8.999999999999999E-5 : (w1'=4) & (stator4'=1); [step] w1=19 & stator13=0 -> 8.999999999999999E-5 : (w1'=13) & (stator13'=1); [step] w1=19 & stator15=0 -> 8.999999999999999E-5 : (w1'=15) & (stator15'=1); [step] w1=19 & stator16=0 -> 8.999999999999999E-5 : (w1'=16) & (stator16'=1); [step] w1=19 & stator17=0 -> 1.7999999999999997E-5 : (w1'=17) & (stator17'=1); [step] w1=19 & stator18=0 -> 0.009 : (w1'=18) & (stator18'=1); [step] w1=19 & stator20=0 -> 0.009 : (w1'=20) & (stator20'=1); [step] w1=19 & stator21=0 -> 1.7999999999999998E-4 : (w1'=21) & (stator21'=1); [step] w1=20 & stator1=0 -> 8.999999999999999E-5 : (w1'=1) & (stator1'=1); [step] w1=20 & stator2=0 -> 1.7999999999999998E-4 : (w1'=2) & (stator2'=1); [step] w1=20 & stator3=0 -> 1.7999999999999998E-4 : (w1'=3) & (stator3'=1); [step] w1=20 & stator4=0 -> 1.7999999999999998E-4 : (w1'=4) & (stator4'=1); [step] w1=20 & stator5=0 -> 8.999999999999999E-5 : (w1'=5) & (stator5'=1); [step] w1=20 & stator13=0 -> 8.999999999999999E-5 : (w1'=13) & (stator13'=1); [step] w1=20 & stator16=0 -> 8.999999999999999E-5 : (w1'=16) & (stator16'=1); [step] w1=20 & stator17=0 -> 8.999999999999999E-6 : (w1'=17) & (stator17'=1); [step] w1=20 & stator18=0 -> 1.7999999999999998E-4 : (w1'=18) & (stator18'=1); [step] w1=20 & stator19=0 -> 0.009 : (w1'=19) & (stator19'=1); [step] w1=20 & stator21=0 -> 0.009 : (w1'=21) & (stator21'=1); [step] w1=21 & stator1=0 -> 8.999999999999999E-5 : (w1'=1) & (stator1'=1); [step] w1=21 & stator2=0 -> 1.7999999999999998E-4 : (w1'=2) & (stator2'=1); [step] w1=21 & stator3=0 -> 0.009 : (w1'=3) & (stator3'=1); [step] w1=21 & stator4=0 -> 1.7999999999999998E-4 : (w1'=4) & (stator4'=1); [step] w1=21 & stator5=0 -> 8.999999999999999E-5 : (w1'=5) & (stator5'=1); [step] w1=21 & stator6=0 -> 8.999999999999999E-5 : (w1'=6) & (stator6'=1); [step] w1=21 & stator13=0 -> 8.999999999999999E-5 : (w1'=13) & (stator13'=1); [step] w1=21 & stator17=0 -> 8.999999999999999E-6 : (w1'=17) & (stator17'=1); [step] w1=21 & stator18=0 -> 1.7999999999999998E-4 : (w1'=18) & (stator18'=1); [step] w1=21 & stator19=0 -> 1.7999999999999998E-4 : (w1'=19) & (stator19'=1); [step] w1=21 & stator20=0 -> 0.009 : (w1'=20) & (stator20'=1); [] w1=1 -> 0.000000001 : (w1'=1); [] w1=2 -> 0.000000001 : (w1'=2); [] w1=3 -> 0.000000001 : (w1'=3); [] w1=4 -> 0.000000001 : (w1'=4); [] w1=5 -> 0.000000001 : (w1'=5); [] w1=6 -> 0.000000001 : (w1'=6); [] w1=7 -> 0.000000001 : (w1'=7); [] w1=8 -> 0.000000001 : (w1'=8); [] w1=9 -> 0.000000001 : (w1'=9); [] w1=10 -> 0.000000001 : (w1'=10); [] w1=11 -> 0.000000001 : (w1'=11); [] w1=12 -> 0.000000001 : (w1'=12); [] w1=13 -> 0.000000001 : (w1'=13); [] w1=14 -> 0.000000001 : (w1'=14); [] w1=15 -> 0.000000001 : (w1'=15); [] w1=16 -> 0.000000001 : (w1'=16); [] w1=17 -> 0.000000001 : (w1'=17); [] w1=18 -> 0.000000001 : (w1'=18); [] w1=19 -> 0.000000001 : (w1'=19); [] w1=20 -> 0.000000001 : (w1'=20); [] w1=21 -> 0.000000001 : (w1'=21); endmodule rewards "steps" [step] true : 1; endrewards rewards "time" true : 1; endrewards rewards "blocked" // time spend in blocked anchorages w1 =2 | w1 =3 | w1 =4 | w1 =5 | w1 =14 | w1 =15: 1; endrewards
Files for additional models from [DKTT13] (including all of those used in [DHK13]) can be found here. The model above has 2.8 x 107 states; it can be constructed, but not analysed, with PRISM's standard engines. The largest circuit is estimated to have to up to 109 states. To analyse the DNA walker models, we use the fast adaptive uniformisation method [MWDH10], which has now been implemented in PRISM [DHK13].
The PRISM properties used to analyse the models are as follows:
// Probability that the walker makes it to the correct end node P=? [F[T,T] (w1=17) ] // The expected number of steps that the walker takes R{"steps"}=? [ C<=T ] // The expected amount of time the walker spends on anchorages that were intended to be blocked R{"blocked"}=? [ C<=T ]
The table below shows results for the walker models, obtained using the fast adaptive uniformisation method. We fixed a time point of 200 minutes (i.e. T=200*60) to allow a comparison with experimental observations. "Model" describes the type of XOR circuit and which instructions are used as input. "Filename" is the name of the model file in the zip file. "Time (s)" is the amount of time the model checker took to generate the answers. "States" is the maximum number of states that were loaded in the memory at any point during the computation. "Lost" represents the amount of probability that was unaccounted for by the end of the analysis. "Signal" is the probability that the walker makes it to the correct end node. "Steps" is the expected number of steps that the walker takes. "Blocked" is the amount of time the walker spends on anchorages that were intended to be blocked. "Steps" and "Blocked" are both calculated using reward properties. The fast adaptive uniformisation method was used with parameters delta=10-8 and epsilon=10-6.
| Model | Filename | Time (s) | States | Lost | Signal | Steps | Blocked (s) | |
| xor(X,Y) | ringLL | 31 | 228,803 | 1.9736E-02 | 0.6455 | 7.7696 | 606.2731 | |
| xor(¬X,Y) | ringRL | 31 | 228,803 | 1.9736E-02 | 0.6455 | 7.7696 | 606.2731 | |
| xor(X,¬Y) | ringLR | 32 | 239,680 | 2.2587E-02 | 0.5979 | 7.5610 | 659.3715 | |
| xor(¬X,¬Y) | ringRR | 33 | 239,680 | 2.2587E-02 | 0.5979 | 7.5610 | 659.3715 | |
| xor-S-(X,Y) | ringSLL | 21 | 215,544 | 1.6719E-02 | 0.5374 | 8.8363 | 133.1672 | |
| xor-S-(¬X,Y) | ringSRL | 21 | 215,544 | 1.6719E-02 | 0.5374 | 8.8363 | 133.1672 | |
| xor-S-(X,¬Y) | ringSLR | 22 | 233,063 | 1.8775E-02 | 0.5473 | 8.4049 | 146.7377 | |
| xor-S-(¬X,¬Y) | ringSRR | 23 | 233,063 | 1.8775E-02 | 0.5473 | 8.4049 | 146.7377 | |
| xor-large-(X,Y) | ringLLL | 65 | 443,584 | 5.1855E-02 | 0.5661 | 9.5020 | 577.2680 | |
| xor-large-(¬X,Y) | ringLRL | 68 | 443,584 | 5.1855E-02 | 0.5661 | 9.5020 | 577.2680 | |
| xor-large-(X,¬Y) | ringLLR | 66 | 455,685 | 5.2995E-02 | 0.5674 | 9.4983 | 567.3420 | |
| xor-large-(¬X,¬Y) | ringLRR | 70 | 455,685 | 5.2995E-02 | 0.5674 | 9.4983 | 567.3420 |
Even though the reachable state space is large, the number of states that are in memory concurrently is tractable. The amount of probability unaccounted for ("Lost") is very high. The expected number of steps increases when fewer blockades are in place (modification S), and equally so for the larger circuit. When fewer blockades are used, the amount of time spend on blocked positions ("Blocked") decreases accordingly. The walker can only step onto blocked positions after a blockade fails. The failure rate used here is 30%.
Since DNA walker circuits are planar, Generalized Stochastic Petri Nets (GSPN) are well suited to their modelling, with the layout of the GSPNs closely corresponding to the layout of the original circuit: the state of each anchorage is modelled using an independent place, while the steps of the walker are modelled with transitions that are exponentially distributed. This approach is presented in [BK15].
More precisely, each DNA walker circuit comprises several tracks (sequences of anchorages) and transitions correspond to walker taking a step from one anchorage to another nearby. The states of each anchorage are modelled as follows:
The figure below illustrates a transition encoding a displacement reaction between two anchorages a and b. Place a encodes the anchorage to which the walker is currently bound. Place b encodes an intact, unblocked anchorage. The transition consumes two tokens in the place corresponding to a and one token in the place corresponding to b, and produces two tokens in the place corresponding to b. Indeed, after the transition is fired the place corresponding to a is left empty, which models the anchorage where the top has melted away.
The walker may move between two anchorages that are sufficiently
close. Each such movement is modelled with independent
transitions. The rate of each transition depends on the distance
between the two anchorages as specified in
Modelling the stepping mechanism
Blocked anchorages do not initially contain tokens. In order to model the possibility of failure of the blocking mechanism, a place with initially one token and two immediate concurrent transitions are added to each blocked anchorage. This is illustrated below. With failure probability f=30%, a token is added to the place for anchorage a. In this case the anchorage is no longer blocked.
We consider four circuit layouts depicted below. Files for each layout can be found here (zip file) in PNML file format, GrML file format, and ANDL file format(Marcie). A PDF representation is also provided.
The probability of presence of the walker in each leaf node of the double junction circuits over time as computed by Cosmos is plotted next.
Experiments comparing three PRISM verification methods (statistical model checking, standard uniformisation and fast adaptive uniformisation) with the statistical model checker Cosmos are reported in table below.
| Model | Cosmos 8 Threads | Cosmos 1 Threads | Prism Sim | Prism | Prism Fau | |||
| Time(s) | Time(s) | Time(s) | Time(s) | Memory(KB) | Time(s) | Memory(MB) | ||
| ex | 0.2 | 0.6 | 2.4 | 0 | 0.5 | 0.06 | 77.58 | |
| control | 2.4 | 11.1 | 29.4 | 0.04 | 40.2 | 1 | 127.18 | |
| controlMissing1 | 1.5 | 6.8 | 18.9 | 0.01 | 7.8 | 0.9 | 98.82 | |
| controlMissing2 | 0.8 | 3.6 | 11.2 | 0 | 7.3 | 0.09 | 81.58 | |
| controlMissing7 | 1.9 | 8.6 | 22.6 | 0.02 | 26 | 0.92 | 113.76 | |
| track12Block1 | 4.7 | 22.4 | 68 | >20H | 388.3 | 3.95 | 245.11 | |
| track12Block2 | 4.7 | 22.2 | 76.4 | - | 530.8 | 4.84 | 296.03 | |
| track12BlockBoth | 4.4 | 20.8 | 71.9 | - | 509.4 | 4.76 | 279.55 | |
| track28LL | 10.6 | 51.5 | 395.5 | >8GB | 879.35 | 1,042.62 | ||
| track28LR | 11.1 | 53.3 | 393.8 | - | 927.59 | 1,061.37 | ||
| track28RL | 11.2 | 54.4 | 382 | - | 929.39 | 1,076.57 | ||
| track28RR | 10.6 | 52.2 | 393.3 | - | 870.48 | 1,047.32 | ||
| ringLL | 10.9 | 53.7 | 360 | >20H | 717,312 | 748.83 | 1,139.35 | |
| ringRL | 11.1 | 55 | 339.1 | - | 717,312 | 755.69 | 1,131.96 | |
| ringLR | 11 | 54.9 | 348.3 | - | 717,312 | 754.01 | 1,164.21 | |
| ringRR | 10.9 | 53.4 | 346.3 | - | 717,312 | 757.72 | 1,154.43 | |
| ringLLLarge | 12.7 | 62.7 | 423.7 | - | 1,864.83 | 2,206.84 | ||
| ringRLLarge | 12.9 | 63.7 | 471.7 | - | 1,802.69 | 2,201.96 | ||
| ringLRLarge | 13 | 64.1 | 442 | - | 1,994.9 | 2,206.27 | ||
| ringRRLarge | 12.7 | 62.2 | 555.2 | - | 2,056.98 | 2,211.3 | ||
| redundantChoice10 | 27.1 | 131.8 | 1,258.2 | >8GB | >8GB | |||
| redundantChoice01 | 26.6 | 128.9 | 1,239.8 | - | - | |||
| lozenge | 480.6 | 1,656.6 | 22,302.6 | - | ||||
| lozengeBlock | 241.7 | 827.8 | 32,293.2 | - | ||||