Model Checking Temporal Logic Formulas Using Sticker Automata

Weijun Zhu, Changwei Feng, Huanmei Wu

Research output: Contribution to journalArticle

1 Citation (Scopus)

Abstract

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.

Original languageEnglish (US)
Article number7941845
JournalBioMed Research International
Volume2017
DOIs
StatePublished - 2017

Fingerprint

Temporal logic
Model checking
Single-Stranded DNA
Molecules
DNA
Finite automata

ASJC Scopus subject areas

  • Biochemistry, Genetics and Molecular Biology(all)
  • Immunology and Microbiology(all)

Cite this

Model Checking Temporal Logic Formulas Using Sticker Automata. / Zhu, Weijun; Feng, Changwei; Wu, Huanmei.

In: BioMed Research International, Vol. 2017, 7941845, 2017.

Research output: Contribution to journalArticle

@article{76e5740cab314974a85886fa8dbd1761,
title = "Model Checking Temporal Logic Formulas Using Sticker Automata",
abstract = "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.",
author = "Weijun Zhu and Changwei Feng and Huanmei Wu",
year = "2017",
doi = "10.1155/2017/7941845",
language = "English (US)",
volume = "2017",
journal = "BioMed Research International",
issn = "2314-6133",
publisher = "Hindawi Publishing Corporation",

}

TY - JOUR

T1 - Model Checking Temporal Logic Formulas Using Sticker Automata

AU - Zhu, Weijun

AU - Feng, Changwei

AU - Wu, Huanmei

PY - 2017

Y1 - 2017

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

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.

UR - http://www.scopus.com/inward/record.url?scp=85031902298&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85031902298&partnerID=8YFLogxK

U2 - 10.1155/2017/7941845

DO - 10.1155/2017/7941845

M3 - Article

C2 - 29119114

AN - SCOPUS:85031902298

VL - 2017

JO - BioMed Research International

JF - BioMed Research International

SN - 2314-6133

M1 - 7941845

ER -