Soft Computing https://doi.org/10.1007/s00500-018-3314-7
FOUNDATIONS
Performing CTL model checking via DNA computing Weijun Zhu1 · Yingjie Han1 · Qinglei Zhou1
© Springer-Verlag GmbH Germany, part of Springer Nature 2018
Abstract The computation using deoxyribonucleic acid (DNA) molecules provides an enormous parallel method that breaks through the limitations of the efficiency of traditional electronic computers. Model checking is a standard formal verification technique, which has been widely used in many fields of computation. It is also a well-known complex problem in computing theory. Until now, there is only one basic formula in the computation tree logic (CTL), for which model checking via DNA computing can be conducted. To this end, Adleman’s model based on DNA computing is used in this paper, based on which a series of DNA-computing-based model-checking algorithms to check the four basic CTL formulas are proposed. As a result, a core of the DNA version of the CTL model-checking problem is solved. The simulated experimental results show that the new algorithms are valid and can be properly implemented in molecular biology. Keywords DNA computing · Model checking · Computation tree logic · DNA molecules
1 Introduction Model checking (MC) was proposed by Turing Award winner Prof. Clarke and his collaborators (Edmund et al. 1999). The MC algorithms automatically answer the question whether a system satisfies a given property. MC is widely used in the fields of hardware verification (Edmund et al. 1999), data flow analysis (Li et al. 2015a), network protocol verification, security protocol verification (Roberto 2011), software verification (Andreas et al. 2013) and biological systems (Brim et al. 2013). Its general principle is formulated as follows. A system model is constructed with an automaton, and a temporal formula represents a property that the system should satisfy. If the automaton is a model of the formula, the system model satisfies the property. Otherwise, the system does not satisfy the property. Turing Award winner Prof. Pnueli’s Linear Temporal Logic (LTL) (Pnueli 1977) and Turing Award winner Prof. Emerson and Clarke’s Computation Tree Logic (CTL) (Emerson and Edmund 1982) are the two most popular temporal logics that can describe the linear and branch temporal properties, respectively. Communicated by A. Di Nola.
B 1
Weijun Zhu
[email protected] School of Information Engineering, Zhengzhou University, Zhengzhou 450001, China
CTL model checking is always one of the research hotspots. On one hand, CTL has been extended to express the stronger properties. For example, Prof. Li Yongming extended CTL to PoCTL and GPoCTL to describe the possibilistic branch-time temporal properties and provided their model-checking algorithms (Li and Ma 2015; Li et al. 2015b). Similarly, the LTL model checking can be extended to its possibilistic version (Li 2017). On the other hand, some techniques have been proposed to enhance the efficiency of CTL model checking. One example is the CTL model-checking algorithm based on the forward state traversal, which reduces the CPU time and memory consumption (Iwashita et al. 1997). The on-the-fly technique will also alleviate the well-known state space explosion problem (Bhat et al. 2002). Furthermore, in the current era of big data and cloud computing, a framework with MapReduce as the core computational model has significantly eased the adoption of a distributed approach to the verification of CTL formulas in large state spaces (Camilli et al. 2015). Thus, many studies have been conducted on CTL model checking. We do not detail them here because of the limitation of space. A DNA computer uses DNA molecules as the carrier of computation and processing information. In 1994, Turing Award winner Prof. Adleman solved a small-scale Hamilton path problem with a DNA experiment (Adleman 1994) which is considered the pioneering work in the field of DNA computing. Since DNA computing has the advantage of massive
123
W. Zhu et al.
parallelization, this technique was rapidly developed. Many DNA computing models and methods were proposed to solve some complex computational problems, including famous non-deterministic polynomial (NP) hard problems and polynomial space (PSPACE) hard problems. For example, Lipton published an article in
, which attempted to solve the satisfiability (SAT) problem (Lipton 1995). Ouyang et al. published an article in on a DNA-computingbased model to solve the maximal clique problem (Ouyang et al. 1997). Shapiro published an article in that solved the automata problem of two states and two characters using autonomous DNA computing (Shapiro et al. 2001). Kensaku et al. published an article in , which represented the logical operations using the so-called hairpin structures of DNA molecules and solved the 3-SAT problem by molecular self-assembly (Kensaku et al. 2000). Zhang et al. published a series of articles on constructing logic gates, which was a new direction of nano-scale computing (Zhang et al. 2016a, b; Yang et al. 2016). Furthermore, the core logical operations were addressed using the algorithmic self-assembly of DNA molecules (Wang et al. 2010). Being a complex computational problem, CTL model checking is always a target of researchers. In 2006, Turing Award winner Prof. Emerson used DNA molecules to conduct CTL model checking for the first time. His DNA-based method works for the basic CTL formula EFp (Emerson et al. 2006). In this work, Kripke structures are used to model the system; the vertices (i.e., states) and edges of the model are encoded into DNA strands. Then, the MC problem of EFp is transformed into DNA reactions among molecule chains. However, EFp is only one of the basic CTL formulas. The above DNA computing method cannot perform MC on other CTL formulas. Therefore, we propose a DNA-computingbased method to check the following basic CTL formulas: EFp, AFp, EGp and AGp. Please note that every CTL formula is a combination of the basic CTL formulas. Thus, the core of the CTL model checking based on DNA computing is solved. This method is the contribution of this paper.
123
One of the fundamental differences between computers and other tools is the universality. Prof. Xu constructed a mathematical model called “probe machine” for the general DNA computer (Xu 2013, 2014). By integrating the storage system, operation system, detection system and control system, he gradually obtained a real general DNA computer: “the Zhongzhou DNA computer” (Xu 2013, 2014). The remainder of this paper is organized as follows. Section 2 proposes the DNA-based algorithms to check the basic CTL formulas. Section 3 conducts some simulated experiments that demonstrate the feasibility of the new algorithm in molecular biology. Section 4 draws the conclusions of this paper.
2 The new algorithms In this section, we will present the DNA-computing-based model-checking algorithms for the four basic CTL formulas, i.e., EGp, AGp, EFp and AFp, where p is an arbitrarily atomic formula. Figure 1 illustrates their intuitive meanings. These CTL formulas describe the following properties. • EGp: There is at least one path in M, such that p is always satisfied. • AGp: For each path in M, p is always satisfied. • EFp: There is at least one path in M, such that p is eventually satisfied. • AFp: For each path in M, p is eventually satisfied. To perform model checking for the above basic CTL formulas, we used some bio-operations, which are summarized in Table 1 and are realizable in biology.
Performing CTL model checking via DNA computing
q
q
q
q
q
q
p
p
q
p
r
EFp
q
q
p
p
q
p
p
q
p
AFp
p
p
p
p
EGp
p
p
p
p
AGp
Fig. 1 Examples of the four basic CTL formulas and their models
Table 1 Bio-operations in the algorithms in this paper The bio-operations
The meaning of the bio-operations
Original documents
Length-separate (T, Tm, Tr, m)
Given a tube T and integer m, this bio-operation separate the DNA strands into two tubes. Tm includes the DNA strands which length is less than m. Tr includes the rest
Adleman (1994)
Subsequence-separate (T, Ts, Tr, s)
Given a tube T, this bio-operation produces tube T s with DNA strands which contains sub-strand s and Tr all the rest
Adleman (1996)
Anneal (T)
Single DNA strands which are complementary with each other according to Watson–Crick law are paired with each other automatically in tube T
Adleman (1994)
Ligate (T, ligase)
DNA ligase repairs the DNA strand skeleton in (3), and forms complete double-stranded structure
Adleman (1994)
Melt (T)
Double-stranded DNA molecules are forced to separate into single-strand molecules by rising temperature in T
Adleman (1996)
Detect (T)
Check whether there exists DNA strands in tube T
Adleman (1994)
Pour (T, strand(s))
Pour the DNA strands of s (s is either a state or a transition) into tube T
Adleman (1994)
123
W. Zhu et al.
We can design the model-checking algorithms based on DNA computing to check the four basic CTL formulas. Ref. Zhu et al. (2016) has proven the following facts: a systematic model M satisfies a basic LTL formula if and only if every path in M, whose length is less than |V | × 2|V |−1 + |E|, satisfies this formula, where |V | and |E| are the numbers of nodes and edges in M, respectively. Similarly, we can easily prove that a systematic model M satisfies a basic CTL formula, if and only if every path in M whose length is less than |V | × 2|V |−1 + |E| satisfies this CTL formula. In this paper, the notation “X” refers to all paths in M whose lengths are less than |V | × 2|V |−1+|E| . Longer paths have no effect on our new algorithms. For model checking, first, all runs in X are generated. Next, different procedures are used to check whether the system model satisfies the properties represented by CTL formulas.
melting, the double DNA strands split into single-stranded DNA strands. According to their length, the DNA strands are separated into two tubes: Tm for the DNA strands whose lengths are less than |S| × 2|S|−1 + |ρ| and Tr for all others.
2.1 Generate all runs in X Adleman’s model (Adleman 1994) uses single-stranded DNA molecules to encode the vertices and edges of a graph and generates runs from the start vertex to the terminal vertex. Similarly, we obtain the runs of the system model here. A Label Finite State Automaton (LFSA) M = (Σ, S, S0 , ρ, F, L) is used to model the system. Atomic propositions p and q are encoded with two singlestranded DNA 5 C( p)3 and 5 C(q)3 with identical lengths and unique identifications. Each state s (s = initial, s = terminal) in M is encoded with single-stranded DNA 5 C(s) R(s)3 , where C(s) = C(L(s)) is a single-stranded DNA molecule. R(s) is used to keep the length of the strands even and make the DNA strands uniquely identified. The initial and terminal states are encoded with single-stranded DNA whose lengths are less than |H (s)| and can be uniquely identified. Let the first part of the strand(s) be 5 H (s)3 and the latter part be 5 T (s)3 . Each transition e = (i, j) is encoded with the single-stranded DNA molecule 3 H (e)T (e)5 . • If i is the initial state, then H (e) = 3 strand(i)5 ; otherwise, H (e) = 3 H (i)5 . • If j is the terminal state, then T (e) = 3 strand( j)5 ; otherwise, T (e) = 3 T ( j)5 . Algorithm Getrun() generates all runs in Rf of system model M. In this paper, an underline denotes a Watson–Crick (WC, for short) complementary. We define an atomic proposition r as the logical complementary of the atomic proposition p. For each state s (s = initial and s = terminal), put strand(s) into tube T. For each transition e, put the Watson– Crick complementary of strand(e) into tube T. The DNA molecules sufficiently anneal and pair with one another. The short double strands ligate to the long double strands. After
123
2.2 DNA model-checking algorithm for the basic CTL formula EGp As in Algorithm 2, in step 1, all runs of the system model whose lengths are less than |S| × 2|S|−1 + |ρ| are generated in tube T. In step 2, a biotin–avidin magnetic system is used to separate strands in tube T into tubes T 1 and T 2. T 1 includes DNA strands containing sub-strand C(r ), and T 2 includes DNA strands that do not contain sub-strand C(r ), where r means “p does not hold”, and C(r ) means the DNA encoding of r. In step 3, detect if there are any DNA strands in T 2. If there are some DNA strands in T 2, they certainly do not contain sub-strand C(r ). For arbitrary state s, either L(s) = p or L(s) = r , so DNA strands in T 2 only contain sub-strand C( p), which shows that all states of a run in T 2 satisfy p, so M EGp. Otherwise, M does not satisfy EGp. The runs in tube T 1 are the counter-examples.
Performing CTL model checking via DNA computing
2.3 DNA model-checking algorithm for the basic CTL formula AGp For the model checking on AGp, Steps 1 and 2 are similar to those in Algorithm 2, which can check EGp. Step 3 is to examine tube T 1. If there are any DNA sequences in T 1, these DNA strands must include at least one sub-strand C(r ). Thus, there are some runs of M where p does not hold in some states of these runs. In this case, M does not satisfy AGp, and DNAs in T 1 are the counter-examples. Otherwise, without the sub-strand C(r ) in Tube T, all runs of the system model satisfy Gp, which proves M AGp.
2.4 The DNA model-checking algorithm for the basic CTL formula EFp Algorithm 4 is to check EFp. Step 1 is identical as before. In step 2, a biotin–avidin magnetic system is used to separate T into T 1, which includes strands that contain sub-strand C( p), and T 2, which does not. Step 3 examines T 1 for any remaining DNA strands. If there is any sub-strand C( p) in T 1, i.e., T 1 is not empty, there is at least one run where p holds in some states in this run. In this case, M satisfies EFp. Otherwise, M does not satisfy EFp, and the runs in T 2 are the counter-examples.
2.5 DNA model-checking algorithm for the basic CTL formula AFp As shown in Algorithm 5, Steps 1 and 2 are similar to algorithm CheckEFp. Step 3 of the algorithm examines T 2. If there are any DNA strands in T 2, there is at least one run where p does not hold in any states of this run. In this case, M does not satisfy AFp, and the runs in T 2 are the counter-examples. Otherwise, M satisfies AFp.
2.6 Complexity analysis The following theorem and corollary indicate the power of the parallel computing that originated from DNA computing and prove that the new algorithms can complete their tasks in linear time. All existing CTL model-checking algorithms are based on electronic computing, such as the methods in Edmund et al. (1999), Iwashita et al. (1997) and Bhat et al. (2002). They run in polynomial time at least to check these formulas. Theorem 2.1 The time complexity of Algorithm 1 is O(n). Proof In the field of DNA computing, the time complexity of an algorithm can be defined as the number of executions of the bio-operations. Algorithm 1 calls the bio-operations only
in Table 1. In fact, this algorithm calls “pour” two times, “anneal” one time, “ligate” one time, “melt” one time and “length-separate” one time. The number of these calls, i.e., the number of executions of the bio-operations, is O(n). Therefore, the time complexity of the Algorithm 1 is O(n). Similarly, we can prove the following corollary. Corollary 2.2 The time complexities of Algorithms 2, 3, 4 and 5 are O(n). Obviously, the new method based on DNA computing significantly reduces the number of basic operations to linear, compared with the classical methods based on electronic computing. However, the time required by the biological operations is neither uniform nor fixed. Some hybridization reaction requires several hours to reach the equilibrium state, which is one of the common flaws of the current DNA computing techniques. Compared with the classical electronic computing, the essence of DNA computing is trading space for time efficiency. In other words, polynomial or exponential DNA molecules compute in parallel manners. The computation is accomplished within linear biological operation steps. If the linear electronic units conduct the identical computation, it will be completed within polynomial or exponential steps. This space-for-time strategy is appropriate because of the large number of DNA molecules. The two types of methods based on different computational mechanisms are complementary. However, the reduction in time complexity is not the first goal of implementing the CTL model checking with DNA computing instead of electronic computing. Please refer to Sect. 4 for more details.
3 Simulation experiments As shown in Table 1, all seven bio-operations in the new algorithms come from the standard Adleman’s DNA computing model, which guarantees that the new algorithms can be effectively realized in biology. The design of the DNA encoding is also related to the success of the experiment. To ensure the specificity of hybridization, an encoding sequence must satisfy some physical constraints and thermodynamic constraints (Wang and Cui 2013). We only study the thermodynamic constraints because the problem is limited by the physical conditions. We examine the thermal denaturation temperature and free energy. A simulation platform called (NUPACK 2015), which is a famous virtual experiment tool, can efficiently simulate the DNA experiments. We use NUPACK as a design platform of our DNA encoding and implement the simulation experiment. We will check the automaton in Fig. 2 and investigate whether it satisfies the four basic CTL formulas.
123
W. Zhu et al. Fig. 2 System model M in our experiments: a LFSA A; b system model M that is equivalent to A (figure b is obtained from a by adding a starting vertex and a terminating vertex. The two vertices add no practical meaning but only for the ease of handling the algorithms)
Table 2 Designed DNA encoding sequence (where WC denotes WC complementary) The DNA chain
5 CGGTTTGGTCGGCTGCTGCAAAGGCGGTCCCTCCTGACCTACCAAGTTAGGACGGCGGTTACTGCG CGCAGTCTCTAAAGCTGCTGCAAAGGCGGTCCCAGACAGTAGCCCCTGCTGCTGCAAAGGCGGTCCC CACCAAGTATTTCCGCTGCTGCAAAGGCGGTCCCGACGAATCCAAACGGCTGCTGCAAAGGCGGTCC CTCTCCGCACTGTTGGTCGGCTGCTGCAAAGGCGGTCCCTCCTGACCTCTAAAGCTGCTGCAAAGGC GGTCCCAGACAGTTATTTCCGCTGCTGCAAAGGCGGTCCCGACGAATTTGGTCGGCTGCTGCAAAGG CGGTCCCTCCTGACAGCCCCTGCTGCTGCAAAGGCGGTCCCCACCAAGCCAAACGGCTGCTGCAAA GGCGGTCCCTCTCCGCTTGGTCGGCTGCTGCAAAGGCGGTCCCTCCTGACTATTTCCGCTGCTGCAAA GGCGGTCCCGACGAATCTACCAAGTTAGGACGGCGGTTACTGCGCGCAGTAGCCCCTGCTGCTGCAA AGGCGGTCCCCACCAAGCTACCAAGTTAGGACGGCGGTTACTGCGCGCAGTTATTTCCGCTGCTGCA AAGGCGGTCCCGACGAATCTCTAAAGCTGCTGCAAAGGCGGTCCCAGACAGTCCAAACGGCTGCTG CAAAGGCGGTCCCTCTCCGC3
The WC of the DNA chain
5 GCGGAGAGGGACCGCCTTTGCAGCAGCCGTTTGGACTGTCTGGGACCGCCTTTGCAGCAGCTTTAG AGATTCGTCGGGACCGCCTTTGCAGCAGCGGAAATAACTGCGCGCAGTAACCGCCGTCCTAACTTGG TAGCTTGGTGGGGACCGCCTTTGCAGCAGCAGGGGCTACTGCGCGCAGTAACCGCCGTCCTAACTTG GTAGATTCGTCGGGACCGCCTTTGCAGCAGCGGAAATAGTCAGGAGGGACCGCCTTTGCAGCAGCCG ACCAAGCGGAGAGGGACCGCCTTTGCAGCAGCCGTTTGGCTTGGTGGGGACCGCCTTTGCAGCAGC AGGGGCTGTCAGGAGGGACCGCCTTTGCAGCAGCCGACCAAATTCGTCGGGACCGCCTTTGCAGCA GCGGAAATAACTGTCTGGGACCGCCTTTGCAGCAGCTTTAGAGGTCAGGAGGGACCGCCTTTGCAGC AGCCGACCAACAGTGCGGAGAGGGACCGCCTTTGCAGCAGCCGTTTGGATTCGTCGGGACCGCCTTT GCAGCAGCGGAAATACTTGGTGGGGACCGCCTTTGCAGCAGCAGGGGCTACTGTCTGGGACCGCCTT TGCAGCAGCTTTAGAGACTGCGCGCAGTAACCGCCGTCCTAACTTGGTAGGTCAGGAGGGACCGCCT TTGCAGCAGCCGACCAAACCG3
3.1 Design of the DNA encoding We have designed a DNA encoding via NUPACK to express system M in Fig. 2, as illustrated in Table 2. The DNA strand from 5 to 3 represents the following character string: s0 , s1 , s2 , s3 , s4 , s5 , s6 , s7 , s1 , s3 , s5 , s1 , s4 , s6 , s1 , s5 , s2 , s4 , s2 , s5 , s3 , s6 . The WC complementary of the DNA strand from 3 to 5 represents the following character string: e(0, 1), e(1, 2), e(2, 3), e(3, 4), e(4, 5), e(5, 6), e(6, 7), x 1 , e(1, 3), e(3, 5), y 5 , x 1 , e(1, 4), e(4, 6), y 6 , x 1 , e(1, 5), y 5 , x 2 , e(2, 4), y 4 , x 2 , e(2, 5), y 5 , x 3 , e(3, 6), y 6 . The relationships among these notations and the WC complementary are illustrated in Fig. 3. Each state si in the state set {s1 , s2 , s3 , s4 , s5 , s6 } contains two code parts: the prefix code xi contains 17 bit bases, and the suffix code yi contains 17 bit bases. The middle 20 bit bases encode an atomic proposition.
123
Table 3 shows the encoding of the state set, edge set, and set of atomic propositions of the encoding sequence in Table 2. Figure 4 shows the thermodynamic analysis of the encoding sequence in Table 2 at 10 ◦ C. As shown in Fig. 4a, the Normalized Ensemble Defect (NED) elucidates the incorrect matching ratio of the nucleotides when a biochemical reaction is in equilibrium. The 0% tips are for an optimal design, whereas 100% tips are for the worst design. The NED of our coding sequence is 0%. The principle of minimum free energy notes that the free energy is minimized when a biochemical reaction is in equilibrium. In Fig. 4b, the matching color between two types of molecules is dark red, which represents the event probability that a double-stranded molecule perfectly matches and reaches the balance. Dark red indicates that this probability is almost 100%. The color change of the vertical bar indi-
Performing CTL model checking via DNA computing
Fig. 3 DNA molecular segments that express the states and edges and the WC relation of the segments Table 3 The DNA encoding of M
Object
The encoding (from 5 to 3 )
Atomic proposition p
GCTGCTGCAAAGGCGGTCCC
Atomic proposition r = p
GTTAGGACGGCGGTTACTGC
State s0
CGGT
State s1
TTGGTCGGCTGCTGCAAAGGCGGTCCCTCCTGAC
State s2
CTACCAAGTTAGGACGGCGGTTACTGCGCGCAGT
State s3
CTCTAAAGCTGCTGCAAAGGCGGTCCCAGACAGT
State s4
AGCCCCTGCTGCTGCAAAGGCGGTCCCCACCAAG
State s5
TATTTCCGCTGCTGCAAAGGCGGTCCCGACGAAT
State s6
CCAAACGGCTGCTGCAAAGGCGGTCCCTCTCCGC
State s7
ACTG
Edge e(0, 1)
TTGCAGCAGCCGACCAAACCG
Edge e(1, 2)
CCGTCCTAACTTGGTAGGTCAGGAGGGACCGCCT
Edge e(1, 3)
TTGCAGCAGCTTTAGAGGTCAGGAGGGACCGCCT
Edge e(1, 4)
TTGCAGCAGCAGGGGCTGTCAGGAGGGACCGCCT
Edge e(1, 5)
TTGCAGCAGCGGAAATAGTCAGGAGGGACCGCCT
Edge e(2, 3)
TTGCAGCAGCTTTAGAGACTGCGCGCAGTAACCG
Edge e(2, 4)
TTGCAGCAGCAGGGGCTACTGCGCGCAGTAACCG
Edge e(2, 5)
TTGCAGCAGCGGAAATAACTGCGCGCAGTAACCG
Edge e(3, 4)
TTGCAGCAGCAGGGGCTACTGTCTGGGACCGCCT
Edge e(3, 5)
TTGCAGCAGCGGAAATAACTGTCTGGGACCGCCT
Edge e(3, 6)
TTGCAGCAGCCGTTTGGACTGTCTGGGACCGCCT
Edge e(4, 5)
TTGCAGCAGCGGAAATACTTGGTGGGGACCGCCT
Edge e(4, 6)
TTGCAGCAGCCGTTTGGCTTGGTGGGGACCGCCT
Edge e(5, 6)
TTGCAGCAGCCGTTTGGATTCGTCGGGACCGCCT
Edge e(6, 7)
CAGTGCGGAGAGGGACCGCCT
cates the balance probability. The results prove that the free energy is approximately equal to the minimum free energy. In Fig. 4c, the position of the red line indicates that all bases in two single strands are completely complementary to each other. The color indicates that the probability of all pairs is approximately equal to 1. Based on the above analysis, we can claim that our DNA sequence satisfies the minimum free energy constraint, and the DNA molecules in the reaction have a fundamentally consistent temperature of the solution chain. Therefore, the experimental results obtained from this encoding are reliable and effective in biology.
With the encoding in Table 3 as an input of Algorithm 1, this algorithm principle is similar to the principle of Adleman’s experiment according to the discussion and analysis of Adleman (1994). A run set of the system, i.e., a path set M, will be generated after Algorithm 1 is executed, as shown in Table 4.
3.2 Experiment 1 (experimental conditions, methods, obtained data and preliminary analysis) It is the key of Algorithms 2 and 3 to check whether there is the fragment that expresses atomic propositionr for all DNA
123
W. Zhu et al.
Fig. 4 Thermodynamic analysis of the encoding in Table 2; a the properties of the structure of the encoding sequence, b thermodynamic analysis: minimum free energy structure and c pairing probability in equilibrium
single-stranded molecules that characterize X. The biotin– avidin magnetic method (Zimmermann et al. 2008) can be used to realize this function. We will simulate this process with NUPACK. For path i, i has fourteen optional values. One value is taken each time. The single-stranded molecules, some of which characterize path i and some characterize the WC complementary of r, are input into the test tube. There are fourteen group sub-experiments for the potential i values. The conditions and processes in each sub-experiment are listed as follows. The two types of single-stranded molecules are poured into a 10−3 -L tube. The corresponding molecular concentrations reach 100 and 100 µM, and the corresponding molecular number is 1016 and 1016 , respectively. When the temperature slowly decreases to 10 ◦ C, the hybridization reaction is observed. Figures 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17 and 18 show the results of the fourteen sub-experiments, where strand1 is a molecule that characterizes path i (molecular i, for short), and strand2
123
is a molecule that characterizes the WC complementary of r. Example 1 Hybridizations between the molecules that characterize path 3 and the molecule that characterizes the WC complementary of r Let us take path 3 as an example, as shown in Fig. 8. The location coordinates of the right slash in red indicate that the base sequence of molecule i from the 46th to the 65th sites in the 5 −3 direction is paired with all bases of the molecule that characterizes the WC complementary of r in the 3 −5 direction. This phenomenon suggests that the hybridization between the two types of molecules is specific. Comparing the color of the slash with the color change of the vertical bar on the right side of the graph, we clearly observe that the former color is notably similar to the color at the top of the vertical bar. This phenomenon suggests that the probability of the base pairs is nearly 100%, which is a higher degree of specificity.
Performing CTL model checking via DNA computing Table 4 All runs (i.e., paths) of X in M Number of path
State sequence in path
Atomic proposition sequence in path
Number of path
State sequence in path
Atomic proposition sequence in path
0
s0 s1 s3 s6 s7
ppp
7
s0 s1 s3 s5 s6 s7
pppp
1
s0 s1 s4 s6 s7
ppp
8
s0 s1 s4 s5 s6 s7
pppp
2
s0 s1 s5 s6 s7
ppp
9
s0 s1 s2 s3 s4 s6 s7
pr ppp
3
s0 s1 s2 s3 s6 s7
pr pp
10
s0 s1 s2 s3 s5 s6 s7
pr ppp
4
s0 s1 s2 s4 s6 s7
pr pp
11
s0 s1 s2 s4 s5 s6 s7
pr ppp
5
s0 s1 s2 s5 s6 s7
pr pp
12
s0 s1 s3 s4 s5 s6 s7
ppppp
6
s0 s1 s3 s4 s6 s7
pppp
13
s0 s1 s2 s3 s4 s5 s6 s7
pr pppp
Fig. 5 Hybridization: 0th path and molecule of WC of r
Fig. 7 Hybridization: 2nd path and molecule of WC of r
Fig. 6 Hybridization: 1st path and molecule of WC of r
Fig. 8 Hybridization: 3rd path and molecule of WC of r
123
W. Zhu et al.
Fig. 9 Hybridization: 4th path and molecule of WC of r
Fig. 11 Hybridization: 6th path and molecule of WC of r
Fig. 10 Hybridization: 5th path and molecule of WC of r
Fig. 12 Hybridization: 7th path and molecule of WC of r
As shown in Fig. 19a, the concentration of strand1–strand2 is 100 µM, which indicates that all molecules that characterize the WC complementary of r are involved in the specific hybridization of molecule i because 100 µM/100 µM = 100%. There is no molecule strand1 or molecule strand2 in the graph. The concentrations of both types of molecules are approximately equal to 0 after their hybridization. (We use “approximately equal to” instead of “equal to” here because NUPACK is only accurate to a certain number.) Therefore, the false negative rate is approximately 0, the false positive rate is approximately 0, and the true positive rate is approximately 100%. Thus, molecule 3 and the molecules that characterize the WC complementary of r are hybridized with strong specificity.
123
According to the analysis of Figs. 8 and 19a, we can conclude that the molecules that characterize r are the sub-chains of molecule 3. Similar to the case of path 3, the molecules that characterize paths 4, 5, 9, 10, 11, and 13 consist of the set of super-chains of the molecules that characterize r according to Figs. 9 and 19b, 10 and 19c, 14 and 19d, 15 and 19e, 16 and 19f, and 18 and 19g, respectively. Example 2 Hybridizations between the molecules that characterize path 0 and the molecule that characterizes the WC complementary of r
Performing CTL model checking via DNA computing
Fig. 13 Hybridization: 8th path and molecule of WC of r
Fig. 15 Hybridization: 10th path and molecule of WC of r
Fig. 16 Hybridization: 11th path and molecule of WC of r Fig. 14 Hybridization: 9th path and molecule of WC of r
With path 0 as another example, as illustrated in Fig. 5, there is no dark red line across strand2, which indicates that the molecules that characterize r are not fully paired with any sub-chain of molecule 0. Therefore, the molecules that characterize r are not the sub-chains of molecule 0. Similar to the case of path 0, molecules 1, 2, 6, 7, 8 and 12 are not the super-chains of the molecules that characterize r according to Figs. 6, 7, 11, 12, 13 and 17, respectively.
3.3 Experiment 2 (experimental conditions, methods, obtained data and preliminary analysis) The key of Algorithms 4 and 5 is to check whether there is a fragment that expresses the atomic proposition p for all DNA single-stranded molecules that characterize X. The biotin– avidin magnetic method (Zimmermann et al. 2008) can be used to realize this function. We will simulate this process with NUPACK.
123
W. Zhu et al.
3.4 Results and discussion
Fig. 17 Hybridization: 12th path and molecule of WC of r
Fig. 18 Hybridization: 13th path and molecule of WC of r
Similar to Experiment 1, Experiment 2 contains fourteen sub-experiments. All conditions and processes are similar to those in Experiment 1. The only difference is that molecule i and the molecules that characterize the WC complementary of p are hybridized. Tables 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17 and 18 show a group of results in fourteen sub-experiments. From these tables, we clearly observe the following points: (1) each base pair of the specific hybridization has a true positive rate, which is more than 94%; (2) 90% of the specific base pairings have true positive rates above 99%. Therefore, the molecules that characterize p are the sub-chains of fourteen types of molecules that characterize the paths.
123
Experiment 1 calls Algorithms 2 and 3 to check whether a system M satisfies EGp and AGp, respectively. Experiment 2 calls Algorithms 4 and 5 to check whether M satisfies EFp and AFp, respectively. The results are shown in Table 19. The specific probability of the DNA computing is less than 100%. It is the probabilistic computing. In actual biochemical reactions, the test tube is bound to have a trace of non-specific molecules that are detected after the algorithms run. Therefore, we must reinterpret the bio-operation “detect” in the algorithms. In fact, the algorithms in this paper can return the equivalent results as long as the specific molecular concentration of the specific results is higher than a threshold (for example, 94%). For example, for Algorithms 4 and 5, if the specific molecular concentration in T2 after the hybridization reaction is lower than 6% of the concentration of the same molecules in T before the hybridization reaction, it can be ignored. The gel-electrophoresis is a technique to read some molecular information, whereas the spectrophotometer-based method can be used to determine the molecular concentration. These methods can be used to read the model-checking results, and their feasibility has been confirmed by Ref. Zhu et al. (2016). The datasets of positive and negative samples do not need to be predefined. We simply need to tell the NUPACK what the required DNA encodings want to express using a piece of NUPACK code. This experimental tool can automatically return the required DNA encodings and ensure that these encodings have good thermal denaturation temperature and free energy. If we input these DNA encodings, which describe the components of a system model, the NUPACK can automatically return the measurements of true positives and negatives. Now, let us compare the new algorithm with some related works. Some approaches have been presented to address DNA model checking problem. Compared with these existing methods, the new one can do something more, as shown in Table 20. A previous study used a parallel model checker DiVinE to analyze the genetic regulatory networks (Barnat et al. 2008) or used the probabilistic model checker PRISM in combination with the DNA strand displacement (DSD) language to design and debug DNA strand displacement components and investigate their kinetics (Lakin et al. 2012). Both methods performed model checking on an electronic computer for biological studies. In comparison, the new approach uses DNA molecules to address a computational problem, i.e., CTL model checking. This is the main difference between the existing methods in Barnat et al. (2008) and Lakin et al. (2012) and the new one in this paper.
Performing CTL model checking via DNA computing
Fig. 19 Molecular concentration after hybridization (a hybridization: 3rd path and molecule of WC of r, b hybridization: 4th path and molecule of WC of r, c hybridization: 5th path and molecule of WC of r, d hybridization: 9th path and molecule of WC of r, e hybridizaTable 5 True positive rate of base pairs between the 0th path and the molecule of WC of p (i.e., p) (all bases are from 5 to 3 )
tion: 10th path and molecule of WC of r, f hybridization: 11th path and molecule of WC of r g hybridization: 13th path and molecule of WC of r)
ith base at p
Base at 0th path for specific pair
Specific pairing probability
ith base at p
Base at 0th path for specific pair
Specific pairing probability
1
31–65–99
0.95111
11
21–55–89
0.99925
2
30–64–98
0.99794
12
20–54–88
0.99965
3
29–63–97
0.99965
13
19–53–87
0.99996
4
28–62–96
0.99985
14
18–52–86
0.99996
5
27–61–95
0.99986
15
17–51–85
0.99985
6
26–60–94
0.99996
16
16–50–84
0.99996
7
25–59–93
0.99996
17
15–49–83
0.99996
8
24–58–92
0.99996
18
14–48–82
0.99955
9
23–57–91
0.99986
19
13–47–81
0.99944
10
22–56–90
0.99955
20
12–46–80
0.98029
In Li (2017), Li and Ma (2015), Li et al. (2015b), Iwashita et al. (1997), Bhat et al. (2002) and Camilli et al. (2015), the model-checking problem is performed on electronic computers, as mentioned in Sect. 1. In comparison, our new method addresses the same problem using a DNA computational device instead of an electronic computer. In a word, Table 21 summarizes the essential distinctions between these existing methods and the new one.
4 Conclusions In this study, we have proposed several new algorithms (Algorithms 2, 3, 4 and 5) and used them to perform model checking for four basic CTL formulas with DNA molecules. This work adds a new member to the solved problem library of DNA computing. It is of value to the universal DNA computer that is currently being developed (Xu 2013, 2014, 2016). This is one motivation, i.e., necessity for us to use
123
W. Zhu et al. Table 6 True positive rate of base pairs between the 1st path and the molecule of WC of p (all bases are from 5 to 3 ) ith base at p
Base at 1st path for specific pair
Specific pairing probability
ith base at p
Base at 1st path for specific pair
Specific pairing probability
1
31–65–99
0.966728
11
21–55–89
0.999262
2
30–64–98
0.999136
12
20–54–88
0.999662
3
29–63–97
0.999764
13
19–53–87
0.999972
4
28–62–96
0.999771
14
18–52–86
0.999972
5
27–61–95
0.999872
15
17–51–85
0.999772
6
26–60–94
0.999972
16
16–50–84
0.999972
7
25–59–93
0.999972
17
15–49–83
0.999972
8
24–58–92
0.999972
18
14–48–82
0.999562
9
23–57–91
0.999872
19
13–47–81
0.999352
10
22–56–90
0.999562
20
12–46–80
0.976852
Table 7 True positive rate of base pairs between the 2nd path and the molecule of WC of p (all bases are from 5 to 3 ) ith base at p
Base at 2nd path for specific pair
Specific pairing probability
ith base at p
Base at 2nd path for specific pair
Specific pairing probability
1
31–99
0.965826
11
21-89
0.998419
2
30–98
0.998218
12
20-88
0.99882
3
29–97
0.99882
13
19-87
0.999121
4
28–96
0.99892
14
18-86
0.999121
5
27–95
0.999021
15
17-85
0.99892
6
26–94
0.999121
16
16-84
0.999021
7
25–93
0.999121
17
15-83
0.999121
8
24–92
0.999121
18
14-82
0.998719
9
23–91
0.999021
19
13-81
0.998418
10
22–90
0.99862
20
12-80
0.973939
Table 8 True positive rate of base pairs between the 3rd path and the molecule of WC of p (all bases are from 5 to 3 ) ith base at p
Base at 3rd path for specific pair
Specific pairing probability
ith base at p
Base at 3rd path for specific pair
Specific pairing probability
1
31–99–133
0.940299
11
21–89–123
0.999277
2
30–98–132
0.997074
12
20–88–122
0.99971
3
29–97–131
0.99972
13
19–87–121
0.999931
4
28–96–130
0.99973
14
18–86–120
0.999931
5
27–95–129
0.999931
15
17–85–119
0.99982
6
26–94–128
0.999942
16
16–84–118
0.999931
7
25–93–127
0.999942
17
15–83–117
0.999931
8
24–92–126
0.999942
18
14–82–116
0.999698
9
23–91–125
0.999831
19
13–81–115
0.999674
10
22–90–124
0.999499
20
12–80–114
0.982605
DNA computing instead of electronic computing for CTL model checking. Furthermore, DNA computing is a type of parallel computer systems that can improve the efficiency of CTL model checking. It is an advantage of using the new method. It is
123
another necessity of using DNA computing instead of electronic computing for CTL model checking. Prof. Thomas, who is a 2015 Nobel Prize winner, has found that cancer likely occurs when the gene repair mechanism is wrong. The DNA repair mechanism in tumor cells
Performing CTL model checking via DNA computing Table 9 True positive rate of base pairs between the 4th path and the molecule of WC of p (all bases are from 5 to 3 ) ith base at p
Base at 4th path for specific pair
Specific pairing probability
ith base at p
Base at 4th path for specific pair
Specific pairing probability
1
31–99–133
0.9436
11
21–89–123
0.9993
2
30–98–132
0.9966
12
20–88–122
0.9997
3
29–97–131
0.9986
13
19–87–121
1.0000
4
28–96–130
0.9997
14
18–86–120
1.0000
5
27–95–129
0.9998
15
17–85–119
0.9998
6
26–94–128
1.0000
16
16–84–118
0.9999
7
25–93–127
1.0000
17
15–83–117
1.0000
8
24–92–126
1.0000
18
14–82–116
0.9995
9
23–91–125
0.9998
19
13–81–115
0.9989
10
22–90–124
0.9995
20
12–80–114
0.9724
Table 10 True positive rate of base pairs between the 5th path and the molecule of WC of p (all bases are from 5 to 3 ) ith base at p
Base at 5th path for specific pair
Specific pairing probability
ith base at p
Base at 5th path for specific pair
Specific pairing probability
1
31–133
0.9612
11
21–123
0.9985
2
30–132
0.9981
12
20–122
0.9988
3
29–131
0.9988
13
19–121
0.9991
4
28–130
0.9989
14
18–120
0.9991
5
27–129
0.9990
15
17–119
0.9989
6
26–128
0.9991
16
16–118
0.9991
7
25–127
0.9991
17
15–117
0.9991
8
24–126
0.9991
18
14–116
0.9987
9
23–125
0.9990
19
13–115
0.9985
10
22–124
0.9986
20
12–114
0.9740
Table 11 True positive rate of base pairs between the 6th path and the molecule of WC of p (all bases are from 5 to 3 ) ith base at p
Base at 6th path for specific pair
Specific pairing probability
ith base at p
Base at 6th path for specific pair
Specific pairing probability
1
31–65–99–133
0.974917
11
21–55–89–123
0.999291
2
30–64–98–132
0.999241
12
20–54–88–122
0.999712
3
29–63–97–131
0.999686
13
19–53–87–121
0.999913
4
28–62–96–130
0.999809
14
18–52–86–120
0.999913
5
27–61–95–129
0.999913
15
17–51–85–119
0.999813
6
26–60–94–128
1.000000
16
16–50–84–118
0.999913
7
25–59–93–127
1.000000
17
15–49–83–117
0.999913
8
24–58–92–126
1.000000
18
14–48–82–116
0.999582
9
23–57–91–125
0.999913
19
13–47–81–115
0.999569
10
22–56–90–124
0.999502
20
12–46–80–114
0.985698
is essential for cancer treatment (Shankara et al. 2011). The methods of artificially controlled gene repair will provide molecular means for this purpose. To improve the abil-
ity of automatic discovery and repair of abnormal gene expressions, researchers often concern the spatio-temporal expression of the genes. Cellular logical computing, which
123
W. Zhu et al. Table 12 True positive rate of base pairs between the 7th path and the molecule of WC of p (all bases are from 5 to 3 ) ith base at p
Base at 7th path for specific pair
Specific pairing probability
ith base at p
Base at 7th path for specific pair
Specific pairing probability
1
31–65–99–133
0.953289
11
21–55–89–123
0.99922
2
30–64–98–132
0.99872
12
20–54–88–122
0.99962
3
29–63–97–131
0.99973
13
19–53–87–121
1.00000
4
28–62–96–130
0.99973
14
18–52–86–120
1.00000
5
27–61–95–129
0.99993
15
17–51–85–119
0.99973
6
26–60–94–128
1.00000
16
16–50–84–118
1.00000
7
25–59–93–127
1.00000
17
15–49–83–117
1.00000
8
24–58–92–126
1.00000
18
14–48–82–116
0.99962
9
23–57–91–125
0.99993
19
13–47–81–115
0.99952
10
22–56–90–124
0.99962
20
12–46–80–114
0.981534
Table 13 True positive rate of base pairs between the 8th path and the molecule of WC of p (all bases are from 5 to 3 ) ith base at p
Base at 8th path for specific pair
Specific pairing probability
ith base at p
Base at 8th path for specific pair
Specific pairing probability
1
31–99–133
0.960175
11
21–89–123
0.999063
2
30–98–132
0.998712
12
20–88–122
0.999407
3
29–97–131
0.999407
13
19–87–121
0.999729
4
28–96–130
0.999517
14
18–86–120
0.999729
5
27–95–129
0.999629
15
17–85–119
0.999518
6
26–94–128
0.999729
16
16–84–118
0.999629
7
25–93–127
0.999739
17
15–83–117
0.999729
8
24–92–126
0.999729
18
14–82–116
0.999205
9
23–91–125
0.999628
19
13–81–115
0.998900
10
22–90–124
0.999295
20
12–80–114
0.973144
Table 14 True positive rate of base pairs between the 9th path and the molecule of WC of p (all bases are from 5 to 3 ) ith base at p
Base at 9th path for specific pair
Specific pairing probability
ith base at p
Base at 9th path for specific pair
Specific pairing probability
1
31–99–133–167
0.97523
11
21–89–123–157
0.999329
2
30–98–132–166
0.999321
12
20–88–122–156
0.999631
3
29–97–131–165
0.999733
13
19–87–121–155
0.999933
4
28–96–130–164
0.999731
14
18–86–120–154
0.999933
5
27–95–129–163
0.999933
15
17–85–119–153
0.999832
6
26–94–128–162
0.999934
16
16–84–118–152
0.999933
7
25–93–127–161
0.999934
17
15–83–117–151
0.999933
8
24–92–126–160
0.999934
18
14–82–116–150
0.999727
9
23–91–125–159
0.999832
19
13–81–115–149
0.999725
10
22–90–124–158
0.999530
20
12–80–114–148
0.983385
was developed in recent years, provides some autonomy methods for molecular diagnosis and gene repair of the human diseases caused by gene mutation (Zimmermann et al. 2008). Since CTL formulas can describe the branch tempo-
123
ral relationships of the dynamic genetic changes, CTL model checking in human living cells will explore an intelligent and automatic computational method of dynamic gene identification and repair in molecular robots. This is an application
Performing CTL model checking via DNA computing Table 15 True positive rate of base pairs between the 10th path and the molecule of WC of p (all bases are from 5 to 3 ) ith base at p
Base at 10th path for specific pair
Specific pairing probability
ith base at p
Base at 10th path for specific pair
Specific pairing probability
1
31–99–133–167
0.97136
11
21–89–123–157
0.99938
2
30–98–132–166
0.99926
12
20–88–122–156
0.99961
3
29–97–131–165
0.99971
13
19–87–121–155
1.00000
4
28–96–130–164
0.99972
14
18–86–120–154
1.00000
5
27–95–129–163
0.99993
15
17–85–119–153
0.99972
6
26–94–128–162
1.00000
16
16–84–118–152
0.99993
7
25–93–127–161
1.00000
17
15–83–117–151
1.00000
8
24–92–126–160
1.00000
18
14–82–116–150
0.99968
9
23–91–125–159
0.99993
19
13–81–115–149
0.99966
10
22–90–124–158
0.99949
20
12–80–114–148
0.98168
Table 16 True positive rate of base pairs between the 11th path and the molecule of WC of p (all bases are from 5 to 3 ) ith base at p
Base at 11th path for specific pair
Specific pairing probability
ith base at p
Base at 11th path for specific pair
Specific pairing probability
1
31–99–133–167
0.95588
11
21–89–123–157
0.99929
2
30–98–132–166
0.99873
12
20–88–122–156
0.99972
3
29–97–131–165
0.99966
13
19–87–121–155
0.99996
4
28–96–130–164
0.99983
14
18–86–120–154
0.99996
5
27–95–129–163
0.99985
15
17–85–119–153
0.99983
6
26–94–128–162
0.99996
16
16–84–118–152
0.99996
7
25–93–127–161
0.99996
17
15–83–117–151
0.99996
8
24–92–126–160
0.99996
18
14–82–116–150
0.99945
9
23–91–125–159
0.99985
19
13–81–115–149
0.99918
10
22–90–124–158
0.99951
20
12–80–114–148
0.97437
Table 17 True positive rate of base pairs between the 12th path and the molecule of WC of p (all bases are from 5 to 3 ) ith base at p
Base at 12th path for specific pair
Specific pairing probability
ith base at p
Base at 12th path for specific pair
Specific pairing probability
1
31–65–99–133–167
0.965978
11
21–55–89–123–157
0.999295
2
30–64–98–132–166
0.999127
12
20–54–88–122–156
0.999726
3
29–63–97–131–165
0.999717
13
19–53–87–121–155
0.999967
4
28–62–96–130–164
0.999744
14
18–52–86–120–154
0.999967
5
27–61–95–129–163
0.999867
15
17–51–85–119–153
0.999746
6
26–60–94–128–162
0.999967
16
16–50–84–118–152
0.999967
7
25–59–93–127–161
0.999967
17
15–49–83–117–151
0.999967
8
24–58–92–126–160
0.999967
18
14–48–82–116–150
0.999506
9
23–57–91–125–159
0.999857
19
13–47–81–115–149
0.999354
10
22–56–90–124–158
0.999616
20
12–46–80–114–148
0.983258
123
W. Zhu et al. Table 18 True positive rate of base pairs between the 13th path and the molecule of WC of p (all bases are from 5 to 3 ) ith base at p
Base at 13th path for specific pair
Specific pairing probability
ith base at p
Base at 13th path for specific pair
Specific pairing probability
1
31–99–133–167–201
0.97238
11
21–89–123–157–191
0.999299
2
30–98–132–166–200
0.999222
12
20–88–122–156–190
0.999722
3
29–97–131–165–199
0.999715
13
19–87–121–155–189
0.999944
4
28–96–130–164–198
0.999822
14
18–86–120–154–188
0.999944
5
27–95–129–163–197
0.999943
15
17–85–119–153–187
0.999833
6
26–94–128–162–196
0.999944
16
16–84–118–152–186
0.999943
7
25–93–127–161–195
0.999944
17
15–83–117–151–185
0.999944
8
24–92–126–160–194
0.999944
18
14–82–116–150–184
0.999629
9
23–91–125–159–193
0.999843
19
13–81–115–149–183
0.999545
10
22–90–124–158–192
0.999510
20
12–80–114–148–182
0.982708
Table 19 Model-checking results on four basic CTL formulas and M using the new algorithms Algorithm
Key biochemical operation
Result of biochemical operation: molecules in T1 (path expressed by molecule)
Result of biochemical operation: molecules in T2 (path expressed by molecule)
Model-checking result
2
Subsequence-separate
3, 4, 5, 9, 10, 11, 13
0, 1, 2, 6, 7, 8, 12
M satisfies EGp
3
Subsequence-separate
3, 4, 5, 9, 10, 11, 13
0, 1, 2, 6, 7, 8, 12
M do not satisfies AGp
4
Subsequence-separate
All of 14 kinds of molecules
None
M satisfies EFp
5
Subsequence-separate
All of 14 kinds of molecules
None
M satisfies AFp
Table 20 Some DNA-based approaches for model-checking temporal logics The formulas\the methods
Molecular_MC_EFp (Emerson et al. 2006)
DNA_MC_LTL (Zhu et al. 2016)
The method in this paper
EFp
Can check
Cannot check
Can check
AFp
Cannot check
Cannot check
Can check
EGp
Cannot check
Cannot check
Can check
AGp
Cannot check
Cannot check
Can check
Fp
Cannot check
Can check
Cannot check
Gp
Cannot check
Can check
Cannot check
Table 21 More comparisons with the related works The methods
Perform computations USING DNA molecules or electronic devices?
Perform computations for the PURPOSE of a computational problem or a biological one?
GPoLTL Model Checking (Li 2017)
Using electronic devices
For a computational problem
GPoCTL Model Checking (Li and Ma 2015)
Using electronic devices
For a computational problem
PoCTL Model Checking (Li et al. 2015b)
Using electronic devices
For a computational problem
BINGO(Fwd) (Iwashita et al. 1997)
Using electronic devices
For a computational problem
modchkCTL* (Bhat et al. 2002)
Using electronic devices
For a computational problem
DiVinE_GRN (Barnat et al. 2008)
Using electronic devices
For a biological problem
PRISM_DSD (Lakin et al. 2012)
Using electronic devices
For a biological problem
MapReduce-based CTL (Camilli et al. 2015)
Using electronic devices
For a computational problem
The new method
Using DNA molecules
For a computational problem
123
Performing CTL model checking via DNA computing
foreground of the new method. It is also a necessity of using DNA computing instead of electronic computing for CTL model checking because the traditional CTL model-checking technique is based on electronic computing and can never be embedded into human living cells. Acknowledgements This study was partially funded by the National Natural Science Foundation of China under Grant Nos. U1204608 and 61572444 and China Postdoctoral Science Foundation under Grant No. 2015M572120.
Compliance with ethical standards Conflict of interest The authors of this paper declare that they have no conflicts of interest. Ethical standard This article does not contain any studies with human participants or animals performed by the authors.
References Adleman LM (1994) Molecular computation of solutions to combinatorial problems. Science 266(5187):1021–1024 Adleman LM (1996) On constructing a molecular computer. Discrete Math Theor Comput Sci 27:1–21 Andreas C, Maxime C, Pierre Y (2013) Featured transition systems: foundations for verifying variability-intensive systems and their application to LTL model checking. IEEE Trans Softw Eng 39(8):1069–1089 Barnat J, Brim L, Ivana C (2008) Parallel model checking large-scale genetic regulatory networks with DiVinE. Electron Notes Theor Comput Sci 194(3):35–50 Bhat G, Cleaveland R, Grumberg O (2002) Efficient on-the-fly model checking for CTL. In: IEEE symposium on logic in computer science, p 388 Brim L, Milan C, David S (2013) Model checking of biological systems. Formal methods for dynamical systems. Springer, Berlin, pp 63– 112 Camilli M, Bellettini C, Capra L, Monga M (2015) CTL Model checking in the cloud using MapReduce. In: International symposium on symbolic and numeric algorithms for scientific computing, pp 333– 340 Edmund MC, Doron AP, Orna G (1999) Model checking. MIT, Massachusetts Emerson EA, Edmund MC (1982) Using branching-time temporal logic to synthesize synchronization skeletons. Sci Comput Program 2(3):241–266 Emerson EA, Kristina DH, Jay HK (2006) Molecular model checking. Int J Found Comput Sci 17(04):733–742 Iwashita H, Nakata T, Hirose F(1997) CTL model checking based on forward state traversal. In: IEEE/ACM international conference on computer-aided design, pp 82–87 Kensaku S, Hidetaka G, Ken K (2000) Molecular computation by DNA hairpin formation. Science 288(5469):1223–1226 Lakin M, Parker D, Cardelli L (2012) Design and analysis of DNA strand displacement devices using probabilistic model checking. J R Soc Interface 9(72):1470–1485
Li YM (2017) Quantitative model checking of linear-time properties based on generalized possibility measures. Fuzzy Sets Syst 320:17–39 Li YM, Ma ZY (2015) Quantitative computation tree logic model checking based on generalized possibility measures. IEEE Trans Fuzzy Syst 23(6):2034–2047 Li YM, Huang SB, Lin JY (2015a) Data flow analysis and formal method. In: International conference of young computer scientists, engineers and educators, ICYCSEE 2015, intelligent computation in big data era, volume 503 of the series communications in computer and information science, Harbin, China, pp 398–406 Li YM, Li YL, Ma ZY (2015b) Computation tree logic model checking based on possibility measures. Fuzzy Sets Syst 262:44–59 Lipton RJ (1995) DNA solution of hard computational problems. Science 268(5210):542–545 NUPACK (2015) http://www.nupack.org/partition/new Ouyang Q, Peter DK, Liu S (1997) DNA solution of the maximal clique problem. Science 278(5337):446–449 Pnueli A (1977) The temporal logic of programs. In: Symposium on foundations of computer science, Washington, DC, USA, pp 46– 57 Roberto C (2011) LTL model-checking for security protocols. AI Commun 24(3):281–283 Shankara C, Das S, Vidyarthi A (2011) Homology modeling and function prediction of hABH1, involving in repair of alkylation damaged DNA. Interdiscip Sci Comput Life Sci 3(3):175–181 Shapiro E, Benenson Y, Adar R (2001) Programmable and autonomous computing machine made of biomolecules. Nature 414(6862):430–434 Wang YF, Cui GZ (2013) The design and optimization of DNA coding sequence. Publishing House of Electronics Industry, Beijing Wang YF, Sun JW, Cui GZ, Zhang XC, Zheng Y (2010) Basic logical operations using algorithmic self-assembly of DNA molecules. J Nanoelectron Optoelectron 5(1):30–37 Xu J (2013) The development programme of the Zhongzhou I DNA computer. Technical report TR-12. Beijing University, Beijing (in Chinese) Xu J (2014) Forthcoming era of biological computer. Bull Chin Acad Sci 29(1):42–54 (in Chinese) Xu J (2016) Probe machine. IEEE Trans Neural Netw Learn Syst 27(7):1405–1416 Yang J, Jiang SX, Liu XR, Pan LQ, Zhang C (2016) Aptamer-binding directed DNA origami pattern for logic gates. ACS Appl Mater Interfaces 8(49):34054–34060 Zhang C, Yang J, Jiang SX, Liu Y, Yan H (2016a) DNAzyme-mediated DNA origami pattern for logic gates. Nano Lett 16(1):736 Zhang C, Shen LJ, Liang C, Dong YF, Yang J, Xu J (2016b) DNA sequential logic gate using two-ring DNA. ACS Appl Mater Interfaces 8(14):9370–9376 Zhu WJ, Zhou QL, Zhang QX (2016) A LTL model checking approach based on DNA computing. Chin J Comput 39(12):2578–2597 (in Chinese) Zimmermann KH, Israel MP, Zoya I (2008) DNA computing models. Springer, New York Publisher’s Note Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
123
