Computer Science ›› 2019, Vol. 46 ›› Issue (11): 25-31.doi: 10.11896/jsjkx.181102091
• Surveys • Previous Articles Next Articles
HAN Ying-jie, ZHOU Qing-lei, ZHU Wei-jun
CLC Number:
[1]BARNAT J,BAUCH P,BRIM L,et al.Designing fast LTLmodel checking algorithms for many-core GPUs[J].Journal of Parallel and Distributed Computing,2012,72(9):1083-1097. [2]CARBONE R.LTL model-checking for security protocols [J].AI Communications,2011,24(3):281-283. [3]FU S,TAYSSIR T.Efficient CTL model-checking for pushdown systems [J].Theoretical Computer Science,2014,549(3):127-145. [4]BRIM L,ČEKA M,AFRÁNEK D.Model checking of biological systems[M]∥Formal Methods for Dynamical Systems.Berlin:Springer-Verlag,2013:63-112. [5]HOU G,ZHOU K J,YONG J W,et al.Survey of state explosion problem in model checking [J].Computer Science,2013,40(S1):77-86.(in Chinese) 侯刚,周宽久,勇嘉伟,等.模型检测中状态爆炸问题研究综述[J].计算机科学,2013,40(S1):77-86. [6]XU J.Forthcoming era of biological computer [J].Bulletin ofChinese Academy of Sciences,2014,29(1):42-54.(in Chinese) 许进.生物计算机时代即将来临[J].中国科学院院刊,2014,29(1):42-54. [7]EMERSON E A,HAGER K D,KONIECZKA J H.Molecularmodel checking [J].International Journal of Foundations of Computer Science,2006,17(4):733-741. [8]CLARKE E M,GRUMBERG O,HIRAISHI H,et al.Verification of the futurebus+ cache coherence protocol[J].Formal Methods in System Design,1995,6(2):217-232. [9]ANDERSON R J,BEAME P,BURNS S,et al.Model checking large software specifications [J].IEEE Transactions on Software Engineering,1998,24(7):498-520. [10]CLARKE E M,EMERSON E A.Design and synthesis of synchronization skeletons using branching-time temporal logic[C]∥The Workshop on Logic of Programs.Berlin:Springer,1981,131:52-71. [11]QUEILLE J P,SIFAKIS J.Specification and verification of concurrent systems in CESAR[C]∥Colloquium on International Symposium on Programming.Berlin:Springer-Verlag,1982:337-351. [12]CLARKE E M,GRUMBERG O,PELED D A.Model checking [M].Massachusetts:The MIT Press,1999:35-36. [13]HAN Y J,ZHU W J,JIAO L F,et al.DNA computing methodsof LTL model checking on Xp [J].Mini-Micro Systems,2017,38(3):553-558.(in Chinese) 韩英杰,朱维军,焦林枫,等.线性时序逻辑公式Xp模型检测的DNA计算方法[J].小型微型计算机系统,2017,38(3):553-558. [14]MARTÍNEZ-PÉREZ I M,ZIMMERMANN K H,IGNATOVA Z.An autonomous DNA model for finite state automata [J].International Journal of Bioinformatics Research & Applications,2009,5(1):81-96. [15]ZIMMERMANN K H,ISRAEL M P,ZOYA I.DNA computing models [M].New York:Springer,2008:127-128. [16]ZHU W J,HAN Y J,ZHOU Q L.Performing CTL model checking via DNA computing [J/OL].https://doi.org/10.1007/s00500-018-3314-7. [17]ZHU W J,WANG Y F,ZHOU Q L,et al.Model checking computational tree logic using sticker automata[M]∥Bio-Inspired Computing-Theories and Applications.Singapore:Springer,2016:12-20. [18]ZHU W J,ZHOU Q L,ZHANG Q X.A LTL model checking approach based on DNA computing [J].Chinese Journal of Computers,2016,39(12):2578-2597.(in Chinese) 朱维军,周清雷,张钦宪.基于DNA计算的线性时序逻辑模型检测方法[J].计算机学报,2016,39(12):2578-2597. [19]KUPFERMAN O,PNUELI A.Once and for all[C]∥Procee-dings of Tenth Annual IEEE Symposium on Logic in Computer Science.New Jersey:IEEE Computer Society Press,1995:25-35. [20]LICHTENSTEIN O,PNUELI A,ZUCK L.The glory of thepast[M]∥Logics of Programs.Berlin:Springer,1985:196-218. [21]EMERSON E A.Temporal and modal logic[M]∥Handbook ofTheoretical Computer Science.Massachusetts:The MIT Press,1990:995-1072. [22]HAN Y J,ZHOU Q L,JIAO L F,et al.Model checking forcomputation tree logic with past based on DNA computing[M]∥Bio-Inspired Computing-Theories and Applications.Singapore:Springer,2017:131-147. [23]ZHU W J,ZHOU Q L,LI Y L.LTL model checking based on DNA computing[J].Acta Electronica Sinica,2016,44(6):1265-1271.(in Chinese) 朱维军,周清雷,李永亮.以DNA 为载体的线性时序逻辑模型检测[J].电子学报,2016,44(6):1265-1271. [24]ZHU W J,FENG C,WU H M.Model checking temporal logic formulas using sticker automata[J].BioMed Research International,2017,2017(3):1-33. [25]MARTÍNEZ-PÉREZ I M,ZHANG G,IGNATOVA Z,et al.Computational genes:a tool for molecular diagnosis and therapy of aberrant mutational phenotype [J].BMC Bioinformatics,2007,8(1):365-365. [26]ADLEMAN L M.On constructing a molecular computer[M]∥Lipton R J,Baum E B,eds.DNA Based Computers.American Mathematical Society,1996:1-21. [27]LIU Q,WANG L,FRUTOS A G,et al.DNA computing on surfaces [J].Nature,2000,403(6766):175-178. [28]ROWEIS S,WINFREE E,BURGOYNE R,et al.A stickerbased model for DNA computation [J].Journal of ComputationalBiology,1998,5(4):615-629. [29]HEAD T.Splicing Schemes and DNA[C]∥Lindenmayer Systems:Impacts on theoretical computer science,computer graphics and developmental biology.Heidelberg:Springer,1992:371-383. [30]ADLEMAN L M.Molecular computation of solutions to combinatorial problems [J].Science,1994,266(5187):1021-1023. [31]LIPTON R J.DNA solution of hard computational problems[J].Science,1995,268(5210):542-545. [32]BRAICH R S,CHELYAPOV N,JOHNSON C,et al.Solution of a 20-variable 3-SAT problem on a DNA computer [J].Science,2002,296(5567):499-502. [33]OUYANG Q,KAPLAN P D,LIU S,et al.DNA solution of the maximal clique problem[J].Science,1997,278(5337):446-449. [34]GAO L,XU J.DNA solution of vertex cover problem based on sticker model[J].Chinese Journal of Electronics,2002,11(2):280-284. [35]LI K L,ZHOU X,XU J.An O(2n) Volume molecular solutionsfor the 3-colorable problem on DNA—based supercomputing [J].Acta Electronica Sinica,2008,36(11):2096-2101.(in Chinese) 李肯立,周旭,许进.图3-着色问题的O(2n)链数DNA计算机算法[J].电子学报,2008,36(11):2096-2101. [36]WINFREE E,LIU F,WENZLER L A,et al.Design and self-assembly of two-dimensional DNA crystals [J].Nature,1998,394(6693):539-544. [37]SAKAMOTO K,GOUZU H,KOMIYA K,et al.Molecularcomputation by DNA hairpin formation [J].Science,2000,288(6469):1223-1226. [38]BENENSON Y,PAZ-ELIZUR T,ADAR R,et al.Programmable and autonomous computing machine made of biomolecules [J].Nature,2001,414(6862):430-439. [39]KURAMOCHI J,SAKAKIBARA Y.Intensive in vitro experiments of implementing and executing finite automata in test tube[M]∥DNA Computing.Berlin:Springer,2005:193-202. [40]XIAO J H,XU J.The DNA computation model based on giant magnetoresistance for sat problem [J].Chinese Journal of Computers,2013,36(4):829-835.(in Chinese) 肖建华,许进.可满足性问题的巨磁电阻型DNA计算模型[J].计算机学报,2013,36(4):829-835. [41]XU J.Probe machine[J].IEEE Transactions on Neural Networks and Learning Systems,2016,27(7):1405-1416. [42]LI K L,LUO X,WU F,et al.An algorithm in tile assembly model for maximum clique problem [J].Journal of Computer Research and Development,2013,50(3):666-675.(in Chinese) 李肯立,罗兴,吴帆,等.基于自组装模型的最大团问题DNA计算算法[J].计算机研究与发展,2013,50(3):666-675. [43]ZHANG G,IGNATOVA Z.Biomolecular autonomous solutionof the Hamiltonian path problem via hairpin formation [J].International Journal of Bioinformatics Research & Applications,2005,1(4):389-398. [44]YANG J,DONG C,DONG Y F,et al.Logic nanoparticle beacon triggered by the binding-induced effect of multiple inputs[J].ACS Applied Materials & Interfaces,2014,6(16):14486-14492. [45]YANG J,JIANG S X,LIU X R,et al.Aptamer-Binding Directed DNA Origami Pattern for Logic Gates[J].ACS Applied Materials & Interfaces,2016,8(49):34054-34060. [46]PAN L Q,WANG Z Y,LI Y F,et al.Nicking enzyme-controlled toehold regulation for DNA logic circuits[J].Nanoscale,2017,9(46):18223-18228. [47]YANG J,WU R F,LI Y F,et al.Entropy-driven DNA logic circuits regulated by DNAzyme[J].Nucleic Acids Research,2018,46(16):8532-8541. [48]SHI X L,WANG Z Y,DENG C Y,et al.A novel bio-sensorbased on DNA strand displacement [J].Plos One,2014,9(10),e108856-e108856. [49]LI X,SONG T,SHI X L,et al.A universal fast colorimetricmethod for DNA signal detection with DNA strand displacement and gold nanoparticles [J].Journal of Nanomaterials,2015(1/2):1-9. [50]LI X,LI H,SONG T,et al.Highly biocompatible drug-delivery systems based on DNA nanotechnology [J].Journal of BiomedicalNanotechnology,2017,13(7):747-757. [51]SHI X L,CHEN C Z,LI X,et al.Size controllable DNA nanoribbons assembled from three types of reusable brick single-strand DNA tiles [J].Soft matter,2015,11(43):8484-8492. [52]SHI X L,WU X X,SONG T,et al.Construction of DNA nanotubes with controllable diameters and patterns by using hierarchical DNA sub-tiles [J].Nanoscale,2016,8(31):14785-14792. [53]The NUPACK team.NUPACK[EB/OL].http://www.nupack.org. [54]ZHU W J,HAN Y J,WU H M,et al.Predicting the results of molecular specific hybridization using boosted tree algorithm[J/OL].https://www.researchgate.net/publication/327760975_Predicting_the_results_of_molecular_specific_hybridization_using_boosted_tree_algorithm. [55]XU J,TAN G J,FAN Y K,et al.DNA computer principle,advances and difficulties(IV):on the models of DNA computer[J].Chinese Journal of Computers,2007,30(6):881-893.(in Chinese) 许进,谭钢军,范月科,等.DNA计算机原理、进展及难点(IV):论DNA计算机模型[J].计算机学报,2007,30(6):881-893. |
[1] | RAN Dan, CHEN Zhe, SUN Yi, YANG Zhi-bin. SCADE Model Checking Based on Program Transformation [J]. Computer Science, 2021, 48(12): 125-130. |
[2] | CAI Yong, QIAN Jun-yan, PAN Hai-yu. Approximate Safety Properties in Metric Linear Temporal Logic [J]. Computer Science, 2020, 47(10): 309-314. |
[3] | XIA Nu-nu, YANG Jin-ji, ZHAO Gan-sen, MO Xiao-shan. Formal Verification of Cloud-aided Lightweight Certificateless Authentication Protocol Based on Probabilistic Model [J]. Computer Science, 2019, 46(8): 206-211. |
[4] | ZHOU Nv-qi, ZHOU Yu. Multi-objective Verification of Web Service Composition Based on Probabilistic Model Checking [J]. Computer Science, 2018, 45(8): 288-294. |
[5] | LI Yun-chou,YIN Ping. Research of Model Checking Application on Aerospace TT&C Software [J]. Computer Science, 2018, 45(6A): 523-526. |
[6] | LEI Li-hui and WANG Jing. Parallelization of LTL Model Checking Based on Possibility Measure [J]. Computer Science, 2018, 45(4): 71-75. |
[7] | NIE Kai, ZHOU Qing-lei, ZHU Wei-jun and ZHANG Chao-yang. Modeling for Three Kinds of Network Attacks Based on Temporal Logic [J]. Computer Science, 2018, 45(2): 209-214. |
[8] | YANG Hong, HONG Mei, QU Yuan-yuan. Approach of Mutation Test Case Generation Based on Model Checking [J]. Computer Science, 2018, 45(11A): 488-493. |
[9] | ZHAO Ying, PAN Hua, ZHANG Yun-meng, MO Qi, DAI Fei. Modeling and Behavior Verification for Collaborative Business Processes [J]. Computer Science, 2018, 45(11A): 597-602. |
[10] | LIU Shuang, WEI Ou, GUO Zong-hao. Infinite-horizon Optimal Control of Genetic Regulatory Networks Based on Probabilistic Model Checking and Genetic Algorithm [J]. Computer Science, 2018, 45(10): 313-319. |
[11] | DU Yi, HE Yang and HONG Mei. Application of Probabilistic Model Checking in Dynamic Power Management [J]. Computer Science, 2018, 45(1): 261-266. |
[12] | GAO Wan-ling, HONG Mei, YANG Qiu-hui and ZHAO He. Efficiency Analysis of Different Statistical Algorithms on Statistical Model Checking [J]. Computer Science, 2017, 44(Z6): 499-503. |
[13] | QU Yuan-yuan, HONG Mei and SUN Ning. Formal Verification of TAPE Strategy for Dynamic Temperature Management in Multi-core System [J]. Computer Science, 2017, 44(Z11): 542-546. |
[14] | GUO Zong-hao and WEI Ou. Optimal Control of Probabilistic Boolean Networks Using Model Checking [J]. Computer Science, 2017, 44(5): 193-198. |
[15] | LIU Bin-bin, LIU Wan-wei, MAO Xiao-guang and DONG Wei. Correctness Verification of Rules for Unmanned Vehicles’ Decision System [J]. Computer Science, 2017, 44(4): 72-74. |
|