Model Checking Temporal Logic Formulas Using Sticker Automata

被引:2
作者
Zhu, Weijun [1 ]
Feng, Changwei [2 ]
Wu, Huanmei [3 ]
机构
[1] Zhengzhou Univ, Sch Informat Engn, Zhengzhou 450001, Henan, Peoples R China
[2] Zhengzhou Univ, Affiliated Hosp 2, Zhengzhou 450001, Henan, Peoples R China
[3] Indiana Univ Purdue Univ Indianapolis, Sch Informat & Comp, Indianapolis, IN USA
基金
中国博士后科学基金; 中国国家自然科学基金;
关键词
DNA; COMPUTATION; DESIGN;
D O I
10.1155/2017/7941845
中图分类号
Q81 [生物工程学(生物技术)]; Q93 [微生物学];
学科分类号
071005 ; 0836 ; 090102 ; 100705 ;
摘要
As an important complex problem, the temporal logic model checking problem is still far from being fully resolved under the circumstance of DNA computing, especially Computation Tree Logic (CTL), Interval Temporal Logic (ITL), and Projection Temporal Logic (PTL), because there is still a lack of approaches for DNA model checking. To address this challenge, a model checking method is proposed for checking the basic formulas in the above three temporal logic types with DNA molecules. First, one-type single-stranded DNA molecules are employed to encode the Finite State Automaton (FSA) model of the given basic formula so that a sticker automaton is obtained. On the other hand, other single-stranded DNA molecules are employed to encode the given system model so that the input strings of the sticker automaton are obtained. Next, a series of biochemical reactions are conducted between the above two types of single-stranded DNA molecules. It can then be decided whether the system satisfies the formula or not. As a result, we have developed a DNA-based approach for checking all the basic formulas of CTL, ITL, and PTL. The simulated results demonstrate the effectiveness of the new method.
引用
收藏
页数:33
相关论文
共 59 条
  • [1] Adleman L., 1995, P C DNA BAS COMP PRI
  • [2] MOLECULAR COMPUTATION OF SOLUTIONS TO COMBINATORIAL PROBLEMS
    ADLEMAN, LM
    [J]. SCIENCE, 1994, 266 (5187) : 1021 - 1024
  • [3] [Anonymous], 2016, LIVENESS MANIFESTOS
  • [4] [Anonymous], THESIS
  • [5] Designing fast LTL model checking algorithms for many-core GPUs
    Barnat, Jiri
    Bauch, Petr
    Brim, Lubos
    Ceska, Milan
    [J]. JOURNAL OF PARALLEL AND DISTRIBUTED COMPUTING, 2012, 72 (09) : 1083 - 1097
  • [6] Immunity-Based Optimal Estimation Approach for a New Real Time Group Elevator Dynamic Control Application for Energy and Time Saving
    Baygin, Mehmet
    Karakose, Mehmet
    [J]. SCIENTIFIC WORLD JOURNAL, 2013,
  • [7] THE TEMPORAL LOGIC OF BRANCHING TIME
    BENARI, M
    PNUELI, A
    MANNA, Z
    [J]. ACTA INFORMATICA, 1983, 20 (03) : 207 - 226
  • [8] Programmable and autonomous computing machine made of biomolecules
    Benenson, Y
    Paz-Elizur, T
    Adar, R
    Keinan, E
    Livneh, Z
    Shapiro, E
    [J]. NATURE, 2001, 414 (6862) : 430 - 434
  • [9] LTL model-checking for security protocols
    Carbone, Roberto
    [J]. AI COMMUNICATIONS, 2011, 24 (03) : 281 - 283
  • [10] DNA Algorithms of Implementing Biomolecular Databases on a Biological Computer
    Chang, Weng-Long
    Vasilakos, Athanasios V.
    [J]. IEEE TRANSACTIONS ON NANOBIOSCIENCE, 2015, 14 (01) : 104 - 111