Model Checking Temporal Logic Formulas Using Sticker Automata.
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 app...
| Publicado en: | BioMed Research International Vol. 2017; pp. 1 - 34 |
|---|---|
| Autores principales: | , , |
| Formato: | algorithm equations & formulas pictorial research tables/charts Journal Article |
| Publicado: |
Wiley-Blackwell
9/28/2017
|
| Acceso en línea: | Ver este registro en EBSCOhost |
| fields | @attributes: recordID: 1 pdfLink: plink: https://search.ebscohost.com/login.aspx?direct=true&db=ccm&AN=125383878&site=ehost-live header: @attributes: shortDbName: ccm uiTerm: 125383878 longDbName: CINAHL Complete uiTag: AN controlInfo: bkinfo: dissinfo: jinfo: jid: 23146133 FT2T jtl: BioMed Research International issn: 23146133 maglogo: N pubinfo: dt: 9/28/2017 vid: 2017 pid: 480 pub: Wiley-Blackwell place: Malden, Massachusetts artinfo: ui: 125383878 125383878 125383878 10.1155/2017/7941845 125383878 ppf: 1 ppct: 33 formats: fmt: @attributes: type: P tig: atl: Model Checking Temporal Logic Formulas Using Sticker Automata. aug: au: Zhu, Weijun Feng, Changwei Wu, Huanmei affil: School of Information Engineering, Zhengzhou University, Zhengzhou 450001, China sug: subj: Bioinformatics DNA Computer Simulation Mathematics ab: 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. pubtype: Academic Journal doctype: algorithm equations & formulas pictorial research tables/charts Journal Article ougenre: Article language: English refInfo: holdings: @attributes: islocal: N |
|---|