Cargando…

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...

Descripción completa

Detalles Bibliográficos
Autores principales: Zhu, Weijun, Feng, Changwei, Wu, Huanmei
Formato: Online Artículo Texto
Lenguaje:English
Publicado: Hindawi 2017
Materias:
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC5651143/
https://www.ncbi.nlm.nih.gov/pubmed/29119114
http://dx.doi.org/10.1155/2017/7941845
_version_ 1783272839621640192
author Zhu, Weijun
Feng, Changwei
Wu, Huanmei
author_facet Zhu, Weijun
Feng, Changwei
Wu, Huanmei
author_sort Zhu, Weijun
collection PubMed
description 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.
format Online
Article
Text
id pubmed-5651143
institution National Center for Biotechnology Information
language English
publishDate 2017
publisher Hindawi
record_format MEDLINE/PubMed
spelling pubmed-56511432017-11-08 Model Checking Temporal Logic Formulas Using Sticker Automata Zhu, Weijun Feng, Changwei Wu, Huanmei Biomed Res Int Research Article 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. Hindawi 2017 2017-09-28 /pmc/articles/PMC5651143/ /pubmed/29119114 http://dx.doi.org/10.1155/2017/7941845 Text en Copyright © 2017 Weijun Zhu et al. https://creativecommons.org/licenses/by/4.0/ This is an open access article distributed under the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.
spellingShingle Research Article
Zhu, Weijun
Feng, Changwei
Wu, Huanmei
Model Checking Temporal Logic Formulas Using Sticker Automata
title Model Checking Temporal Logic Formulas Using Sticker Automata
title_full Model Checking Temporal Logic Formulas Using Sticker Automata
title_fullStr Model Checking Temporal Logic Formulas Using Sticker Automata
title_full_unstemmed Model Checking Temporal Logic Formulas Using Sticker Automata
title_short Model Checking Temporal Logic Formulas Using Sticker Automata
title_sort model checking temporal logic formulas using sticker automata
topic Research Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC5651143/
https://www.ncbi.nlm.nih.gov/pubmed/29119114
http://dx.doi.org/10.1155/2017/7941845
work_keys_str_mv AT zhuweijun modelcheckingtemporallogicformulasusingstickerautomata
AT fengchangwei modelcheckingtemporallogicformulasusingstickerautomata
AT wuhuanmei modelcheckingtemporallogicformulasusingstickerautomata